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.
|
concur02@fi.muni.cz |