Generic Model Checking for Modal Fixpoint Logics in COOL-MC

被引:1
作者
Hausmann, Daniel [1 ]
Humml, Merlin [2 ]
Prucker, Simon [2 ]
Schroeder, Lutz [2 ]
Strahlberger, Aaron [2 ]
机构
[1] Univ Gothenburg, Gothenburg, Sweden
[2] Friedrich Alexander Univ Erlangen Nurnberg, Erlangen, Germany
来源
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT I | 2024年 / 14499卷
关键词
Model checking; parity games; mu-calculus; lazy evaluation;
D O I
10.1007/978-3-031-50524-9_8
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (nondeterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal mu-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the mu-calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets.
引用
收藏
页码:171 / 185
页数:15
相关论文
共 39 条
[21]  
Hausmann D, 2023, Arxiv, DOI [arXiv:2311.01315, 10.48550/arXiv.2311.01315, DOI 10.48550/ARXIV.2311.01315]
[22]  
Hausmann D, 2024, Arxiv, DOI [arXiv:2212.11055, 10.48550/arXiv.2212.11055, DOI 10.48550/ARXIV.2212.11055]
[23]   Quasipolynomial Computation of Nested Fixpoints [J].
Hausmann, Daniel ;
Schroeder, Lutz .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2021, 2021, 12651 :38-56
[24]  
Kański M, 2021, Studia Informatica System and information technology, DOI [10.34739/si.2021.25.01, 10.34739/si.2021.25.01, DOI 10.34739/SI.2021.25.01]
[25]   RESULTS ON THE PROPOSITIONAL MU-CALCULUS [J].
KOZEN, D .
THEORETICAL COMPUTER SCIENCE, 1983, 27 (03) :333-354
[26]  
Kupferman O., 2002, Automated Deduction, CADE 2002, V2392, P423, DOI [DOI 10.1007/3-540-45620-1_34, 10.1007/3-540-45620-134, DOI 10.1007/3-540-45620-134]
[27]  
Kupke C., 2022, Logic in Computer Science, DOI DOI 10.1145/3531130.3533339
[28]  
Kwiatkowska Marta, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P585, DOI 10.1007/978-3-642-22110-1_47
[29]  
Landsaat E., 2022, A model checker for game logic via parity games
[30]  
Liu WW, 2015, PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), P882