2013 20th International Symposium on Temporal Representation and Reasoning (TIME) (2013)
Pensacola, FL, USA
Sept. 26, 2013 to Sept. 28, 2013
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2013.20
Marcello M. Bersani , Dipt. di Elettron. Inf. e Bioingegneria, Politec. di Milano, Milan, Italy
Matteo Rossi , Dipt. di Elettron. Inf. e Bioingegneria, Politec. di Milano, Milan, Italy
Pierluigi San Pietro , Dipt. di Elettron. Inf. e Bioingegneria, Politec. di Milano, Milan, Italy
Constraint LTL-over-clocks is a variant of CLTL, an extension of linear-time temporal logic allowing atomic assertions in a concrete constraint system. Satisfiability of CLTL-over-clocks is here shown to be decidable by means of a reduction to a decidable SMT (Satisfiability Modulo Theories) problem. The result is a complete Bounded Satisfiability Checking procedure, which has been implemented by using standard SMT solvers. The importance of this technique derives from the possibility of translating various continuous-time metric temporal logics, such as MITL and QTL, into CLTL-over-clocks itself. Although standard decision procedures of these logics do exist, they have never been realized in practice. Suitable translations into CLTL-over-clocks have instead allowed us the development of the first prototype tool for deciding MITL and QTL. The paper also reports preliminary, but encouraging, experiments on some significant examples of MITL and QTL formulae.
Automata, Cost accounting, Atomic clocks, Standards, Semantics
M. M. Bersani, M. Rossi and P. San Pietro, "A Tool for Deciding the Satisfiability of Continuous-Time Metric Temporal Logic," 2013 20th International Symposium on Temporal Representation and Reasoning (TIME), Pensacola, FL, USA, 2014, pp. 99-106.