Difference between revisions of "Publications/renkin.20.atva"
From LRDE
(Created page with "{{Publication | published = true | date = 2020-10-01 | authors = Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet | title = Practical “Paritizing” of Emerson-Lei Aut...") |
|||
| (4 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| published = true |
| published = true |
||
| − | | date = 2020- |
+ | | 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 = |
+ | | 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. |
||
| ⚫ | |||
| + | | 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 |
||
| + | | identifier = doi:10.1007/978-3-030-59152-6_7 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> renkin.20.atva, |
@InProceedings<nowiki>{</nowiki> renkin.20.atva, |
||
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 40: | Line 41: | ||
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> |
||
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}
}