Model Checking Fixed Point Logic with Chop

Martin Lange, Colin Stirling

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


This paper investigates FLC, fixed point logic with chop, which extends modal mu-calculus with a sequential composition operator. We prove some interesting properties of FLC, like the tree model property and bisimulation invariance. Furthermore, we give examples of formulas that cannot be expressed in modal mu-calculus. The main part of the paper deals with FLC's model checking problem. A tableau system is defined and proved sound and complete. It gives rise to an EXPTIME model checking algorithm. It is also shown that FLC model checking can be done in PSPACE for formulas with fixed alternation depth. Finally, the problem is proved to be PSPACE-hard.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Start Conference Manager
Conference Systems