DROPS

Artifact

Software

VeriFIT/kofola

Authors: Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi

Abstract

Cite as

Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, Nicolas Mazzocchi. VeriFIT/kofola (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27641,
   title = {{VeriFIT/kofola}}, 
   author = {Alexaj, Ondrej and Havlena, Vojt\v{e}ch and Leng\'{a}l, Ond\v{r}ej and Li, Yong and Mazzocchi, Nicolas},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:16f5c469b77f8e8488673e13345e75955093f282;origin=https://github.com/VeriFIT/kofola;visit=swh:1:snp:d50f929a4280f72180b38e1e5a749a39e7182a4a;anchor=swh:1:rev:f916ecc579fa2eeb858211545936d51e9a088d3e}{\texttt{swh:1:dir:16f5c469b77f8e8488673e13345e75955093f282}} (visited on 2026-08-24)},
   url = {https://github.com/VeriFIT/kofola},
   doi = {10.4230/artifacts.27641},
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.8

Complementing Emerson-Lei Elevator Automata

Authors: Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract

Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected component is either deterministic or inherently weak. It was shown that this class contains the majority of Büchi automata generated in practical applications, including LTL model-checking and verification of hyperproperties. Moreover, the elevator subclass enables more efficient complementation and determinization algorithms than unrestricted Büchi automata. In this paper, we introduce Emerson-Lei elevator automata, which is a generalization of Büchi elevator automata to richer acceptance conditions. We provide a complementation algorithm with a significantly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata. The practical efficiency of our algorithm is demonstrated by an experimental comparison with the popular state-of-the-art tool Spot. Our work is, to the best of our knowledge, the first step towards practical algorithms for complementing, determinizing, and testing universality and inclusion of Emerson-Lei automata with rich acceptance conditions.

Cite as

Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi. Complementing Emerson-Lei Elevator Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{alexaj_et_al:LIPIcs.CONCUR.2026.8,
  author =	{Alexaj, Ondrej and Havlena, Vojt\v{e}ch and Leng\'{a}l, Ond\v{r}ej and Li, Yong and Mazzocchi, Nicolas},
  title =	{{Complementing Emerson-Lei Elevator Automata}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{8:1--8:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.8},
  URN =		{urn:nbn:de:0030-drops-273390},
  doi =		{10.4230/LIPIcs.CONCUR.2026.8},
  annote =	{Keywords: Emerson-Lei elevator automata, complementation, elevator automata, omega automata, infinite words, omega-regular languages}
}

Search Results

Documents authored by Alexaj, Ondrej

VeriFIT/kofola

Abstract

Cite as

Complementing Emerson-Lei Elevator Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message