Local Model Checking Games for Fixed Point Logic with Chop

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