Difference between revisions of "Publications/casares.22.tacas"
From LRDE
(Created page with "{{Publication  published = true  date = 20220201  authors = Antonio Casares, Alexandre DuretLutz, Klara J Meyer, Florian Renkin, Salomon Sickert  title = Practical Appl...") 

Line 6:  Line 6:  
 booktitle = Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 
 booktitle = Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 

 series = Lecture Notes in Computer Science 
 series = Lecture Notes in Computer Science 

+   volume = 13244 

 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 EmersonLei automata, i.e., <math>\omega</math>automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of EmersonLei 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 <math>\omega</math>automata. 
 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 EmersonLei automata, i.e., <math>\omega</math>automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of EmersonLei 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 <math>\omega</math>automata. 

 lrdeprojects = Spot 
 lrdeprojects = Spot 

 lrdenewsdate = 20220201 
 lrdenewsdate = 20220201 

 lrdepaper = https://www.lrde.epita.fr/dload/papers/casares.22.tacas.pdf 
 lrdepaper = https://www.lrde.epita.fr/dload/papers/casares.22.tacas.pdf 

−   
+   pages = 99 to 117 
 type = inproceedings 
 type = inproceedings 

 id = casares.22.tacas 
 id = casares.22.tacas 

+   identifier = doi:10.1007/9783030995270_6 

 bibtex = 
 bibtex = 

@InProceedings<nowiki>{</nowiki> casares.22.tacas, 
@InProceedings<nowiki>{</nowiki> casares.22.tacas, 

Line 24:  Line 26:  
year = <nowiki>{</nowiki>2022<nowiki>}</nowiki>, 
year = <nowiki>{</nowiki>2022<nowiki>}</nowiki>, 

series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, 
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, 

+  volume = <nowiki>{</nowiki>13244<nowiki>}</nowiki>, 

month = apr, 
month = apr, 

abstract = <nowiki>{</nowiki>In 2021, Casares, Colcombet, and Fijalkow introduced the 
abstract = <nowiki>{</nowiki>In 2021, Casares, Colcombet, and Fijalkow introduced the 

Line 42:  Line 45:  
B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi automata, providing a framework of practical 
B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi automata, providing a framework of practical 

algorithms for $\omega$automata.<nowiki>}</nowiki>, 
algorithms for $\omega$automata.<nowiki>}</nowiki>, 

−  +  pages = <nowiki>{</nowiki>99117<nowiki>}</nowiki>, 

+  doi = <nowiki>{</nowiki>10.1007/9783030995270_6<nowiki>}</nowiki> 

<nowiki>}</nowiki> 
<nowiki>}</nowiki> 

Latest revision as of 14:43, 5 April 2022
 Authors
 Antonio Casares, Alexandre DuretLutz, 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
 20220201
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 EmersonLei automata, i.e., automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of EmersonLei 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.
Documents
Bibtex (lrde.bib)
@InProceedings{ casares.22.tacas, author = {Antonio Casares and Alexandre DuretLutz 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 EmersonLei automata, i.e., $\omega$automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of EmersonLei 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 = {99117}, doi = {10.1007/9783030995270_6} }