Practical “Paritizing” of Emerson-Lei Automata

From LRDE

Revision as of 10:41, 7 July 2020 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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