Reasoning About Regular Properties: A Comparative Study

被引:2
作者
Fiedor, Tomas [1 ]
Holik, Lukas [1 ]
Hruska, Martin [1 ]
Rogalewicz, Adam [1 ]
Sic, Juraj [1 ]
Vargovcik, Pavol [1 ]
机构
[1] Brno Univ Technol, Brno, Czech Republic
来源
AUTOMATED DEDUCTION, CADE 29 | 2023年 / 14132卷
关键词
FINITE; CHECKING; AUTOMATA; UNIVERSALITY; MINIMIZATION; ANTICHAINS; INCLUSION; DESIGN;
D O I
10.1007/978-3-031-38499-8_17
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:286 / 306
页数:21
相关论文
共 82 条
[11]  
Boudet A., 1996, Trees in Algebra and Programming - CAAP '96. 21st International Colloquium. Proceedings, P30
[12]   Formal Design and Safety Analysis of AIR6110 Wheel Brake System [J].
Bozzano, M. ;
Cimatti, A. ;
Pires, A. Fernandes ;
Jones, D. ;
Kimberly, G. ;
Petri, T. ;
Robinson, R. ;
Tonetta, S. .
COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 :518-535
[13]  
Bradley A., 2015, IC3 reference implementation: a short, simple, fairly competitive implementation of IC3
[14]  
Bradley AR, 2007, FMCAD 2007: FORMAL METHODS IN COMPUTER AIDED DESIGN, PROCEEDINGS, P173, DOI 10.1109/.15
[15]  
Brayton R, 2010, LECT NOTES COMPUT SC, V6174, P24, DOI 10.1007/978-3-642-14295-6_5
[16]  
Brzozowski J.A, 1962, P S MATH THEORY AUTO
[17]  
BRZOZOWSKI JA, 1980, THEOR COMPUT SCI, V10, P19, DOI 10.1016/0304-3975(80)90069-9
[18]  
Buchi J.R, 1962, P INT C LOGIC METHOD
[19]  
Buchi J.R., 1990, Weak Second-Order Arithmetic and Finite Automata, P398, DOI DOI 10.1007/978-1-4613-8928-622
[20]  
Cavada R, 2014, LECT NOTES COMPUT SC, V8559, P334, DOI 10.1007/978-3-319-08867-9_22