Jak udowodnić, że formuła nie może być wyrażona w LTL, ale może być w automatach Buchi?

11

Szukam ogólnej techniki, która może mi pomóc udowodnić nie tylko, że automaty Buchi są bardziej ekspresyjnym modelem niż LTL, ale że konkretna formuła może / nie może być wyrażona w LTL.

Na przykład „ występuje co najmniej na parzystych pozycjach” można opisać następującymi automatami Buchi: gdzie i . $p$ $({q_0, q_1}, \Sigma, \delta, q_0, \{q_0\})$ $\delta(q_1, *) = q_0$ $\delta(q_0, p) = q_1$

Mam przeczytać , że automaty nie mogą być wyrażone w LTL, ale nie rozumiem, jak formalnie udowodnić.

Dzięki.

lo.logic automata-theory

— Daniil
źródło

Zabawny. Też dzisiaj oglądałem te slajdy.

— Dave Clarke

9

Najpierw musisz wiedzieć, co chcesz wyrazić i jak zamierzasz to wyrazić. Na przykład możesz reprezentować właściwość jako zestaw nieskończonych śladów.

$\omega$ $\omega$

Punkt 5.1 zasad sprawdzania modeli Baiera i Katoena jest dobrym, elementarnym punktem wyjścia. Jeśli potrzebujesz ogólnych technik dowodowych, istnieje wiele różnych sposobów postępowania. Jedną z ogólnych technik, która mi się podoba, jest używanie gier. Pierwszy gracz próbuje pokazać dwie struktury, które można rozróżnić za pomocą formuły LTL. Drugi pokazuje, że są takie same. Dwie struktury są równoważne LTL, jeśli drugi gracz ma zwycięską strategię. Tak więc, jeśli weźmiesz dwie struktury, które nie są izomorficzne, ale drugi gracz ma zwycięską strategię, wówczas nie ma formuły LTL, aby je rozróżnić.

Until Hierarchy and Other Applications of a Ehrenfeucht-Fraisse Game for Temporal Logic , K. Etessami and Th. Wilke.

$\omega$

Logiczna definiowalność nieskończonych śladów , Werner Ebinger i Anca Muscholl

Skopię jeszcze trochę i spróbuję znaleźć bardziej algorytmiczną prezentację.

— Vijay D.
źródło

ω

$\omega$

Jeśli więc udowodnię, że konkretna właściwość może być wyrażona tylko w języku regularnym innym niż gwiazdka, oznacza to, że właściwość nie może być wyrażona w LTL. Dlatego szukam technik, które mogłyby to udowodnić dla określonych właściwości.

— Daniil,

ω

$\omega$

ω

$\omega$

Ja osobiście wolę techniki algebraiczne. Moja intuicja jest ogólnie okropna i odkryłem, że techniki algebraiczne prowadzą mnie do mniejszej liczby czerwonych śledzi i krótszych dowodów. Jednak z papierowych odrzuceń i prezentacji mam wrażenie, że większość informatyków preferuje gry lub techniki sprawdzania relacji (bisimulation itp.).

— Vijay D

7

Sugerowałbym wykorzystanie charakterystyki języków pierwszego rzędu przez bezbłędne automaty Büchi: patrz np. V. Diekert i P. Gastin, Języki definiowane pierwszego rzędu . In Logic and Automata: History and Perspectives, Texts in Logic and Games 2, strony 261--306. Amsterdam University Press, 2008. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf

PS: ponad skończonymi słowami ta kolumna BEATCS jest również bardzo pomocna: J.-E. Pin, Logic on Words , http://hal.archives-ouvertes.fr/hal-00020073 .

— Sylvain
źródło

4

$\omega$

$\omega$ $x\in S$ $n$ $x^n=x^{n+1}$

To daje algorytm definiowalności LTL.

— Denis
źródło