Local Model Checking Games for Fixed Point Logic with Chop Martin Lange
The logic considered in this paper is FLC, fixed point logic with
chop. It is an extension of modal mucalculus MMC that is capable of
defining nonregular properties which makes it interesting for
verification purposes. Its model checking problem over finite
transition systems is PSPACEhard. We define games that characterise
FLC's model checking problem over arbitrary transition systems. Over
finite transition systems they can be used as a basis of a local model
checker for FLC. I.e. the games allow the transition system to be
constructed onthefly. On formulas with fixed alternation depth and
socalled sequential depth deciding the winner of the games is
PSPACEcomplete. The best upper bound for the general case is
EXPSPACE which can be improved to EXPTIME at the cost of losing the
locality property. On modal mucalculus formulas the games behave
equally well as the model checking games for MMC, i.e. deciding the
winner is in NP intersect coNP.

concur02@fi.muni.cz 