Ekspresyjność Büchi vs CTL (*)

Jaki jest związek między ekspresyjnością LTL , Büchi / QPTL , CTL i CTL * ?

Czy możesz podać odniesienia, które obejmują tak wiele logiki czasowej, jak to możliwe (szczególnie między czasem liniowym a rozgałęzieniem)?

Idealny byłby diagram Venna z logiką czasową i pewnymi praktycznymi właściwościami jako przykładami.

Na przykład:

• Czy to prawda, że ​​w Büchi istnieją właściwości określone, ale nie w CTL *? Czy masz dobry przykład?
• Co powiesz na Büchi i CTL, ale nie na LTL?

Detale:

Ekspresyjność logiki jest dla mnie bardziej istotna niż przykłady. Ten ostatni jest po prostu pomocny dla zrozumienia i motywacji.

Wiem już o twierdzeniu o wyrazistości między CTL * i LTL z [Clarke i Draghicescu, 1988] , ale nie podoba mi się zwykły przykład uczciwości w CTL, a nie w LTL, ponieważ istnieje mnóstwo wariantów uczciwości, z których niektóre są wyrażalny w LTL.

Nie podoba mi się również zwykły przykład równości Büchi, podany np. W [Wolper83] o ograniczeniach LTL, ponieważ dodanie innej zmiennej zdań rozwiązałoby problem ( ).$even(p) \equiv q \wedge \Box ( q \implies X \neg q ) \wedge \Box ( \neg q \implies X q ) \wedge \Box ( q \implies p )$

Podoba mi się przykład równości Büchi-własności, podany np. W [Wolper83] na temat ograniczeń LTL, ponieważ jest on prosty i pokazuje konieczność PQTL dla równości (dzięki za uwagę poniżej).

Aktualizacja:

Myślę, że twierdzenie o ekspresyjności między CTL * i LTL z [Clarke i Draghicescu, 1988] można przenieść na automaty Büchi, w wyniku czego:

Let $\phi$ be a CTL* state formula. 
Then $\phi$ is expressible via Büchi automaton 
         iff $\phi$ is equivalent to $A\phi^d$.

Dzięki temu Büchi CTL * = LTL, odpowiadając na moje pytania powyżej:$\cap$

• Czy to prawda, że ​​w Büchi istnieją właściwości określone, ale nie w CTL *? Yes, e.g. evenness.
• Co powiesz na Büchi i CTL, ale nie na LTL? No.

Czy ktoś podniósł już twierdzenie Clarke'a i Draghicescu do automatów Büchi, czy wypowiedział podobne twierdzenie? A może jest to zbyt trywialne, aby o nim wspominać, skoro kwantyfikatory ścieżki CTL * są oczywiście „ortogonalne” względem kryteriów stanów akceptowanych ścieżek przez automaty Büchi?

Jedną rzeczą, na którą musimy wyjaśnić, jest rodzaj własności, o której mówimy: CTL i CTL * to logika czasu rozgałęzienia, używana do mówienia o językach drzewiastych, podczas gdy LTL to logika czasu liniowego, która per se mówi o słowach , ale można go zastosować do drzew, wymagając od wszystkich gałęzi spełnienia wzoru.

To już daje podpowiedź dla niektórych właściwości CTL, których LTL nie może wyrazić, a mianowicie tych, które łączą uniwersalne i egzystencjalne kwantyfikatory ścieżki, takie jak AGEFp („Zawsze można uzyskać stan p”). Typowym przykładem w innym kierunku jest FGa, patrz na przykład http://blob.inf.ed.ac.uk/mlcsb/files/2010/02/mlcsb7.pdf w celu uzyskania szczegółowych informacji (i diagram Venna).

Jeśli chodzi o automaty, sprawy stają się bardziej skomplikowane. Możesz mówić o automatach do słów lub drzew; jeśli to drugie, należy zauważyć, że automaty Büchi są mniej wyraziste niż inne warunki akceptacji (Rabin / parzystość / ...) w tym przypadku. Zobacz na przykład http://www.cs.rice.edu/~vardi/papers/lics96r1.ps.gz dla porównań (w tym w przypadku języków pochodnych, które są językami drzewa rozpoznawalnymi przez automatyczne słowa).

Nie odpowiadam na pełne pytanie, ale tylko na jego część (nie jestem zainteresowany czasem rozgałęziania).

$\mathit{even}$$\mathit{even}(p) \equiv \exists q.(q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p ))$$q$$q$informacji nie ma w twoim systemie, więc nie powinna być wolną zmienną twojej formuły (w przeciwnym razie twój system i twoja formuła są zdefiniowane na różnych alfabetach). Taka formuła jest formułą LTL egzystencjalnie obliczoną (w skrócie EQLTL).

$\exists$$\exists q.(q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p ))$$q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p )$$q$$\exists s_1.\exists s_2\ldots$$\exists s_1.\exists s_2.(s_1\land\Box(s_1\rightarrow a\land \mathsf{X}s_2)\land\Box(s_2)\rightarrow b\land\mathsf{X}(s_1))\land\Box\Diamond s_2\land\Box(\bigwedge_i (s_i\rightarrow\bigwedge_{j\ne i}\neg s_j)))$$s_1$$s_2$$a$$s_2$$s_1$$b$$s_2$Stutter-Invariant Languages, ω-Automata i Temporal-Logic na ten temat.

$\exists q$$q$$even$

$\exists$$\forall$

$\mathsf{EF}\mathsf{AG}p$