Practical “Paritizing” of Emerson-Lei Automata

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 $\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 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

• Paper

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