Publication Details

Modular Mix-and-Match Complementation of Büchi Automata

HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata. In: Proceedings of TACAS'23. Paris: Springer Verlag, 2023, pp. 249-270. ISSN 0302-9743.
Czech title
Modulární komplementace Büchiho automatů (technická zpráva)
Type
conference paper
Language
english
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Li Yong (Chinese Academy of Sciences)
Šmahlíková Barbora, Ing. (FIT BUT)
Turrini Andrea (Chinese Academy of Sciences)
Keywords

Büchi automata, omega regular languages, complementation

Abstract

Complementation of nondeterministic Büchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis of programs, model checking, or in decision procedures of some logics. We build on ideas from a recent work on BA determinization by Li et al. and propose a new modular algorithm for BA complementation. Our algorithm allows to combine several BA complementation procedures together, with one procedure for a subset of the BAs strongly connected components (SCCs). In this way, one can exploit the structure of particular SCCs (such as when they are inherently weak or deterministic) and use more efficient specialized algorithms, regardless of the structure of the whole BA. We give a general framework into which partial complementation procedures can be plugged in, and its instantiation with several algorithms. The framework can, in general, produce a complement with an Emerson-Lei acceptance condition, which can often be more compact. Using the algorithm, we were able to establish an exponentially better new upper bound of O(4^n) for complementation of the recently introduced class of elevator automata. We implemented the algorithm in a prototype and performed a comprehensive set of experiments on a large set of benchmarks, showing that our framework complements well the state of the art and that it can serve as a basis for future efficient BA complementation and inclusion checking algorithms.

Published
2023
Pages
249-270
Journal
Lecture Notes in Computer Science, no. 13993, ISSN 0302-9743
Proceedings
Proceedings of TACAS'23
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'23, Paris, FR
Publisher
Springer Verlag
Place
Paris, FR
BibTeX 
@INPROCEEDINGS{FITPUB12921,
   author = "Vojt\v{e}ch Havlena and Ond\v{r}ej Leng\'{a}l and Yong Li and Barbora \v{S}mahl\'{i}kov\'{a} and Andrea Turrini",
   title = "Modular Mix-and-Match Complementation of B{\"{u}}chi Automata",
   pages = "249--270",
   booktitle = "Proceedings of TACAS'23",
   journal = "Lecture Notes in Computer Science",
   number = 13993,
   year = 2023,
   location = "Paris, FR",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12921"
}
Back to top