Model Checking Timeline-based Systems over Dense Temporal Domains?

In this paper, we introduce an automaton-theoretic approach to model checking linear time properties of timeline-based systems over dense temporal domains. The system under consideration is specified by means of (a decidable fragment of) timeline structures, timelines for short, which are a formal setting proposed in the literature to model planning problems in a declarative way. Timelines provide an interval-based description of the behavior of the system, instead of a more conventional point-based one. The relevant system properties are expressed by formulas of the logic MITL (a well-known timed extension of LTL) to be checked against timelines. In the paper, we prove that the model checking problem for MITL formulas (resp., its fragment MITL(0,∞)) over timelines is EXPSPACE-complete (resp., PSPACE-complete).