Apa yang paling sederhana untuk menerapkan semua terjemahan LTL-ke-Buchi yang layak atau algoritma verifikasi LTL lainnya?

Saya sedang menulis modelchecker mainan , dan saya pada titik di mana saatnya untuk mengimplementasikan terjemahan LTL ke Buchi automata.

Untuk berbagai alasan yang jelas, saya ingin algoritme menjadi sederhana :) misalnya saya ingin kode tetap sangat jelas dan singkat selama mungkin.

Saya telah melihat pendekatan "automata lokal + kemungkinan automata", yang dijelaskan dalam beberapa tutorial, tetapi tampaknya tidak mudah untuk diimplementasikan / dipahami (bukti kebenarannya cukup besar), juga tidak menghasilkan automata kecil. Jadi saya tidak mengimplementasikannya sampai saya yakin saya tidak akan menyesal :)

Jadi, saya akan berterima kasih untuk referensi ke makalah yang menggambarkan algoritma sederhana dan efisien untuk terjemahan ini, atau mungkin yang sederhana dan tidak efisien - maka makalah tentang minimalisasi Buchi automata akan diterima juga :)

... Atau mungkin ada pendekatan alternatif yang menarik untuk verifikasi LTL?

Untuk referensi, berikut adalah silsilah algoritma terjemahan LTL-to-Buchi http://spot.lip6.fr/wiki/LtlTranslationAlgorithms . Adakah yang bisa mengatakan sesuatu tentang ini?

Satu konstruksi yang tidak tercantum di situs web SPOT diberikan dalam survei oleh Demri & Gastin, Spesifikasi dan Verifikasi menggunakan Logika Temporal , 2009. Konstruksi sederhana dan menghasilkan automata yang cukup kecil, sehingga dapat dilakukan dengan tangan untuk formulæ kecil, yang bagus untuk mengajar (seperti itulah cara saya menggunakannya), tetapi mungkin juga bermanfaat untuk men-debug implementasi. Saya tidak akan bertaruh itu lebih efisien daripada yang digunakan oleh SPOT.

Tentang minimalisasi, tidak ada otomat Büchi minimal kanonik untuk bahasa reguler diberikan. Untuk mendapatkan automata yang lebih kecil, seseorang dapat hasilkan otomat dengan beberapa hubungan simulasi. Makalah klasik tentang masalah ini adalah oleh Etessami, Wilke & Schuller, Hubungan Simulasi yang Adil, Game Paritas, dan Pengurangan Ruang Angkasa Negara untuk Büchi Automata , Jurnal SIAM tentang Komputasi 34: 1159 - 1175, 2005.$\omega$

Saya akan mempertimbangkan terjemahan yang berjalan melalui automata bolak-balik. (Lihat makalah Vardi "Alternating Automata dan verifikasi program"). Ini adalah terjemahan yang sangat elegan dari LTL ke alternata automata dan kemudian Anda dapat menggunakan Mihano Ayashi (yang juga elegan - ini adalah konstruksi subset ganda) untuk mencapai Buchi automata yang non deterministik.