Model Checking CTL+ and FCTL is Hard

Abstract. Among the branching-time temporal logics used for the specification and verification of systems, CTL+ , FCTL and ECTL+ are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is ∆p 2-complete.

• Type: Conference
• Year: 2001
• Where: FOSSACS
• Authors: François Laroussinie, Nicolas Markey, Ph. Schnoebelen
• Keywords: Branching-time Temporal Logics, FOSSACS 2001, Model Checking, Notable Logics, Software Engineering