Difference between revisions of "Publications/casares.22.tacas"
From LRDE
(Created page with "{{Publication | published = true | date = 2022-02-01 | authors = Antonio Casares, Alexandre Duret-Lutz, Klara J Meyer, Florian Renkin, Salomon Sickert | title = Practical Appl...") |
|||
(One intermediate revision by the same user not shown) | |||
Line 4: | Line 4: | ||
| authors = Antonio Casares, Alexandre Duret-Lutz, Klara J Meyer, Florian Renkin, Salomon Sickert |
| authors = Antonio Casares, Alexandre Duret-Lutz, Klara J Meyer, Florian Renkin, Salomon Sickert |
||
| title = Practical Applications of the Alternating Cycle Decomposition |
| title = Practical Applications of the Alternating Cycle Decomposition |
||
− | | 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 (TACAS'22) |
| 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 Emerson-Lei automata, i.e., <math>\omega</math>-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 <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 Emerson-Lei automata, i.e., <math>\omega</math>-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 <math>\omega</math>-automata. |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2022-02-01 |
| lrdenewsdate = 2022-02-01 |
||
| 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/978-3-030-99527-0_6 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> casares.22.tacas, |
@InProceedings<nowiki>{</nowiki> casares.22.tacas, |
||
Line 20: | Line 22: | ||
<nowiki>{</nowiki>D<nowiki>}</nowiki>ecomposition<nowiki>}</nowiki>, |
<nowiki>{</nowiki>D<nowiki>}</nowiki>ecomposition<nowiki>}</nowiki>, |
||
booktitle = <nowiki>{</nowiki>Proceedings of the 28th International Conference on Tools |
booktitle = <nowiki>{</nowiki>Proceedings of the 28th International Conference on Tools |
||
− | and Algorithms for the Construction and Analysis of |
+ | and Algorithms for the Construction and Analysis of Systems |
− | + | (TACAS'22)<nowiki>}</nowiki>, |
|
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>99--117<nowiki>}</nowiki>, |
|
+ | doi = <nowiki>{</nowiki>10.1007/978-3-030-99527-0_6<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 18:52, 10 March 2023
- 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 (TACAS'22)
- 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., -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.
Documents
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 (TACAS'22)}, 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} }