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.
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.
R. Alur & T.A. Henzinger (1991):
Logics and Models of Real Time: A Survey.
In: REX Workshop,
pp. 74–106,
doi:10.1007/BFb0031988.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
K. Claessen & N. Sörensson (2012):
A Liveness Checking Algorithm that Counts.
In: FMCAD.
IEEE,
pp. 52–59.
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.
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.
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.
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.
T. A. Henzinger, J.-F. Raskin & P.-Y. Schobbens (1998):
The Regular Real-Time Languages.
In: ICALP,
pp. 580–591,
doi:10.1007/BFb0055086.
Y. Hirshfeld & A.M. Rabinovich (2006):
An Expressive Temporal Logic for Real Time.
In: MFCS,
pp. 492–504,
doi:10.1007/11821069_43.
R. Koymans (1990):
Specifying Real-Time Properties with Metric Temporal Logic.
Real-Time Systems 2(4),
pp. 255–299,
doi:10.1007/BF01995674.
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.
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.
Z. Manna & A. Pnueli (1992):
The temporal logic of reactive and concurrent systems - specification.
Springer,
doi:10.1007/978-1-4612-0931-7.
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.
A. Pnueli (1977):
The Temporal Logic of Programs.
In: FOCS,
pp. 46–57,
doi:10.1109/SFCS.1977.32.
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.
J.-F. Raskin & P.-Y. Schobbens (1997):
State Clock Logic: A Decidable Real-Time Logic.
In: HART,
pp. 33–47,
doi:10.1007/BFb0014711.
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.