Practical “Paritizing” of Emerson–Lei Automata

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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