Local Model Checking Games for Fixed Point Logic with Chop

Abstract

The logic considered in this paper is FLC, fixed point logic with chop. It is an extension of modal μ-calculus L _μ that is capable of defining non-regular properties which makes it interesting for verification purposes. Its model checking problem over finite transition systems is PSPACE-hard. 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 on-the- fly. On formulas with fixed alternation depth and so-called sequential depth deciding the winner of the games is PSPACE-complete. 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 L_μ formulas the games behave equally well as the model checking games for L_μ, i.e. deciding the winner is in NP蝅co-NP.