Abstract:

We present a dense timed interval temporal logic (DTITL) and exploit the decidability problem of DTITL. To do so, we define an equivalence relation with finite equivalence classes over state spaces of DTITL models. Using the equivalence relation, we can construct a discrete model of a subset of the first order interval temporal logic called SFO from a continuous DTITL model. A set of rules are also applied to construct SFO formulas from DTITL ones. Then the satisfiability of DTITL is equivalently transformed to the same problem for SFO. Since the decidability of SFO can be transformed to the satisfiability of the propositional interval temporal logic, so SFO is decidable. Thus, the satisfiability of DTITL can be proved to be decidable.

Key words: real time systems, temporal logic, model checking, hybrid systems