Practical Applications of the Alternating Cycle Decomposition

Authors

Antonio Casares, Alexandre Duret-Lutz, Klara J Meyer, Florian Renkin, Salomon Sickert

Where

Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Type

inproceedings

Projects

Spot

Date

2022-02-01

Abstract

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., $\omega$-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 $\omega$-automata.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  casares.22.tacas,
  author	= {Antonio Casares and Alexandre Duret-Lutz and Klara J.
		  Meyer and Florian Renkin and Salomon Sickert},
  title		= {Practical Applications of the {A}lternating {C}ycle
		  {D}ecomposition},
  booktitle	= {Proceedings of the 28th International Conference on Tools
		  and Algorithms for the Construction and Analysis of
		  Systems},
  year		= {2022},
  series	= {Lecture Notes in Computer Science},
  volume	= {13244},
  month		= apr,
  abstract	= {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., $\omega$-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{\"u}chi automata, providing a framework of practical
		  algorithms for $\omega$-automata.},
  pages		= {99--117},
  doi		= {10.1007/978-3-030-99527-0_6}
}