Model Checking Games for the Alternation Free mu-Calculus and Alternating Automata
| Title | Model Checking Games for the Alternation Free mu-Calculus and Alternating Automata |
| Publication Type | Conference Paper |
| Year of Publication | 1999 |
| Authors | Leucker, M |
| Editor | Ganzinger, H, McAllester, D, Voronkov, A |
| Conference Name | Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning "(LPAR'99)" |
| Series | Lecture Notes in Artificial Intelligence |
| Volume | 1705 |
| Publisher | Springer |
| Abstract | We relate game-based model checking and model checking via {\em 1-letter simple weak alternating {B}üchi automata} (1SWABA) for the {\em altern\-ation-free $μ$-calculus}. Game-based algorithms have the advantage that in addition to checking whether a formula is valid or not they determine a winning strategy which can be employed for explaining to the user why the formula is valid or not. 1SWABA are a restricted class of alternating {B}üchi automata and were defined in \cite{BVW94}. They admit efficient automata-based model checking for CTL and the alternation-free $μ$-calculus. We give an interpretation for these automata in terms of game theory and show that this interpretation coincides with the notion of model checking games for CTL and the $μ$-calculus. Then we explain that the efficient non-emptiness procedure for 1SWABA presented in \cite{BVW94} can also be understood as a game-based model checking procedure. Furthermore, we show that this algorithm is not only useful for checking the validity of a formula but also for determining a {\em winning strategy} for the winner of the underlying model checking game. In this way we obtain a linear time algorithm for model checking games. |
| URL | http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/leucker__Games_Automata_mu_calculus.ps.gz |
@inproceedings {L99,
title = {Model Checking Games for the Alternation Free mu-Calculus and Alternating Automata},
booktitle = {Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning "(LPAR{\textquoteright}99)"},
series = {Lecture Notes in Artificial Intelligence},
volume = {1705},
year = {1999},
pages = {77{\textendash}91},
publisher = {Springer},
organization = {Springer},
abstract = {We relate game-based model checking and model checking via {\em 1-letter simple weak alternating {B}{\"u}chi automata} (1SWABA) for the {\em altern\-ation-free $μ$-calculus}. Game-based algorithms have the advantage that in addition to checking whether a formula is valid or not they determine a winning strategy which can be employed for explaining to the user why the formula is valid or not. 1SWABA are a restricted class of alternating {B}{\"u}chi automata and were defined in \cite{BVW94}. They admit efficient automata-based model checking for CTL and the alternation-free $μ$-calculus. We give an interpretation for these automata in terms of game theory and show that this interpretation coincides with the notion of model checking games for CTL and the $μ$-calculus. Then we explain that the efficient non-emptiness procedure for 1SWABA presented in \cite{BVW94} can also be understood as a game-based model checking procedure. Furthermore, we show that this algorithm is not only useful for checking the validity of a formula but also for determining a {\em winning strategy} for the winner of the underlying model checking game. In this way we obtain a linear time algorithm for model checking games.},
url = {http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/leucker__Games_Automata_mu_calculus.ps.gz},
author = {Martin Leucker},
editor = {Harald Ganzinger and David McAllester and Andrei Voronkov}
}