Three notes on the complexity of model checking fixpoint logic with chop
Department of Computer Science, University of Munich, Oettingenstr. 67, 80538 München, Germany; Martin.Lange@ifi.lmu.de
Accepted: 18 August 2006
This paper analyses the complexity of model checking fixpoint logic with Chop – an extension of the modal μ-calculus with a sequential composition operator. It uses two known game-based characterisations to derive the following results: the combined model checking complexity as well as the data complexity of FLC are EXPTIME-complete. This is already the case for its alternation-free fragment. The expression complexity of FLC is trivially P-hard and limited from above by the complexity of solving a parity game, i.e. in UP ∩ co-UP. For any fragment of fixed alternation depth, in particular alternation- free formulas it is P-complete.
Mathematics Subject Classification: 03B44 / 68Q17 / 68Q60
Key words: Model checking / games / EXPTIME-complete
© EDP Sciences, 2007