Semantics Club 31 08 2001

Model Checking Modal Mu-Calculus with Sequential Composition

Martin Lange

(joint work with Colin Stirling)

Abstract

In this talk we present FLC which is modal mu-calculus enriched with a sequential composition operator. This temporal logic was introduced by Markus Mueller-Olm in 1999. It has been known so far that FLC is undecidable whereas its model checking problem is trivially seen to be decidable. We will prove that the latter is at least PSPACE-hard and at most in EXPTIME, thus showing that its increased expressive power compared to modal mu-calculus does not come for free. PSPACE-hardness is established by reduction from QBF. To show membership in EXPTIME we present a tableau proof system that gives rise to an alternating PSPACE algorithm. We will conclude by discussing a few ideas on how to improve the complexity bounds.