Trace Equivalence vs LTL Equivalence

Saya mencari contoh mudah dari dua sistem transisi yang setara LTL, tetapi tidak setara jejak.

Saya telah membaca bukti Trace Equivalence yang lebih baik daripada LTL Equivalence dalam buku "Principles of Model Checking" (Baier / Katoen) tapi saya tidak yakin saya benar-benar memahaminya. Saya tidak dapat menggambarkannya, apakah mungkin ada contoh sederhana yang dapat memvisualisasikan perbedaannya?

Membaca Baier dan Katoen dengan cermat, mereka mempertimbangkan sistem transisi yang terbatas dan tidak terbatas. Lihat halaman 20 buku itu untuk definisi.

Pertama, ambil sistem transisi sederhana :$EVEN$

Lemma: Tidak ada formula LTL yang mengenali bahasa Jejak ( E V E N ) . Sebuah string c ∈ L e v e n iff c i = a untuk genap i . Lihat Wolper '81 . Anda dapat membuktikan ini dengan terlebih dahulu menunjukkan bahwa tidak ada formula LTL dengan n "waktu-berikutnya" operator dapat membedakan string dari bentuk p i ¬ p p ω untuk i > $L_{even} =$$(EVEN)$$c \in L_{even}$$c_i = a$$i$$n$$p^i\neg p p^\omega$$i> n$, dengan induksi sederhana.

Pertimbangkan hal berikut (tak terbatas, non-deterministik) sistem transisi . Perhatikan bahwa ada dua kondisi awal yang berbeda:$NOTEVEN$

Jejaknya persis .$\{a,\neg a\}^\omega - L_{even}$

Akibat wajar bagi Lemma: Jika maka E V E N ⊭ ¬ $NOTEVEN \vDash \phi$$EVEN \not\vDash \neg\phi$

Sekarang, pertimbangkan sistem transisi sederhana ini :$TOTAL$

Jejaknya jelas .$\{a,\neg a\}^\omega$

Jadi, dan T O T A $NOTEVEN$$TOTAL$ tidak setara jejak. Misalkan mereka tidak setara LTL. Maka kita akan memiliki formula LTL sehingga N O T E V E N ⊨ ϕ dan T O T A L ⊭ $\phi$$NOTEVEN \vDash \phi$$TOTAL \not\vDash \phi$ . Tapi kemudian, . Ini adalah kontradiksi.$EVEN\vDash \neg\phi$

Terima kasih kepada Sylvain karena telah menangkap bug bodoh di versi pertama dari jawaban ini.

Jika definisi LTL Anda termasuk operator "selanjutnya", maka yang berikut ini berlaku. Anda memiliki dua set jejak dan B . Biarkan b menjadi awalan terbatas jejak di B . b juga harus merupakan awalan terbatas jejak dalam$A$$B$$b$$B$$b$ , karena jika tidak, Anda dapat mengonversikannya ke rumus yang hanya serangkaian operator berikutnya yang mendeteksi perbedaannya. Oleh karena itu setiap awalan terbatas dari suatu B- kata harus menjadi awalan terbatas darikata- A dan sebaliknya. Ini berarti bahwa jika A ≠ B , perlu ada kata dalam b sehingga semua awalan terbatasnya muncul dalam A tetapi$A$$B$$A$$A \not= B$$b$$A$ sendiri tidak muncul dalam A . Jika A dan B dihasilkan olehsistem transisihinggasaya pikir ini tidak mungkin. Dengan asumsi sistem transisi yang tak terbatas, Anda dapat mendefinisikan$b$$A$$A$$B$

dan B = A ∖ { w } di mana w misalnya kata tak terbatas$A = \{a,b\}^\omega$$B = A \setminus \{w\}$$w$ .$aba^2b^2a^3b^3a^4b^4\cdots$

Formula LTL yang memegang universal untuk akan mengadakan universal untuk B karena B adalah himpunan bagian dari A . Formula LTL apa pun yang berlaku untuk B juga berlaku untuk A ; demi kontradiksi, menganggap tidak, tapi itu φ berlaku untuk setiap elemen B (yaitu untuk setiap elemen alam semesta harapkan untuk kata w ) tetapi tidak untuk w . Kemudian ¬ φ mengevaluasi true pada w tetapi tidak pada kata lain dari alam semesta (dan LTL ditutup dengan negasi), dan tidak ada formula LTL yang dapat benar hanya untuk $A$$B$$B$$A$$B$$A$$\varphi$$B$$w$$w$$\neg\varphi$$w$$w$ karena setiap otomat Buchi yang hanya menerima satu kata tak terbatas harus siklik sedangkan $w$ tidak.