Model checking CTL+ and FCTL is hard

43Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

This article is free to access.

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 Δp2 -complete.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free