Model Checking Games for Branching Time Logics

Martin Lange, Colin Stirling

Research output: Contribution to journalArticlepeer-review


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 important fragments of CTL*. A game based model checking algorithm that matches the known lower and upper complexity bounds is sketched.
Original languageEnglish
Pages (from-to)623-639
Number of pages17
JournalJournal of Logic and Computation
Issue number4
Publication statusPublished - 2002


Dive into the research topics of 'Model Checking Games for Branching Time Logics'. Together they form a unique fingerprint.

Cite this