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 Δp2 -complete.
CITATION STYLE
Laroussinie, F., Markey, N., & Schnoebelen, P. (2001). Model checking CTL+ and FCTL is hard. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2030, pp. 318–331). Springer Verlag. https://doi.org/10.1007/3-540-45315-6_21
Mendeley helps you to discover research relevant for your work.