Sciweavers

LOGCOM
2002

Model Checking Games for Branching Time Logics

13 years 10 months ago
Model Checking Games for Branching Time Logics
This paper defines and examines model checking games for the branching time temporal logic CTL . The games employ a technique called focus which enriches sets by picking out one distinguished element. This is necessary to avoid ambiguities in the regeneration of temporal operators. The correctness of these games is proved, and optimisations are considered to obtain model checking games for important fragments of CTL . A game based model checking algorithm that matches the known lower and upper complexity bounds is sketched.
Martin Lange, Colin Stirling
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 2002
Where LOGCOM
Authors Martin Lange, Colin Stirling
Comments (0)