Deciding the Satisfiability of MITL Specifications

Preprint English OPEN
Bersani, Marcello Maria; Rossi, Matteo; Pietro, Pierluigi San;
(2013)

In this paper we present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. T... View more
  • References (20)
    20 references, page 1 of 2

    [1] qtlsolver. available from qtlsolver.googlecode.com.

    [2] Zot: a Bounded Satisfiability Checker. available from zot.googlecode.com.

    [3] Rajeev Alur & David L. Dill (1994): A theory of timed automata. Theor. Comp. Sci. 126(2), pp. 183-235. Available at http://dx.doi.org/10.1016/0304-3975(94)90010-8.

    [4] Rajeev Alur, Toma´s Feder & Thomas A. Henzinger (1996): The Benefits of Relaxing Punctuality. Journal of the ACM 43(1), pp. 116-146. Available at http://doi.acm.org/10.1145/112600.112613.

    [5] Christel Baier & Joost-Pieter Katoen (2008): Principles of Model Checking. MIT Press.

    [6] Johan Bengtsson & Wang Yi (2004): Timed Automata: Semantics, Algorithms and Tools. In: Lect. on Concurrency and Petri Nets, LNCS 3098, Springer, pp. 87-124. Available at http://dx.doi.org/10. 1007/978-3-540-27755-2_3.

    [7] Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi & Pierluigi San Pietro (2010): Bounded Reachability for Temporal Logic over Constraint Systems. In: TIME, IEEE Computer Society, pp. 43-50. Available at http://dx.doi.org/10.1109/TIME.2010.21.

    [8] Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi & Pierluigi San Pietro (2012): CLTL Satisfiability Checking without Automata. arXiv:1205.0946v1.

    [9] Marcello M. Bersani, Achille Frigeri, Matteo Rossi & Pierluigi San Pietro (2011): Completeness of the Bounded Satisfiability Problem for Constraint LTL. In: Reachability Problems, LNCS 6945, pp. 58-71. Available at http://dx.doi.org/10.1007/978-3-642-24288-5_7.

    [10] Marcello M. Bersani, Matteo Rossi & Pierluigi San Pietro (2013): A Tool for Deciding the Satisfiability of Continuous-time Metric Temporal Logic. In: Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME). To appear.

  • Metrics
    No metrics available
Share - Bookmark