Title
Model Checking Games for Branching Time Logics
Abstract
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 optimizations are considered to obtain model checking games for importa...
Year
DOI
Venue
2002
10.1093/logcom/12.4.623
Journal of Logic and Computation
Keywords
Field
DocType
Model checking,games,temporal logics,branching time,CTL*, CTL, CTL+
Computation tree logic,T-norm fuzzy logics,Abstraction model checking,Discrete mathematics,Model checking,Algorithm,Theoretical computer science,Mathematics,Branching (version control)
Journal
Volume
Issue
ISSN
12
4
0955-792X
Citations 
PageRank 
References 
19
0.78
16
Authors
2
Name
Order
Citations
PageRank
Martin Lange144722.83
Colin Stirling2934102.50