Bader Abu Radi ; Orna Kupferman - Minimization and Canonization of GFG Transition-Based Automata

lmcs:7587 - Logical Methods in Computer Science, August 2, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:16)2022
Minimization and Canonization of GFG Transition-Based AutomataArticle

Authors: Bader Abu Radi ; Orna Kupferman

    While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) 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 deterministic Büchi and co-Büchi word automata is NP-complete. In particular, no canonical minimal deterministic automaton exists, and a language may have different minimal deterministic automata. We describe a polynomial minimization algorithm for GFG co-Büchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set $\alpha$ 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. We use our minimization algorithm to show canonicity for transition-based GFG co-Büchi word automata: all minimal automata have isomorphic safe components (namely components obtained by restricting the transitions to these not in $\alpha$) and once we saturate the automata with $\alpha$-transitions, we get full isomorphism.


    Volume: Volume 18, Issue 3
    Published on: August 2, 2022
    Accepted on: June 10, 2022
    Submitted on: June 15, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,F.1.1,F.4.3

    2 Documents citing this article

    Consultation statistics

    This page has been seen 2159 times.
    This article's PDF has been downloaded 666 times.