Difference between revisions of "Publications/renkin.20.atva"
From LRDE
Line 5: | Line 5: | ||
| title = Practical “Paritizing” of Emerson-Lei Automata |
| 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 = |
+ | | volume = 12302 |
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
− | | pages = |
+ | | pages = 127 to 143 |
| publisher = Springer |
| publisher = Springer |
||
− | | 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 |
| lrdekeywords = Spot |
||
| lrdenewsdate = 2020-07-07 |
| lrdenewsdate = 2020-07-07 |
||
− | | lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf |
||
| type = inproceedings |
| type = inproceedings |
||
| id = renkin.20.atva |
| id = renkin.20.atva |
||
Line 20: | Line 18: | ||
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 |
+ | 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 |
||
(ATVA'20)<nowiki>}</nowiki>, |
(ATVA'20)<nowiki>}</nowiki>, |
||
year = <nowiki>{</nowiki>2020<nowiki>}</nowiki>, |
year = <nowiki>{</nowiki>2020<nowiki>}</nowiki>, |
||
− | volume = <nowiki>{</nowiki> |
+ | volume = <nowiki>{</nowiki>12302<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
− | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>127--143<nowiki>}</nowiki>, |
month = oct, |
month = oct, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
⚫ | |||
abstract = <nowiki>{</nowiki>We introduce a new algorithm that takes a |
abstract = <nowiki>{</nowiki>We introduce a new algorithm that takes a |
||
\emph<nowiki>{</nowiki>Transition-based Emerson-Lei Automaton<nowiki>}</nowiki> (TELA), that |
\emph<nowiki>{</nowiki>Transition-based Emerson-Lei Automaton<nowiki>}</nowiki> (TELA), that |
||
Line 42: | Line 39: | ||
degeneralization<nowiki>}</nowiki>. Our motivation is to use this algorithm |
degeneralization<nowiki>}</nowiki>. Our motivation is to use this algorithm |
||
to improve our LTL synthesis tool, where producing |
to improve our LTL synthesis tool, where producing |
||
− | deterministic parity automata is an intermediate step.<nowiki>}</nowiki> |
+ | deterministic parity automata is an intermediate step.<nowiki>}</nowiki>, |
⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 15:19, 4 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.
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} }