Difference between revisions of "Publications/renkin.20.atva"
From LRDE
| Line 3: | Line 3: | ||
| date = 2020-07-07 |
| date = 2020-07-07 |
||
| authors = Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet |
| authors = Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet |
||
| − | | title = Practical “Paritizing” of |
+ | | title = Practical “Paritizing” of Emerson–Lei Automata |
| booktitle = Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20) |
| booktitle = Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20) |
||
| volume = 12302 |
| volume = 12302 |
||
| Line 20: | Line 20: | ||
author = <nowiki>{</nowiki>Florian Renkin and Alexandre Duret-Lutz and Adrien |
author = <nowiki>{</nowiki>Florian Renkin and Alexandre Duret-Lutz and Adrien |
||
Pommellet<nowiki>}</nowiki>, |
Pommellet<nowiki>}</nowiki>, |
||
| − | title = <nowiki>{</nowiki>Practical ``Paritizing'' of <nowiki>{</nowiki>E<nowiki>}</nowiki>merson-<nowiki>{</nowiki>L<nowiki>}</nowiki>ei Automata<nowiki>}</nowiki>, |
+ | title = <nowiki>{</nowiki>Practical ``Paritizing'' of <nowiki>{</nowiki>E<nowiki>}</nowiki>merson--<nowiki>{</nowiki>L<nowiki>}</nowiki>ei Automata<nowiki>}</nowiki>, |
booktitle = <nowiki>{</nowiki>Proceedings of the 18th International Symposium on |
booktitle = <nowiki>{</nowiki>Proceedings of the 18th International Symposium on |
||
Automated Technology for Verification and Analysis |
Automated Technology for Verification and Analysis |
||
Latest revision as of 09:58, 5 November 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 {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}
}