Decidability results for metric and layered temporal logics (Q1815429)

The decidability problem for metric and layered temporal logics (MLTL for short) is studied. Metric temporal logics extend propositional logic with a parametrized operator of relative temporal realization. MLTL can be viewed as the combination of a number of differently grained metric temporal logics. It replaces the flat temporal domain of metric temporal logics with a temporal universe consisting of a set of differently grained temporal domains together with relations between instants belonging to different domains. The decidability of MLTL is studied by embedding finitely layered metric temporal structures into their finest metric component, and then reducing the decidability of the theory of the simplest component to a theory that is known to be decidable, namely S1S (the second-order theory of one successor).