References

  1. R. Alur, T. Feder & T.A. Henzinger (1996): The Benefits of Relaxing Punctuality. J. ACM 43(1), pp. 116–146, doi:10.1145/227595.227602.
  2. R. Alur, L. Fix & T.A. Henzinger (1999): Event-Clock Automata: A Determinizable Class of Timed Automata. Theor. Comput. Sci. 211(1-2), pp. 253–273, doi:10.1016/S0304-3975(97)00173-4.
  3. R. Alur & T.A. Henzinger (1991): Logics and Models of Real Time: A Survey. In: REX Workshop, pp. 74–106, doi:10.1007/BFb0031988.
  4. R. Alur & T.A. Henzinger (1993): Real-Time Logics: Complexity and Expressiveness. Inf. Comput. 104(1), pp. 35–77, doi:10.1006/inco.1993.1025.
  5. C.W. Barrett, R. Sebastiani, S.A. Seshia & C. Tinelli (2009): Satisfiability Modulo Theories. In: Handbook of Satisfiability, pp. 825–885, doi:10.3233/978-1-58603-929-5-825.
  6. D.A. Basin, F. Klaedtke & S. Müller (2010): Policy Monitoring in First-Order Temporal Logic. In: CAV, pp. 1–18, doi:10.1007/978-3-642-14295-6_1.
  7. A. Bouajjani & Y. Lakhnech (1995): Temporal Logic + Timed Automata: Expressiveness and Decidability. In: CONCUR, pp. 531–545, doi:10.1007/3-540-60218-6_40.
  8. P. Bouyer, F. Chevalier & N. Markey (2010): On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), pp. 97–116, doi:10.1016/j.ic.2009.10.004.
  9. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri & S. Tonetta (2014): The nuXmv Symbolic Model Checker. In: CAV, pp. 334–342, doi:10.1007/978-3-319-08867-9_22.
  10. A. Cimatti, M. Dorigatti & S. Tonetta (2013): OCRA: A tool for checking the refinement of temporal contracts. In: ASE, pp. 702–705, doi:10.1109/ASE.2013.6693137.
  11. A. Cimatti, A. Griggio, S. Mover & S. Tonetta (2014): IC3 Modulo Theories via Implicit Predicate Abstraction. In: TACAS, LNCS 8413. Springer, pp. 46–61, doi:10.1007/978-3-642-54862-8_4.
  12. A. Cimatti, A. Griggio, S. Mover & S. Tonetta (2014): Verifying LTL Properties of Hybrid Systems with K-Liveness. In: CAV, LNCS 8559. Springer, pp. 424–440, doi:10.1007/978-3-319-08867-9_28.
  13. A. Cimatti, A. Griggio, S. Mover & S. Tonetta (2015): HyComp: An SMT-Based Model Checker for Hybrid Systems. In: TACAS, pp. 52–67, doi:10.1007/978-3-662-46681-0_4.
  14. A. Cimatti, M. Roveri & S. Tonetta (2009): Requirements Validation for Hybrid Systems. In: CAV, pp. 188–203, doi:10.1007/978-3-642-02658-4_17.
  15. K. Claessen & N. Sörensson (2012): A Liveness Checking Algorithm that Counts. In: FMCAD. IEEE, pp. 52–59.
  16. J. Daniel, A. Cimatti, A. Griggio, S. Tonetta & S. Mover (2016): Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. In: CAV, pp. 271–291, doi:10.1007/978-3-319-41528-4_15.
  17. S. Demri & R. Lazic (2009): LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), pp. 16:1–16:30, doi:10.1145/1507244.1507246.
  18. C.A. Furia & M. Rossi (2007): On the Expressiveness of MTL Variants over Dense Time. In: FORMATS, pp. 163–178, doi:10.1007/978-3-540-75454-1_13.
  19. S. Ghilardi, E. Nicolini, S. Ranise & D. Zucchelli (2007): Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. In: CADE, pp. 362–378, doi:10.1007/978-3-540-73595-3_25.
  20. T. A. Henzinger, J.-F. Raskin & P.-Y. Schobbens (1998): The Regular Real-Time Languages. In: ICALP, pp. 580–591, doi:10.1007/BFb0055086.
  21. Y. Hirshfeld & A.M. Rabinovich (2006): An Expressive Temporal Logic for Real Time. In: MFCS, pp. 492–504, doi:10.1007/11821069_43.
  22. R. Koymans (1990): Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems 2(4), pp. 255–299, doi:10.1007/BF01995674.
  23. R. Koymans (1992): Specifying Message Passing and Time-Critical Systems with Temporal Logic. Lecture Notes in Computer Science 651. Springer, doi:10.1007/3-540-56283-4.
  24. O. Lichtenstein, A. Pnueli & L.D. Zuck (1985): The Glory of the Past. In: Logics of Programs, pp. 196–218, doi:10.1007/3-540-15648-8_16.
  25. Z. Manna & A. Pnueli (1992): The temporal logic of reactive and concurrent systems - specification. Springer, doi:10.1007/978-1-4612-0931-7.
  26. J.J. Ortiz, A. Legay & P.-Y. Schobbens (2010): Memory Event Clocks. In: FORMATS, pp. 198–212, doi:10.1007/978-3-642-15297-9_16.
  27. A. Pnueli (1977): The Temporal Logic of Programs. In: FOCS, pp. 46–57, doi:10.1109/SFCS.1977.32.
  28. A.M. Rabinovich (1998): On the Decidability of Continuous Time Specification Formalisms. J. Log. Comput. 8(5), pp. 669–678, doi:10.1093/logcom/8.5.669.
  29. J.-F. Raskin & P.-Y. Schobbens (1997): State Clock Logic: A Decidable Real-Time Logic. In: HART, pp. 33–47, doi:10.1007/BFb0014711.
  30. J.-F. Raskin & P.-Y. Schobbens (1999): The Logic of Event Clocks - Decidability, Complexity and Expressiveness. Journal of Automata, Languages and Combinatorics 4(3), pp. 247–286.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org