Trace-Äquivalenz vs. LTL-Äquivalenz

17

Ich suche ein einfaches Beispiel für zwei Übergangssysteme, die LTL-Äquivalent, aber kein Trace-Äquivalent sind.

Ich habe in dem Buch "Principles of Model Checking" (Baier / Katoen) den Beweis gelesen, dass die Spurenäquivalenz feiner ist als die LTL-Äquivalenz, aber ich bin nicht sicher, ob ich das wirklich verstehe. Ich kann es mir nicht vorstellen, gibt es vielleicht ein einfaches Beispiel, das den Unterschied sichtbar macht?

großartig
quelle
3
Könnte ich empfehlen, das Akronym im Titel zu erweitern. Dies wird anderen helfen, die Frage und die Antworten zu finden, und kann auch dazu beitragen, Ihre Frage an diejenigen weiterzuleiten, die gute Antworten liefern können.
Marc Hamann
1
ganz zu schweigen von google search :)
Suresh Venkat
5
@Marc: Die Verwendung des Akronyms LTL ist absolut standardmässig - modale Logiker mögen ihre kurzen Namen (denken Sie an B, D4.3, KL usw.). Ich denke, der Titel sollte nicht erweitert werden, da wir den Tag haben.
Charles Stewart
1
Die Frage ist noch nicht sehr klar definiert: Erlauben Sie unendliche Kripke-Strukturen? Betrachten Sie gemischte (maximale) endliche und unendliche Spuren oder lassen Sie nur unendliche zu? Ich frage, weil AFAICR Baier & Katoen nur den Fall endlicher Kripke-Strukturen und unendlicher Spuren betrachten, die Daves Antwort unten ausschließen.
Sylvain
1
@atticae: Mit endlichen totalen Kripke-Strukturen (und damit unendlichen Spuren) würde ich erwarten, dass LTL-Äquivalenz und Spurenäquivalenz dasselbe sind ... Ich werde darüber nachdenken.
Sylvain

Antworten:

9

Bei genauerer Betrachtung von Baier und Katoen ziehen sie sowohl endliche als auch unendliche Übergangssysteme in Betracht. Siehe Seite 20 dieses Buches für Definitionen.

Nehmen Sie zunächst das einfache Übergangssystem :EVEN

SOGAR

Lemma: Keine LTL-Formel erkennt die Sprache Traces ( E V E N ) . Ein String c L e v e n iff c i = a für gerade i . Siehe Wolper '81 . Sie können dies beweisen, indem Sie zunächst zeigen, dass keine LTL-Formel mit n "next-time" -Operatoren die Zeichenfolgen der Form p i ¬ p p ω für i > n unterscheiden kannLeven=(EVEN)cLevenci=ainpi¬ppωi>ndurch eine einfache Induktion.

Betrachten Sie das folgende (unendlich, nicht-deterministisch ) Übergangssystem . Beachten Sie, dass es zwei verschiedene Ausgangszustände gibt:NOTEVEN

Bildbeschreibung hier eingeben

Seine Spuren sind genau .{a,¬a}ωLeven

NOTEVENϕEVEN¬ϕ

Betrachten Sie nun dieses einfache Übergangssystem :TOTAL

TS gesamt

Seine Spuren sind eindeutig .{a,¬a}ω

Daher sind und keine Trace-Äquivalente. Angenommen, sie wären LTL-ungleichwertig. Dann hätten wir eine LTL-Formel so dass und . Aber dann . Das ist ein Widerspruch.NOTEVENTOTALϕNOTEVENϕTOTALϕEVEN¬ϕ

Vielen Dank an Sylvain, der in der ersten Version dieser Antwort einen dummen Fehler entdeckt hat.

Mark Reitblatt
quelle
Hmm, das ist nicht ganz klar. Sollte ich die Schritte um den Widerspruch deutlicher machen? Die Übergangssysteme sind auch nicht so hübsch wie sie sein könnten ...
Mark Reitblatt
Sie interpretieren die Sprache falsch : Das von Ihnen vorgeschlagene System entspricht der Formel . Das richtige System sollte eine nichtdeterministische Auswahl in dem Anfang hat, -markierten Zustand zwischen einem Zustand gehen durch markierte und ein nicht durch markierte . Sowohl als auch haben Übergänge, die zu . LevenaG((aX¬a)(¬aXa))aq0q1aq2aq1q2q0
Sylvain
@ Sylvain du hast recht. Ich habe versucht, es zu vereinfachen und habe es schließlich gebrochen! Lassen Sie mich das beheben.
Mark Reitblatt
Können Sie das Argument nicht "umkehren", sodass die beiden Systeme, die Sie am Ende vergleichen, und anstelle von und ? EVENTOTALNOTEVENTOTAL
Sylvain
1
@ Mark Reitblatt: Woraus schließen Sie diesen Satz am Ende ab ? "Aber dann, ." Ich kann keine Argumentation sehen, die zu diesem Punkt führt, der für die Darstellung des Widerspruchs wesentlich ist. EVEN¬ϕ
Magnattic
3

Wenn Ihre LTL-Definition den Operator "next" enthält, gilt Folgendes. Sie haben zwei Sätze von Spuren und . Lassen in jedem endlichen Präfix eine Spur sein . muss auch ein endliches Präfix eines Traces in , da Sie dies ansonsten in eine Formel umwandeln können, die nur eine Reihe von Next-Operatoren ist, die den Unterschied erkennen. Daher muss jedes endliche Präfix eines Wortes ein endliches Präfix eines Wortes sein und umgekehrt. Dies bedeutet, dass wenn , es ein Wort in so dass alle seine endlichen Präfixe in aberABbBbABAABbAban sich wird nicht in . Wenn und durch endliche Übergangssysteme erzeugt werden , halte ich dies für unmöglich. Angenommen, Sie definieren unendliche ÜbergangssystemeAAB

A={a,b}ω und wobei zB das unendliche Wort .B=A{w}waba2b2a3b3a4b4

Jede LTL-Formel, die universell für gilt, gilt universell für da eine Teilmenge von . Jede LTL-Formel, die für gilt , gilt auch für ; Nehmen wir aus Gründen des Widerspruchs nicht an, aber dass für jedes Element von (dh für jedes Element des Universums, das für das Wort erwartet wird ), aber nicht für . Dann wird für als wahr ausgewertet, für kein anderes Wort des Universums jedoch (und LTL wird unter Negation geschlossen), und es gibt keine LTL-Formel, die nur für wahr sein kannABBABAφBww¬φwwwie jeder Buchi-Automat, der nur ein unendliches Wort akzeptiert, streng zyklisch sein muss, während nicht zyklisch ist.w

antti.huima
quelle
Das sind endliche Spuren. Angenommen, Sie erweitern sie auf unendliche Spuren mit am Ende, dann akzeptiert die Formel die zweite Menge, lehnt jedoch die erste ab. ¬ ( b X ( b X G a ) )aω¬(bX(bXGa))
Mark Reitblatt
Du hast recht, ich habe eine neue Antwort geschrieben :) LOL, ich erinnere mich aus meiner theoretischen Zeit, dass LTL nicht den nächsten Operator hat :)
antti.huima
Ich denke, das macht den Trick.
Dave Clarke
Ich denke es funktioniert auch.
Mark Reitblatt
Diese Antwort ist nicht zufriedenstellend. Das OP forderte Übergangssysteme, aber die Antwort bezieht sich auf Sprachen und ist in Bezug auf Buchi-Automaten und reguläre Sprachen gerechtfertigt , die nicht in dem Text enthalten sind, auf den verwiesen wird. ω
Mark Reitblatt