Publication Details

Reasoning about Regular Properties: A Comparative Study

HOLÍK, L.; HRUŠKA, M.; SÍČ, J.; VARGOVČÍK, P.; FIEDOR, T.; ROGALEWICZ, A. Reasoning about Regular Properties: A Comparative Study. In Automated Deduction - CADE 29. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2023. p. 286-306. ISSN: 0302-9743.
Czech title
Uvažování o regulárních vlastnostech: Srovnávací studie
Type
conference paper
Language
English
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Hruška Martin, Ing., Ph.D. (Automata@FIT)
Síč Juraj, Mgr. (DITS)
Vargovčík Pavol, Ing. (DITS)
Fiedor Tomáš, Ing., Ph.D. (RG VERIFIT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Keywords

Regular languages, finite automata, nondeterministic finite automata, tool
comparison.

Abstract

Several new algorithms for deciding emptiness of Boolean combinations of regular
languages and of languages of alternating automata have been proposed recently,
especially in the context of analysing regular expressions and in string
constraint solving. The new algorithms demonstrated a significant potential, but
they have never been systematically compared, neither among each other nor with
the state-of-the art implementations of existing (non)deterministic
automata-based methods. In this paper, we provide such comparison as well as an
overview of the existing algorithms and their implementations. We collect
a diverse benchmark mostly originating in or related to practical problems from
string constraint solving, analysing LTL properties, and regular model checking,
and evaluate collected implementations on it. The results reveal the best tools
and hint on what the best algorithms and implementation techniques are. Roughly,
although some advanced algorithms are fast, such as antichain algorithms and
reductions to IC3/PDR, they are not as overwhelmingly dominant as sometimes
presented and there is no clear winner. The simplest NFA-based technology may
sometimes be a better choice, depending on the problem source and the
implementation style. We believe that our findings are relevant for development
of automata techniques as well as for related fields such as string constraint
solving.

Published
2023
Pages
286–306
Journal
Lecture Notes in Computer Science, no. 14132, ISSN 0302-9743
Proceedings
Automated Deduction - CADE 29
Conference
29th International Conference on Automated Deduction, Rome, IT
Publisher
Springer Nature Switzerland AG
Place
Cham
DOI
10.1007/978-3-031-38499-8_17
UT WoS
001156342400017
EID Scopus
2-s2.0-85172215435
BibTeX 
@inproceedings{BUT185181,
  author="Lukáš {Holík} and Martin {Hruška} and Juraj {Síč} and Pavol {Vargovčík} and Tomáš {Fiedor} and Adam {Rogalewicz}",
  title="Reasoning about Regular Properties: A Comparative Study",
  booktitle="Automated Deduction - CADE 29",
  year="2023",
  journal="Lecture Notes in Computer Science",
  number="14132",
  pages="286--306",
  publisher="Springer Nature Switzerland AG",
  address="Cham",
  doi="10.1007/978-3-031-38499-8\{_}17",
  issn="0302-9743"
}
Back to top