eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-07-04
100:1
100:16
10.4230/LIPIcs.ICALP.2019.100
article
Minimizing GFG Transition-Based Automata (Track B: Automata, Logic, Semantics, and Theory of Programming)
Abu Radi, Bader
1
Kupferman, Orna
1
School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. The minimization problem for nondeterministic and deterministic Büchi and co-Büchi word automata are PSPACE-complete and NP-complete, respectively. We describe a polynomial minimization algorithm for good-for-games co-Büchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol132-icalp2019/LIPIcs.ICALP.2019.100/LIPIcs.ICALP.2019.100.pdf
Minimization
Deterministic co-Büchi Automata