# 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 |

## Latest revision as of 10: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.} }