Model Checking Restricted Sets of Timed Paths

In this paper, we study the complexity of model-checking formulas of three important real-time logics (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) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

• Type: Conference
• Year: 2004
• Where: CONCUR
• Authors: Nicolas Markey, Jean-François Raskin
• Keywords: CONCUR 2004, Important Real-time Logics, Infinite Set, Timed Paths