Automata pada Objek Tak Terbatas

Automata pada objek tak terbatas membaca masukan yang tidak pernah berakhir, seperti kata tak terbatas atau pohon tak terbatas, dan menerima sesuai dengan status atau transisi mana yang dikunjungi secara tak terbatas, menyediakan mesin matematis untuk penalaran tentang sistem yang sedang berlangsung dan tidak berakhir.

Definition

Omega-automaton adalah mesin keadaan-terbatas yang jalannya tak terbatas, dengan penerimaan didefinisikan oleh kondisi pada himpunan keadaan yang dikunjungi secara tak terbatas; automata semacam itu mengenali himpunan kata atau pohon tak terbatas yang disebut bahasa omega-reguler.

Scope

Topik ini mencakup automata Büchi, Muller, Rabin, dan paritas pada kata tak terbatas, kondisi penerimaan yang membedakannya, hasil determinisasi dan komplementasi, automata pada pohon tak terbatas, dan hubungan mendalam antara automata ini, logika orde kedua monadik, dan permainan tak terbatas yang digunakan dalam sintesis dan verifikasi.

Core questions

• Bagaimana mesin terbatas dapat menerima atau menolak masukan yang tidak memiliki akhir?
• Mengapa automata Büchi nondeterministik dan deterministik berbeda dalam kekuatan ekspresif?
• Bagaimana automata pada objek tak terbatas berhubungan dengan logika untuk menentukan perilaku sistem?
• Apa yang membuat komplementasi automata ini sulit, dan mengapa itu penting?

Key theories

Penerimaan Büchi dan bahasa omega-reguler

Automaton Büchi menerima kata tak terbatas ketika beberapa keadaan penerima dikunjungi secara tak terbatas, dan bahasa yang dikenali demikian, bahasa omega-reguler, bertepatan dengan yang dapat didefinisikan dalam logika orde kedua monadik pada bilangan asli.

Determinisasi dan kondisi paritas

Automata Büchi nondeterministik umumnya tidak dapat dibuat deterministik tanpa mengubah kondisi penerimaan, tetapi konstruksi Safra mengubahnya menjadi automata Rabin atau paritas deterministik, yang penting untuk komplementasi dan untuk memecahkan permainan.

Clinical relevance

Omega-automata adalah tulang punggung algoritmik dari pemeriksaan model (model checking): sistem reaktif dan properti logika temporal masing-masing diterjemahkan ke dalam automata pada kata tak terbatas, dan pemeriksaan properti tersebut direduksi menjadi uji kekosongan, memungkinkan verifikasi otomatis perangkat keras, protokol, dan perangkat lunak konkuren.

History

Büchi memperkenalkan automata pada kata tak terbatas sekitar tahun 1960 untuk memutuskan teori orde kedua monadik dari bilangan asli, McNaughton menunjukkan cara untuk mendeterminasikannya dengan kondisi penerimaan yang lebih kuat, dan Rabin memperluas teori tersebut ke pohon tak terbatas, hasil yang menjadi sentral untuk verifikasi setelah logika temporal memasuki ilmu komputer pada akhir tahun 1970-an.

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

Bagaimana mesin dapat menerima masukan tak terbatas?

Penerimaan didefinisikan bukan dengan mencapai keadaan akhir pada akhirnya, karena tidak ada akhir, tetapi oleh keadaan mana yang berulang. Automaton Büchi, misalnya, menerima ketika melewati keadaan penerima yang ditentukan secara tak terbatas selama jalannya yang tak berujung.

Mengapa automata ini penting untuk verifikasi?

Sistem yang tidak berakhir seperti sistem operasi dan protokol jaringan secara alami dimodelkan oleh perilaku tak terbatas. Properti seperti "sistem tidak pernah mengalami kebuntuan" atau "setiap permintaan pada akhirnya dilayani" menjadi bahasa omega-reguler, sehingga memeriksanya direduksi menjadi operasi automata yang dapat dilakukan secara otomatis oleh pemeriksa model (model checker).