Nicolas Markey

Résumé

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 Δ2p-complete.

@inproceedings{fossacs2001-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking {CTL}{\(^+\)} and {FCTL} is hard},
  editor =              {Honsell, Furio and Miculan, Marino},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'01)},
  acronym =             {{FoSSaCS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2030},
  pages =               {318-331},
  year =                {2001},
  month =               apr,
  doi =                 {10.1007/3-540-45315-6_21},
  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
                         \(\Delta_2^p\)-complete.},
}