[Lrde Annonce] New publication: Practical “paritizing” of Emerson-Lei automata

I am happy to announce that the following paper has been accepted at the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20) Practical "paritizing" of Emerson-Lei automata Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet https://www.lrde.epita.fr/wiki/Publications/renkin.20.atva [1] 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 latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. -- Florian Renkin Links: ------ [1] https://www.lrde.epita.fr/wiki/Publications/blahoudek.20.atva