Równoważność śladu vs równoważność LTL

Szukam prostego przykładu dwóch systemów przejściowych, które są równoważne LTL, ale nie równoważne.

Przeczytałem dowód na to, że Trace Equivalence jest lepszy niż LTL Equivalence w książce „Principles of Model Checking” (Baier / Katoen), ale nie jestem pewien, czy naprawdę to rozumiem. Nie jestem w stanie tego wyobrazić, czy może jest prosty przykład, który może zobrazować różnicę?

lo.logic model-checking linear-temporal-logic

— magnetyczny
źródło

Może polecam rozszerzenie akronimu w tytule. Pomoże to innym znaleźć pytanie i odpowiedź, a także może zwrócić uwagę na pytanie tych, którzy mogą udzielić dobrych odpowiedzi.

— Marc Hamann,

nie wspominając o wyszukiwaniu w Google :)

— Suresh Venkat

@Marc: Używanie akronimu LTL jest absolutnie standardowe - modalni logicy lubią ich krótkie nazwy (pomyśl B, D4.3, KL i c.). Myślę, że tytuł nie powinien być rozszerzany, biorąc pod uwagę, że mamy tag.

— Charles Stewart

Pytanie wciąż nie jest dobrze zdefiniowane: czy pozwalasz na nieskończone struktury Kripke? Czy rozważasz mieszane (maksymalne) ślady skończone i nieskończone, czy dopuszczasz tylko te nieskończone? Pytam, ponieważ AFAICR Baier i Katoen rozważają jedynie przypadek skończonych struktur Kripke i nieskończonych śladów, co wyklucza odpowiedź Dave'a poniżej.

— Sylvain,

@atticae: przy skończonych strukturach Kripke (a więc nieskończonych śladach) oczekiwałbym, że równoważność LTL i równoważność śledzenia będą takie same ... Pomyślę o tym.

— Sylvain,

Odpowiedzi:

Czytając uważnie Baiera i Katoena, rozważają zarówno skończone, jak i nieskończone systemy przejściowe. Definicje znajdują się na stronie 20 tej książki.

Najpierw weź prosty system przejściowy : $EVEN$

PARZYSTY

Lemat: Żadna formuła LTL nie rozpoznaje języka Ślady . Ciąg iff dla parzystego . Zobacz Wolper '81 . Można to udowodnić najpierw pokazując, że nie formuła LTL z operatorów „następny raz” można odróżnić ciągi postaci $L_{even} =$ $(EVEN)$ $c \in L_{even}$ $c_i = a$ $i$ $n$ dla $p^i\neg p p^\omega$ $i> n$ , przez prostą indukcję.

Rozważmy następujące (nieskończonej niedeterministycznego) system przejścia, . Zauważ, że istnieją dwa różne stany początkowe: $NOTEVEN$

wprowadź opis zdjęcia tutaj

Jego ślady to dokładnie . $\{a,\neg a\}^\omega - L_{even}$

W następstwie lematu: Jeśli to $NOTEVEN \vDash \phi$ $EVEN \not\vDash \neg\phi$

Rozważmy teraz ten prosty system przejściowy : $TOTAL$

Ogółem TS

Jego ślady są wyraźnie . $\{a,\neg a\}^\omega$

Zatem i nie są równoważne śladowo. Załóżmy, że były niesprawne LTL. Wtedy mielibyśmy wzór LTL taki, że i . Ale potem . To jest sprzeczność. $NOTEVEN$ $TOTAL$ $\phi$ $NOTEVEN \vDash \phi$ $TOTAL \not\vDash \phi$ $EVEN\vDash \neg\phi$

Dzięki Sylvainowi za złapanie głupiego błędu w pierwszej wersji tej odpowiedzi.

— Mark Reitblatt
źródło

Hmm, to nie jest całkowicie jasne. Czy powinienem uściślić kroki wokół sprzeczności? Systemy przejściowe też nie są tak ładne, jak mogłyby być ...

— Mark Reitblatt,

Źle interpretujesz język

: proponowany system jest równoważny formule

. Prawidłowy system powinien na początku mieć niedeterministyczny wybór,

L_{even}

$L_\text{even}$

a \land G ((a \to X \neg a) \land (\neg a \to X a))

$a\wedge\mathsf{G}((a\to\mathsf{X}\neg a)\wedge(\neg a\to\mathsf{X}a))$

znakowanych stanu

między przechodząc do stanu

oznaczonego przez

i jednego

nie oznaczonego przez. Zarówno

a

$a$

q_{0}

$q_0$

q_{1}

$q_1$

a

$a$

q_{2}

$q_2$

a

$a$

q_{1}

$q_1$

q_{2}

$q_2$ przejścia mają powrót do

q_{0}

$q_0$

— Sylvain,

@Sainain masz rację. Próbowałem uprościć i ostatecznie to złamałem! Pozwól mi to naprawić.

— Mark Reitblatt,

Czy nie można „odwrócić” argumentu, aby dwa porównywane systemy to

zamiast

E V E N

$\mathit{EVEN}$

T O T A L

$\mathit{TOTAL}$

N O T E V E N

$\mathit{NOTEVEN}$

T O T A L

$\mathit{TOTAL}$

— Sylvain,

@ Mark Reitblatt: Z czego rozumujesz to zdanie na końcu: „Ale w takim razie

.”? Nie widzę argumentów, które prowadzą do tego punktu, który jest niezbędny do wykazania sprzeczności.

E V E N ⊨ \neg ϕ

$EVEN\vDash \neg\phi$

— magnatyczny

Jeśli twoja definicja LTL obejmuje operatora „next”, obowiązują następujące zasady. Masz dwa zestawy śladów i . Niech być dowolny skończony prefiksem śladu w . musi być również skończonym prefiksem śledzenia w , ponieważ w przeciwnym razie możesz przekonwertować to na formułę, która jest tylko serią kolejnych operatorów wykrywających różnicę. Dlatego każdy skończony prefiks słowa musi być skończonym prefiksem słowa i odwrotnie. Oznacza to, że jeśli , musi istnieć słowo , aby wszystkie jego skończone prefiksy pojawiły się w ale $A$ $B$ $b$ $B$ $b$ $A$ $B$ $A$ $A \not= B$ $b$ $A$ sam w sobie nie pojawia się w . Jeślisą generowane przezskończonesystemy przejściowe, myślę, że jest to niemożliwe. Zakładając nieskończone systemy przejściowe, możesz zdefiniować $b$ $A$ i $A$ $B$

i gdzie jest np. Nieskończonym słowem $A = \{a,b\}^\omega$ $B = A \setminus \{w\}$ $w$ . $aba^2b^2a^3b^3a^4b^4\cdots$

Wszelkie formuła LTL że posiada uniwersalnie do odbędzie się uniwersalnie do bo jest podzbiorem . Każda formuła LTL, która obowiązuje dla również dotyczy ; ze względu na sprzeczność załóżmy, że nie, ale dla każdego elementu (tj. dla każdego elementu wszechświata oczekuje słowa ), ale nie dla . Następnie sprawdza się jako prawda na ale nie na żadnym innym słowie wszechświata (i LTL jest zamknięte pod negacją), i nie ma formuły LTL, która może być prawdziwa tylko dla $A$ $B$ $B$ $A$ $B$ $A$ $\varphi$ $B$ $w$ $w$ $\neg\varphi$ $w$ $w$ ponieważ każdy automat Buchi, który akceptuje tylko jedno nieskończone słowo, musi być ściśle cykliczny, podczas gdy nie. $w$

— antti.huima
źródło

To skończone ślady. Zakładając, że przedłużona do nieskończoności śladów z

na końcu wzór

przyjmuje drugi zestaw lecz odrzuca pierwszy.

a^{ω}

$a^\omega$

\neg (b \land X (b \land X G a))

$\neg (b\wedge X (b \wedge X G a))$

— Mark Reitblatt,

Masz rację, napisałem nową odpowiedź :) LOL, przypomniałem sobie z moich teoretycznych czasów, że LTL nie ma następnego operatora :)

— antti.huima

Myślę, że to wystarczy.

— Dave Clarke,

Myślę, że to też działa.

— Mark Reitblatt,

Ta odpowiedź nie jest satysfakcjonująca. OP poprosił o systemy przejściowe, ale odpowiedź dotyczy języków i jest uzasadniona w odniesieniu do automatów Buchi i języków

regularnych, których nie ma w odnośnym tekście.

ω

$\omega$

— Mark Reitblatt,