Model checking fixed point logic with chop

Abstract

This paper examines FLC, which is the modal μ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal μ-calculus. The main focus lies on FLC’s model checking problem over finite transition systems. It is proved to be PSPACE-hard. A tableau model checker is given and an upper EXPTIME bound is derived from it. For a fixed alternation depth FLC’s model checking problem turns out to be PSPACE-complete. © Springer-Verlag Berlin Heidelberg 2002.