Nicolas Markey

Abstract

In this paper, we study the complexity of model-checking formulas of four important real-time logics (TPTL, MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

Several results are quite negative: TPTL and MTL remain undecidable along region- and zone-paths. On the other hand, we obtained PTIME algorithms for model checking TCTL along a region path, and for MTL along a single timed path.

@article{tcs358(2-3)-MR,
  author =              {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Model Checking Restricted Sets of Timed Paths},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {358},
  number =              {2-3},
  pages =               {273-292},
  year =                {2006},
  month =               aug,
  doi =                 {10.1016/j.tcs.2006.01.019},
  abstract =            {In this paper, we study the complexity of
                         model-checking formulas of four important real-time
                         logics (TPTL, MTL, MITL, and TCTL) over restricted
                         sets of timed paths. The classes of restricted sets
                         of timed paths that we consider are
                         \textit{(i)}~a~single finite (or ultimately
                         periodic) timed path, \textit{(ii)}~an~infinite set
                         of finite (or infinite) timed paths defined by a
                         finite (or ultimately periodic) path in a region
                         graph, \textit{(iii)}~an~infinite set of finite (or
                         infinite) timed paths defined by a finite (or
                         ultimately periodic) path in a zone graph. \par
                         Several results are quite negative: TPTL and MTL
                         remain undecidable along region- and zone-paths. On
                         the other hand, we obtained PTIME algorithms for
                         model checking TCTL along a region path, and for MTL
                         along a single timed path.},
}