Selective Approaches for Solving Weak Games
Malte Helmert, Robert Mattmüller, and Sven Schewe
Model-checking alternating-time properties has recently attracted much interest in the verification of distributed protocols. While checking the validity of a specification in alternating-time temporal logic (ATL) against an explicit model is cheap (linear in the size of the formula and the model), the problem becomes EXPTIME-hard when symbolic models are considered. Practical ATL model-checking therefore often consumes too much computation time to be tractable.
In this paper, we describe a novel approach for ATL model-checking, which constructs an explicit weak model-checking game on-the-fly. This game is then evaluated using heuristic techniques inspired by efficient evaluation algorithms for and/or-trees.
To show the feasibility of our approach, we compare its performance to the ATL model-checking system MOCHA on some practical examples. Using very limited heuristic guidance, we achieve a significant speedup on these benchmarks.
4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006).