Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 4, August 2002: pp. 623-639

Model Checking Games for Branching Time Logics

Martin Lange1 and Colin Stirling1

1LFCS, Division of Informatics, The University of Edinburgh, Scotland. E-mail: {martin,cps}@dcs.ed.ac.uk

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.

Keywords: Model checking; games; temporal logics; branching time; CTL*; CTL; CTL+

Table of Contents   Full-Text PDF (171 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement