CTL * i rachunek różniczkowy

9

dobrze wiadomo, że modal -calculusμ jest jedną z najbardziej ekspresyjnych logik czasowych do wyrażania właściwości drzew / grafów, i że CTL * jest ściśle mniej ekspresyjny niż -calculus.μ

W tym miejscu chciałbym poprosić o przykład formuły calculus, tak prostej, jak to możliwe, która nie jest wyrażalna w CTL *, i mam nadzieję, że wyjaśni wyjaśnienie jej znaczenia (formuły stałoprzecinkowe szybko stają się nieczytelne). Wszelkie dobre odniesienia do „konkretnego” prostego przykładu również byłyby świetne!μ

Z góry dziękuję

LORE81
źródło

Odpowiedzi:

11

Weźmy właściwość ścieżki, która nie jest wyrażalna pierwszego rzędu, np. która mówi, że istnieje ścieżka, w której propozycja atomowa utrzymuje się na każdej parzystej pozycji, a każdą wycenę można zastosować na nieparzystych pozycjach .

νx.px
p
Sylvain
źródło
wielkie dzięki za tę prostą odpowiedź. Czy możesz również zasugerować referencję na poparcie tego przykładu?
Jeszcze
Ładne pytanie i odpowiedź (+2). Zobacz cstheory.stackexchange.com/q/16186/6424 . Podałem tam również przykład równości. Może jakaś odpowiedź dotyczy również równości.
DaveBall aka user750378
@ LORE81: przykład `` na pozycjach parzystych '' to klasyk, który można znaleźć na przykład w artykule Wolpera wskazanym przez @DaveBall w jego pytaniu. Nie jest zbyt trudno udowodnić bezpośrednio przez indukcję formuł LTL; alternatywnie możesz skonstruować monoid przejściowy i zobaczyć, że nie jest nieperiodyczny; w końcu możesz wypróbować argument Ehrenfeucht-Fraïssé, choć długo trzeba szczegółowo opisywać. p
Sylvain,