Model Checking a Path

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.

• Type: Conference
• Year: 2003
• Where: CONCUR
• Authors: Nicolas Markey, Ph. Schnoebelen
• Keywords: CONCUR 2003, Extended Temporal Logics, Temporal Logic Formula, Temporal Logics