Minimization and Canonization of GFG Transition-Based Automata
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7587/pdf |
| _version_ | 1797268535769038848 |
|---|---|
| author | Bader Abu Radi Orna Kupferman |
| author_facet | Bader Abu Radi Orna Kupferman |
| author_sort | Bader Abu Radi |
| collection | DOAJ |
| description | 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\"uchi and
co-B\"uchi 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\"uchi 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\"uchi 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. |
| first_indexed | 2024-04-25T01:34:02Z |
| format | Article |
| id | doaj.art-fc1e8b3f68ba4ae3a1b1f992edaea872 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:02Z |
| publishDate | 2022-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-fc1e8b3f68ba4ae3a1b1f992edaea8722024-03-08T10:39:30ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-08-01Volume 18, Issue 310.46298/lmcs-18(3:16)20227587Minimization and Canonization of GFG Transition-Based AutomataBader Abu RadiOrna KupfermanWhile 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\"uchi and co-B\"uchi 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\"uchi 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\"uchi 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.https://lmcs.episciences.org/7587/pdfcomputer science - logic in computer sciencecomputer science - formal languages and automata theoryf.1.1f.4.3 |
| spellingShingle | Bader Abu Radi Orna Kupferman Minimization and Canonization of GFG Transition-Based Automata Logical Methods in Computer Science computer science - logic in computer science computer science - formal languages and automata theory f.1.1 f.4.3 |
| title | Minimization and Canonization of GFG Transition-Based Automata |
| title_full | Minimization and Canonization of GFG Transition-Based Automata |
| title_fullStr | Minimization and Canonization of GFG Transition-Based Automata |
| title_full_unstemmed | Minimization and Canonization of GFG Transition-Based Automata |
| title_short | Minimization and Canonization of GFG Transition-Based Automata |
| title_sort | minimization and canonization of gfg transition based automata |
| topic | computer science - logic in computer science computer science - formal languages and automata theory f.1.1 f.4.3 |
| url | https://lmcs.episciences.org/7587/pdf |
| work_keys_str_mv | AT baderaburadi minimizationandcanonizationofgfgtransitionbasedautomata AT ornakupferman minimizationandcanonizationofgfgtransitionbasedautomata |