*Semantics Club 31 08 2001*

# Model Checking Modal Mu-Calculus with Sequential Composition

(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.