Canonicity in GFG and transition-based automata

Bader Abu Radi, Orna Kupferman

نتاج البحث: نشر في مجلةمقالة من مؤنمرمراجعة النظراء


Minimization of deterministic automata on finite words results in a canonical automaton. For deterministic automata on infinite words, no canonical minimal automaton exists, and a language may have different minimal deterministic Büchi (DBW) or co-Büchi (DCW) automata. In recent years, researchers have studied good-for-games (GFG) automata - nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. Several applications of automata in formal methods, most notably synthesis, that are traditionally based on deterministic automata, can instead be based on GFG automata. The minimization problem for DBW and DCW is NP-complete, and it stays NP-complete for GFG Büchi and co-Büchi automata. On the other hand, minimization of GFG co-Büchi automata with transition-based acceptance (GFG-tNCWs) can be solved in polynomial time. In these automata, acceptance is defined by a set a of transitions, and a run is accepting if it traverses transitions in α only finitely often. This raises the question of canonicity of minimal deterministic and GFG automata with transition-based acceptance. In this paper we study this problem. We start with GFG-tNCWs and show that the safe components (that is, these obtained by restricting the transitions to these not in a) of all minimal GFGtNCWs are isomorphic, and that by saturating the automaton with transitions in a we get isomorphism among all minimal GFG-tNCWs. Thus, a canonical form for minimal GFG-tNCWs can be obtained in polynomial time. We continue to DCWs with transition-based acceptance (tDCWs), and their dual tDBWs. We show that here, while no canonical form for minimal automata exists, restricting attention to the safe components is useful, and implies that the only minimal tDCWs that have no canonical form are these for which the transition to the GFG model results in strictly smaller automaton, which do have a canonical minimal form.

اللغة الأصليةإنجليزيّة أمريكيّة
الصفحات (من إلى)199-215
عدد الصفحات17
دوريةElectronic Proceedings in Theoretical Computer Science, EPTCS
مستوى الصوت326
المعرِّفات الرقمية للأشياء
حالة النشرنُشِر - 20 سبتمبر 2020
الحدث11th International Symposium on Games, Automata, Logics, and Formal Verification, G AND ALF 2020 - Virtual, Brussels, بلجيكا
المدة: ٢١ سبتمبر ٢٠٢٠٢٢ سبتمبر ٢٠٢٠

All Science Journal Classification (ASJC) codes

  • !!Software


أدرس بدقة موضوعات البحث “Canonicity in GFG and transition-based automata'. فهما يشكلان معًا بصمة فريدة.

قم بذكر هذا