2-SORTED METRIC TEMPORAL LOGICS

Temporal logic has been successfully used for modeling and analyzing t he behavior of reactive and concurrent systems. Standard temporal logi c is inadequate for real-time applications because it only deals with qualitative timing properties. This is overcome by metric temporal log ics which offer a uniform logical framework in which both qualitative and quantitative timing properties can be expressed by making use of a parameterized operator of relative temporal realization. In this pape r we deal with completeness issues for basic systems of metric tempora l logic despite their relevance, such issues have been ignored or only partially addressed in the literature. We view metric temporal logics as two-sorted formalisms having formulae ranging over time instants a nd parameters ranging over an (ordered) abelian group of temporal disp lacements. We first provide an axiomatization of the pure metric fragm ent of the logic, and prove its soundness and completeness. Then, we s how how to obtain the metric temporal logic of linear orders by adding an ordering over displacements. Finally, we consider general metric t emporal logics allowing quantification over algebraic variables and fr ee mixing of algebraic formulae and temporal propositional symbols.