Sciweavers

Share
ATVA
2006
Springer

Selective Approaches for Solving Weak Games

9 years 3 months ago
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.
Malte Helmert, Robert Mattmüller, Sven Schewe
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Malte Helmert, Robert Mattmüller, Sven Schewe
Comments (0)
books