Paper Details

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 mu-calculus MMC 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 modal mu-calculus formulas the games behave equally well as the model checking games for MMC, i.e. deciding the winner is in NP intersect co-NP.