zbMATH — the first resource for mathematics

Model checking fixed point logic with chop. (English) Zbl 1077.68690
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 250-263 (2002).
Summary: This paper examines FLC, which is the modal \(\mu\)-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal \(\mu\)-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.
For the entire collection see [Zbl 0989.00051].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: Link