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,