Temporal logic programming with metric and past operators

Temporal logic allows us to use logic programming to specify and to program dynamically changing situations and non-terminating computations in a natural and problem oriented way. Recently so called metric or real-time temporal logics have been proposed for the specification of real-time systems, for which not only qualitative but also quantitative temporal properties are very important. In this work we investigate a subset of metric temporal Horn logic called MTL-programs, for which we give a translation into CLP(A′)-programs and CLP(A′)-goals over a suitable algebra A′. We give a restriction of the CLP(A′)-derivation mechanism sufficient for the derivation of MTL-goals from MTL-programs, which admits efficient satisfiability checking of the constraints generated. Its worst case complexity is linear in the number of variables involved, contrary to general satisfiability checking of constraints over A′ which is NP-complete. Moreover, we show that an extension of the metric temporal logic considered by the inclusion of variables within the temporal operators leads already to a temporal Horn logic which is expressively equivalent to constraint logic programs over A′.