Bagaimana cara membuktikan bahwa formula tidak dapat diekspresikan dalam LTL, tetapi dapat di Buchi automata?

11

Saya mencari teknik umum yang dapat membantu saya membuktikan tidak hanya bahwa Buchi automata adalah model yang lebih ekspresif daripada LTL, tetapi formula spesifiknya dapat / tidak dapat diungkapkan dalam LTL.

Misalnya, " terjadi setidaknya pada posisi genap" dapat dijelaskan oleh Buchi automata berikut: mana dan .hal(q0,q1,Σ,δ,q0,{q0})δ(q1,∗)=q0δ(q0,p)=q1

Saya telah membaca bahwa automata tidak dapat diekspresikan dalam LTL, tetapi saya tidak mengerti bagaimana membuktikannya secara formal.

Terima kasih.

lo.logic automata-theory Daniil
sumber
Lucu. Saya melihat slide-slide itu hari ini juga.
Dave Clarke

Jawaban:

9

Pertama, Anda perlu tahu apa yang ingin Anda ungkapkan dan bagaimana Anda akan mengungkapkannya. Misalnya, Anda bisa mewakili properti sebagai serangkaian jejak tak terbatas.

Properti yang dapat didefinisikan oleh Buechi automata adalah regular bahasa. Properti yang dapat didefinisikan oleh rumus LTL adalah bahasa reguler bebas bintang. Bahasa bebas bintang adalah subset ketat dari bahasa tidak reguler .ωωω

Bagian 5.1 dari Prinsip-prinsip Model Memeriksa oleh Baier dan Katoen adalah titik awal yang baik dan dasar. Jika Anda ingin teknik pembuktian umum ada berbagai cara untuk melanjutkan. Salah satu teknik umum yang menarik bagi saya adalah menggunakan game. Pemain pertama yang mencoba menunjukkan dua struktur dapat dibedakan dengan formula LTL. Yang kedua menunjukkan mereka sama. Dua struktur setara dengan LTL jika pemain kedua memiliki strategi kemenangan. Jadi, jika Anda mengambil dua struktur yang bukan isomorfis tetapi pemain kedua memiliki strategi kemenangan, maka, tidak ada formula LTL untuk membedakan keduanya.

Hierarki Hingga dan Aplikasi Lain dari Game Ehrenfeucht-Fraisse untuk Temporal Logic , K. Etessami dan Th. Wilke.

Ada algoritma untuk memeriksa apakah bahasa reguler diberikan bebas bintang. Sayangnya ini biasanya ditulis di dalam bukti teorema.ω

Keterbatasan logis pada jejak tak terbatas , Werner Ebinger dan Anca Muscholl

Saya akan menggali sedikit lebih banyak dan mencoba menemukan presentasi yang lebih algoritmik.

Vijay D
sumber
Saya minta maaf jika saya tidak cukup jelas. Saya membaca sekilas 5.1 Prinsip Memeriksa Model dan saya tidak menemukan informasi baru. Saya tahu apa itu LTL dan bagaimana mengekspresikan properti dengannya. Saya juga tahu bahwa ada properti tertentu yang tidak dapat Anda ungkapkan dalam LTL (mis. bahasa biasa lebih ekspresif). Saya tahu bahwa formula LTL dapat dikonversi ke Buchi automata. Namun, saya tidak tahu bagaimana membuktikan bahwa Buchi-automata tertentu TIDAK dapat dikonversi ke LTL. ω
Daniil
Jadi, jika saya membuktikan bahwa properti tertentu dapat diekspresikan hanya dalam bahasa reguler bebas bintang, maka properti tersebut tidak dapat dinyatakan dalam LTL. Jadi saya mencari teknik untuk membuktikannya untuk properti tertentu.
Daniil
Masalah memutuskan apakah bahasa reguler bebas bintang dapat ditentukan. Algoritma dianggap sebagai teknik bukti umum. Saya mencoba menemukan referensi yang menjawab pertanyaan Anda dengan tepat. Referensi yang saya sertakan di atas tidak tepat, tetapi saya berharap mereka berwawasan luas. ω
Vijay D
ω
Saya, secara pribadi lebih suka teknik aljabar. Intuisi saya buruk pada umumnya dan saya menemukan teknik aljabar membuat saya lebih sedikit ikan haring merah dan bukti lebih pendek. Namun, dari penolakan kertas dan presentasi, saya memiliki kesan mayoritas ilmuwan komputer lebih suka game atau teknik bukti relasional (bisimulasi, dll).
Vijay D
7

Saya akan menyarankan menggunakan karakterisasi bahasa orde pertama oleh Büchi automata bebas-counter: lihat misalnya V. Diekert dan P. Gastin, bahasa -bahasa yang dapat didefinisikan tingkat-Pertama . Dalam Logika dan Automata: Sejarah dan Perspektif, Teks dalam Logika dan Game 2, halaman 261--306. Amsterdam University Press, 2008. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf

PS: lebih dari kata-kata yang terbatas, kolom BEATCS ini juga sangat membantu: J.-E. Pin, Logic on Words , http://hal.archives-ouvertes.fr/hal-00020073 .

Sylvain
sumber
4

ω

ω

ωx∈Snxn=xn+1

Ini memberi Anda algoritma untuk definisi-LTL.

Denis
sumber