Sciweavers

Share
ITA
2007

Three notes on the complexity of model checking fixpoint logic with chop

8 years 10 months ago
Three notes on the complexity of model checking fixpoint logic with chop
Abstract. 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 EXPTIMEcomplete. 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 alternationfree formulas it is P-complete. 1991 Mathematics Subject Classification. 68Q60,68Q17,03B44.
Martin Lange
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where ITA
Authors Martin Lange
Comments (0)
books