Difference between revisions of "Publications/renkin.20.atva"
From LRDE
Line 10: | Line 10: | ||
| publisher = Springer |
| publisher = Springer |
||
| note = To appear |
| note = To appear |
||
− | | abstract = We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an <math>\omega</math>-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a emphlatest appearance record principle, and introduces a emphpartial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. |
+ | | abstract = We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an <math>\omega</math>-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a emphlatest appearance record principle, and introduces a emphpartial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. |
+ | | lrdekeywords = Spot |
||
| lrdenewsdate = 2020-07-07 |
| lrdenewsdate = 2020-07-07 |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf |
Revision as of 09:41, 7 July 2020
- Authors
- Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet
- Where
- Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20)
- Type
- inproceedings
- Publisher
- Springer
- Keywords
- Spot
- Date
- 2020-07-07
Abstract
We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an -automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a emphlatest appearance record principle, and introduces a emphpartial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.
Documents
Bibtex (lrde.bib)
@InProceedings{ renkin.20.atva, author = {Florian Renkin and Alexandre Duret-Lutz and Adrien Pommellet}, title = {Practical ``Paritizing'' of Emerson-Lei Automata}, booktitle = {Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20)}, year = {2020}, volume = {?????}, series = {Lecture Notes in Computer Science}, pages = {???--???}, month = oct, publisher = {Springer}, note = {To appear}, abstract = {We introduce a new algorithm that takes a \emph{Transition-based Emerson-Lei Automaton} (TELA), that is, an $\omega$-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a \emph{Transition-based Parity Automaton} (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a \emph{latest appearance record} principle, and introduces a \emph{partial degeneralization}. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.} }