CTL * i rachunek różniczkowy

dobrze wiadomo, że modal -calculus$\mu$ 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.$\mu$

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!$\mu$

Z góry dziękuję

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 .