References

1. qtlsolver. available from http://qtlsolver.googlecode.comqtlsolver.googlecode.com.
2. Zot: a Bounded Satisfiability Checker. available from http://zot.googlecode.comzot.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, Tomá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. http://arxiv.org/abs/1205.0946arXiv: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.
11. Patricia Bouyer, Fabrice Chevalier & Nicolas Markey (2010): On the expressiveness of TPTL and MTL. Information and Computation 208(2), pp. 97 – 116. Available at http://dx.doi.org/10.1016/j.ic.2009.10.004.
12. Stéphane Demri & Deepak D'Souza (2007): An automata-theoretic approach to constraint LTL. Information and Computation 205(3), pp. 380–415. Available at http://dx.doi.org/10.1016/j.ic.2006.09.006.
13. Deepak D'Souza & Nicolas Tabareau (2004): On Timed Automata with Input-Determined Guards. In: Proc. of FORMATS/FTRTFT, LNCS 3253. Springer, pp. 68–83. Available at http://dx.doi.org/10.1007/978-3-540-30206-3_7.
14. Carlo A. Furia, Dino Mandrioli, Angelo Morzenti & Matteo Rossi (2012): Modeling Time in Computing. EATCS Monographs in Theoretical Computer Science. Springer. Available at http://dx.doi.org/10.1007/978-3-642-32332-4.
15. Thomas A. Henzinger, Jean F. Raskin & Pierre Y. Schobbens (1998): The Regular Real-Time Languages. In: Proc. of ICALP'98, LNCS 1343, pp. 580–591. Available at http://dx.doi.org/10.1007/BFb0055086.
16. Yoram Hirshfeld & Alexander Moshe Rabinovich (2004): Logics for Real Time: Decidability and Complexity. Fundamenta Informaticae 62(1), pp. 1–28.
17. Oded Maler, Dejan Nickovic & Amir Pnueli (2006): From MITL to Timed Automata. In: Proc. of FORMATS, LNCS 4202, pp. 274–289. Available at http://dx.doi.org/10.1007/11867340_20.
18. Microsoft Research (2009): Z3: An Efficient SMT Solver. Available at: http://research.microsoft.com/en-us/um/redmond/projects/z3/.
19. Angelo Morzenti & Pierluigi San Pietro (1994): Object-Oriented Logical Specification of Time-Critical Systems. ACM Transactions on Software Engineering and Methodology (TOSEM) 3(1), pp. 56–98. Available at http://doi.acm.org/10.1145/174634.174636.
20. Matteo Pradella, Angelo Morzenti & Pierluigi San Pietro (2013): Bounded Satisfiability Checking of Metric Temporal Logic Specifications. ACM Trans. on Soft. Eng. and Meth. (TOSEM). To appear.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org