# Practical “Paritizing” of Emerson-Lei Automata

## Abstract

We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ${\displaystyle \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.

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