Model checking \(\text{CTL}^+\) and FCTL is hard. (English) Zbl 0986.68067
Honsell, Furio (ed.) et al., Foundations of software science and computation structures. 4th international conference, FOSSACS 2001, held as part of the joint European conferences on theory and practice of software, ETAPS 2001, Genova, Italy, April 2-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2030, 318-331 (2001).
Summary: 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 complete.
For the entire collection see [Zbl 0960.00057].
For the entire collection see [Zbl 0960.00057].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68N17 | Logic programming |
