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