@misc(qtlsolver,
 title        = "qtlsolver",
 howpublished = "available from \href {http://qtlsolver.googlecode.com}{\texttt {qtlsolver.googlecode.com}}",
)
@misc(ae2zot,
 title        = "Zot: a Bounded Satisfiability Checker",
 howpublished = "available from \href {http://zot.googlecode.com}{\texttt {zot.googlecode.com}}",
)
@article(Alur&Dill94,
 author       = "Rajeev Alur and David L. Dill",
 year         = "1994",
 title        = "A theory of timed automata",
 journal      = "Theor. Comp. Sci.",
 volume       = "126",
 number       = "2",
 pages        = "183--235",
 url          = "http://dx.doi.org/10.1016/0304-3975(94)90010-8",
)
@article(AFH96,
 author       = "Rajeev Alur and Tom{\' a}s Feder and Thomas A. Henzinger",
 year         = "1996",
 title        = "The Benefits of Relaxing Punctuality",
 journal      = "Journal of the ACM",
 volume       = "43",
 number       = "1",
 pages        = "116--146",
 url          = "http://doi.acm.org/10.1145/112600.112613",
)
@book(BK08,
 author       = "Christel Baier and Joost-Pieter Katoen",
 year         = "2008",
 title        = "Principles of Model Checking",
 publisher    = "MIT Press",
)
@incollection(BY04,
 author       = "Johan Bengtsson and Wang Yi",
 year         = "2004",
 title        = "Timed Automata: Semantics, Algorithms and Tools",
 booktitle    = "Lect. on Concurrency and Petri Nets",
 series       = "LNCS",
 volume       = "3098",
 publisher    = "Springer",
 pages        = "87--124",
 url          = "http://dx.doi.org/10.1007/978-3-540-27755-2_3",
)
@inproceedings(BFMPRS10,
 author       = "Marcello M. Bersani and Achille Frigeri and Angelo Morzenti and Matteo Pradella and Matteo Rossi and Pierluigi {San Pietro}",
 year         = "2010",
 title        = "Bounded Reachability for Temporal Logic over Constraint Systems",
 booktitle    = "TIME",
 publisher    = "IEEE Computer Society",
 pages        = "43--50",
 url          = "http://dx.doi.org/10.1109/TIME.2010.21",
)
@misc(BFMPRS12,
 author       = "Marcello M. Bersani and Achille Frigeri and Angelo Morzenti and Matteo Pradella and Matteo Rossi and Pierluigi {San Pietro}",
 year         = "2012",
 title        = "{CLTL Satisfiability Checking without Automata}",
 howpublished = "\href {http://arxiv.org/abs/1205.0946}{arXiv:1205.0946v1}",
)
@incollection(BFRS11,
 author       = "Marcello M. Bersani and Achille Frigeri and Matteo Rossi and Pierluigi {San Pietro}",
 year         = "2011",
 title        = "Completeness of the Bounded Satisfiability Problem for Constraint {LTL}",
 booktitle    = "Reachability Problems",
 series       = "LNCS",
 volume       = "6945",
 pages        = "58--71",
 url          = "http://dx.doi.org/10.1007/978-3-642-24288-5_7",
)
@inproceedings(BRS13b,
 author       = "Marcello M. Bersani and Matteo Rossi and Pierluigi {San Pietro}",
 year         = "2013",
 title        = "A Tool for Deciding the Satisfiability of Continuous-time Metric Temporal Logic",
 booktitle    = "Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME)",
 note         = "To appear",
)
@article(BCM10,
 author       = "Patricia Bouyer and Fabrice Chevalier and Nicolas Markey",
 year         = "2010",
 title        = "On the expressiveness of {TPTL} and {MTL}",
 journal      = "Information and Computation",
 volume       = "208",
 number       = "2",
 pages        = "97 -- 116",
 url          = "http://dx.doi.org/10.1016/j.ic.2009.10.004",
)
@article(DD07,
 author       = "St\'{e}phane Demri and Deepak D'Souza",
 year         = "2007",
 title        = "An automata-theoretic approach to constraint {LTL}",
 journal      = "Information and Computation",
 volume       = "205",
 number       = "3",
 pages        = "380--415",
 url          = "http://dx.doi.org/10.1016/j.ic.2006.09.006",
)
@incollection(Souza&Tabareau04,
 author       = "Deepak D'Souza and Nicolas Tabareau",
 year         = "2004",
 title        = "On Timed Automata with Input-Determined Guards",
 booktitle    = "Proc. of FORMATS/FTRTFT",
 series       = "LNCS",
 volume       = "3253",
 publisher    = "Springer",
 pages        = "68--83",
 url          = "http://dx.doi.org/10.1007/978-3-540-30206-3_7",
)
@book(FMMR12,
 author       = "Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Rossi",
 year         = "2012",
 title        = "Modeling Time in Computing",
 series       = "{EATCS} Monographs in Theoretical Computer Science",
 publisher    = "Springer",
 url          = "http://dx.doi.org/10.1007/978-3-642-32332-4",
)
@inproceedings(HRS98a,
 author       = "Thomas A. Henzinger and Jean F. Raskin and Pierre Y. Schobbens",
 year         = "1998",
 title        = "{The Regular Real-Time Languages}",
 booktitle    = "Proc. of ICALP'98",
 series       = "LNCS",
 volume       = "1343",
 pages        = "580--591",
 url          = "http://dx.doi.org/10.1007/BFb0055086",
)
@article(HR04,
 author       = "Yoram Hirshfeld and Alexander Moshe Rabinovich",
 year         = "2004",
 title        = "Logics for Real Time: Decidability and Complexity",
 journal      = "Fundamenta Informaticae",
 volume       = "62",
 number       = "1",
 pages        = "1--28",
)
@incollection(MNP06,
 author       = "Oded Maler and Dejan Nickovic and Amir Pnueli",
 year         = "2006",
 title        = "From {MITL} to Timed Automata",
 booktitle    = "Proc. of FORMATS",
 series       = "LNCS",
 volume       = "4202",
 pages        = "274--289",
 url          = "http://dx.doi.org/10.1007/11867340_20",
)
@misc(z3,
 author       = "{Microsoft Research}",
 year         = "2009",
 title        = "Z3: An Efficient {SMT} Solver",
 howpublished = "Available at: http://research.microsoft.com/en-us/um/redmond/projects/z3/",
)
@article(MS94,
 author       = "Angelo Morzenti and Pierluigi {San Pietro}",
 year         = "1994",
 title        = "Object-Oriented Logical Specification of Time-Critical Systems",
 journal      = "ACM Transactions on Software Engineering and Methodology ({TOSEM})",
 volume       = "3",
 number       = "1",
 pages        = "56--98",
 url          = "http://doi.acm.org/10.1145/174634.174636",
)
@article(PMS12,
 author       = "Matteo Pradella and Angelo Morzenti and Pierluigi {San Pietro}",
 year         = "2013",
 title        = "Bounded Satisfiability Checking of Metric Temporal Logic Specifications",
 journal      = "{ACM} Trans. on Soft. Eng. and Meth. ({TOSEM})",
 note         = "To appear",
)