We are happy to announce that the following article has been accepted
to the 28th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'22) to be held in Munich
in April 2022.
======================================================================
Practical Applications of the Alternating Cycle Decomposition
Antonio Casares¹, Alexandre Duret-Lutz², Klara J. Meyer³,
Florian Renkin², and Salomon Sickert⁴
¹LaBRI, Universitée de Bordeaux, France
²LRDE, EPITA, France
³Independent Researcher
⁴School of Computer Science and Engineering, The Hebrew Univ., Israel
In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating
Cycle Decomposition (ACD) to study properties and transformations of
Muller automata. We present the first practical implementation of the
ACD in two different tools, Owl and Spot, and adapt it to the
framework of Emerson-Lei automata, i.e., ω-automata whose acceptance
conditions are defined by Boolean formulas. The ACD provides a
transformation of Emerson-Lei automata into parity automata with
strong optimality guarantees: the resulting parity automaton is
minimal among those automata that can be obtained by duplication of
states. Our empirical results show that this transformation is usable
in practice. Further, we show how the ACD can generalize many other
specialized constructions such as deciding typeness of automata and
degeneralization of generalized Büchi automata, providing a framework
of practical algorithms for ω-automata.
https://www.lrde.epita.fr/wiki/Publications/casares.22.tacas
======================================================================
