Nicolas Markey

Abstract

We consider the problem of checking whether a finite (or ultimately periodic) run satisfies a temporal logic formula. This problem is at the heart of "runtime verification" but it also appears in many other situations. By considering several extended temporal logics, we show that the problem of model checking a path can usually be solved efficiently, and profit from specialized algorithms. We further show it is possible to efficiently check paths given in compressed form.

@inproceedings{concur2003-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking a Path (Preliminary Report)},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {251-265},
  year =                {2003},
  month =               aug,
  doi =                 {10.1007/978-3-540-45187-7_17},
  abstract =            {We consider the problem of checking whether a finite
                         (or ultimately periodic) run satisfies a temporal
                         logic formula. This problem is at the heart of
                         {"}runtime verification{"} but it also appears in
                         many other situations. By considering several
                         extended temporal logics, we show that the problem
                         of model checking a path can usually be solved
                         efficiently, and profit from specialized algorithms.
                         We further show it is possible to efficiently check
                         paths given in compressed form.},
}