Selective Approaches for Solving Weak Games

Abstract. 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.

• Type: Conference
• Year: 2006
• Where: ATVA
• Authors: Malte Helmert, Robert Mattmüller, Sven Schewe
• Keywords: Alternating-time Temporal Logic, ATVA 2006, Hardware, Model-checking Alternating-time Properties, Practical ATL