Nicolas Markey

Résumé

We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied.

We exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).

Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes Δ2P-complete or PSPACE-complete depending on the considered semantics.

@article{tcs353(1-3)-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Efficient timed model checking for discrete-time
                         systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {353},
  number =              {1-3},
  pages =               {249-271},
  year =                {2006},
  month =               mar,
  doi =                 {10.1016/j.tcs.2005.11.020},
  abstract =            {We consider model checking of timed temporal
                         formulae in \emph{durational transition graphs}
                         (DTGs), \emph{i.e.}, Kripke structures where
                         transitions have integer durations. Two semantics
                         for DTGs are presented and motivated. We consider
                         timed versions of CTL where subscripts put
                         quantitative constraints on the time it takes before
                         a property is satisfied. \par We exhibit an
                         important gap between logics where subscripts of the
                         form {"}\(= c\){"} (exact duration) are allowed, and
                         simpler logics that only allow subscripts of the
                         form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded
                         duration).\par Without exact durations, model
                         checking can be done in polynomial time, but with
                         exact durations, it becomes
                         \(\Delta_{2}^{P}\)-complete or PSPACE-complete
                         depending on the considered semantics.},
}