Practical “Paritizing” of Emerson–Lei Automata
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- 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 {E}merson--{L}ei Automata}, booktitle = {Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20)}, year = {2020}, volume = {12302}, series = {Lecture Notes in Computer Science}, pages = {127--143}, month = oct, publisher = {Springer}, 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.}, doi = {10.1007/978-3-030-59152-6_7} }