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...") |
|||
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 Emerson-Lei Automata |
| title = Practical “Paritizing” of Emerson-Lei Automata |
||
Line 8: | Line 8: | ||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
| pages = ??? to ??? |
| pages = ??? to ??? |
||
− | | lrdeprojects = Spot |
||
| 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 |
||
+ | | lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf |
||
| type = inproceedings |
| type = inproceedings |
||
| id = renkin.20.atva |
| id = renkin.20.atva |
Revision as of 10:35, 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
- 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. lrdekeywords = Spot
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.} }