\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{MAB{\etalchar{+}}94}

\bibitem[AD94]{AD94}
R.~Alur and D.L. Dill.
\newblock A theory of timed automata.
\newblock {\em Theor. Comp. Sci.}, 126:183--235, 1994.

\bibitem[AH89]{TPTL1}
R.~Alur and T.A. Henzinger.
\newblock A really temporal logic.
\newblock In {\em Proc. 30th IEEE Symp. Found. of Comp. Sci.}, pages 164--169,
  1989.

\bibitem[AH92]{AHsur}
R.~Alur and T.~Henzinger.
\newblock Logics and models of real time: A survey.
\newblock In J.W. de~Bakker, C.~Huizing, W.P. de~Roever, and G.~Rozenberg,
  editors, {\em Proceedings of the REX Workshop ``Real-Time: Theory in
  Practice''}, volume 600 of {\em Lect. Notes in Comp. Sci.}, pages 74--106.
  Springer-Verlag, 1992.

\bibitem[AL94]{AL91}
M.~Abadi and L.~Lamport.
\newblock An old-fashioned recipe for real time.
\newblock {\em ACM Trans. Prog. Lang. Sys.}, 16(5):1543--1571, 1994.

\bibitem[BAMP83]{BMP}
M.~Ben-Ari, Z.~Manna, and A.~Pnueli.
\newblock The temporal logic of branching time.
\newblock {\em Acta Informatica}, 20:207--226, 1983.

\bibitem[BH81]{BH81}
A.~Bernstein and P.~K. Harter.
\newblock Proving real time properties of programs with temporal logic.
\newblock In {\em Proceedings of the Eighth Symposium on Operating Systems
  Principles}, pages 1--11. ACM, 1981.

\bibitem[EC82]{EC}
E.A. Emerson and E.M. Clarke.
\newblock Using branching time temporal logic to synthesize synchronization
  skeletons.
\newblock {\em Sci. Comp. Prog.}, 2:241--266, 1982.

\bibitem[FG95]{FG95}
L.~Fix and O.~Grumberg.
\newblock Verificaiton of temporal properties.
\newblock to appear in {\sl Logic and Computation}, 1995.

\bibitem[Har87]{H}
D.~Harel.
\newblock Statecharts: {A} visual formalism for complex systems.
\newblock {\em Sci. Comp. Prog.}, 8:231--274, 1987.

\bibitem[Hen92]{IPL}
T.A. Henzinger.
\newblock Sooner is safer than later.
\newblock {\em Info. Proc. Lett.}, 43(3):135--142, 1992.

\bibitem[HMP94]{TPMTTS}
T.~Henzinger, Z.~Manna, and A.~Pnueli.
\newblock Temporal proof methodologies for timed transition systems.
\newblock {\em Inf. and Comp.}, 112(2):273--337, 1994.

\bibitem[KdR85]{KdR}
R.~Koymans and W.-P. de~Roever.
\newblock Examples of a real-time temporal logic specifications.
\newblock In B.D. Denvir, W.T. Harwood, M.I. Jackson, and M.J. Wray, editors,
  {\em The Analysis of Concurrent Systems}, volume 207 of {\em Lect. Notes in
  Comp. Sci.}, pages 231--252. Springer-Verlag, 1985.

\bibitem[Koy90]{Koy90}
R.~Koymans.
\newblock Specifying real-time properties with metric temporal logic.
\newblock {\em Real-time Systems}, 2(4):255--299, 1990.

\bibitem[KVdR83]{KVdR}
R.~Koymans, J.~Vytopyl, and W.-P. de~Roever.
\newblock Real-time programming and asynchronous message passing.
\newblock In {\em Proc. 2nd ACM Symp. Princ. of Dist. Comp.}, pages 187--197,
  1983.

\bibitem[Lam95]{possibility}
L.~Lamport.
\newblock Proving possibiity properties.
\newblock Technical Report 137, Digital Equipment Corporation, Systems Research
  Center, Palo Alto, July 1995.

\bibitem[MAB{\etalchar{+}}94]{STeP}
Z.~Manna, A.~Anuchitanukul, N.~Bj{\o}rner, A.~Browne, E.~Chang, M.~Col\'{o}n,
  L.~De Alfaro, H.~Devarajan, H.~Sipma, and T.~Uribe.
\newblock {STeP}: The {S}tanford {T}emporal {P}rover.
\newblock Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford
  University, Stanford, California, 1994.

\bibitem[MMP92]{MMP}
O.~Maler, Z.~Manna, and A.~Pnueli.
\newblock From timed to hybrid systems.
\newblock In J.W. de~Bakker, C.~Huizing, W.P. de~Roever, and G.~Rozenberg,
  editors, {\em Proceedings of the REX Workshop ``Real-Time: Theory in
  Practice''}, volume 600 of {\em Lect. Notes in Comp. Sci.}, pages 447--484.
  Springer-Verlag, 1992.

\bibitem[MP91a]{Comp91}
Z.~Manna and A.~Pnueli.
\newblock Completing the temporal picture.
\newblock {\em Theor. Comp. Sci.}, 83(1):97--130, 1991.

\bibitem[MP91b]{MPB}
Z.~Manna and A.~Pnueli.
\newblock {\em The Temporal Logic of Reactive and Concurrent Systems:
  Specification}.
\newblock Springer-Verlag, New York, 1991.

\bibitem[MP93]{ModR}
Z.~Manna and A.~Pnueli.
\newblock Models for reactivity.
\newblock {\em Acta Informatica}, 30:609--678, 1993.

\bibitem[MP94]{tacs94}
Z.~Manna and A.~Pnueli.
\newblock Temporal verification diagrams.
\newblock In T.~Ito and A.~R. Meyer, editors, {\em Theoretical Aspects of
  Computer Software}, volume 789 of {\em Lect. Notes in Comp. Sci.}, pages
  726--765. Springer-Verlag, 1994.

\bibitem[MP95]{MPB2}
Z.~Manna and A.~Pnueli.
\newblock {\em Temporal Verification of Reactive Systems: Safety}.
\newblock Springer-Verlag, New York, 1995.

\bibitem[MT90]{MT90}
F.~Moller and C.~Tofts.
\newblock A temporal calculus of communicating systems.
\newblock In J.C.M. Baeten and J.W. Klop, editors, {\em Proceedings of
  Concur'90}, volume 458 of {\em Lect. Notes in Comp. Sci.}, pages 401--415.
  Springer-Verlag, 1990.

\bibitem[NSY92]{NSY91}
X.~Nicollin, J.~Sifakis, and S.~Yovine.
\newblock From {ATP} to timed graphs and hybrid systems.
\newblock In J.W. de~Bakker, C.~Huizing, W.P. de~Roever, and G.~Rozenberg,
  editors, {\em Proceedings of the REX Workshop ``Real-Time: Theory in
  Practice''}, volume 600 of {\em Lect. Notes in Comp. Sci.}, pages 549--572.
  Springer-Verlag, 1992.

\bibitem[Ost90]{BOST}
J.S. Ostroff.
\newblock {\em Temporal Logic of Real-Time Systems}.
\newblock Advanced Software Development Series. Research Studies Press (John
  Wiley \& Sons), Taunton, England, 1990.

\bibitem[Pnu92]{vital}
A.~Pnueli.
\newblock How vital is liveness?
\newblock In W.R. Cleaveland, editor, {\em Proceedings of Concur'92}, volume
  630 of {\em Lect. Notes in Comp. Sci.}, pages 162--175. Springer-Verlag,
  1992.

\bibitem[SBM92]{SBM91}
F.~B. Schneider, B.~Bloom, and K.~Marzullo.
\newblock Putting time into proof outlines.
\newblock In J.W. de~Bakker, C.~Huizing, W.P. de~Roever, and G.~Rozenberg,
  editors, {\em Proceedings of the REX Workshop ``Real-Time: Theory in
  Practice''}, volume 600 of {\em Lect. Notes in Comp. Sci.}, pages 618--639.
  Springer-Verlag, 1992.

\bibitem[Sif91]{Si91}
J.~Sifakis.
\newblock An overview and synthesis on timed process algebra.
\newblock In K.G. Larsen and A.~Skou, editors, {\em 3rd Computer Aided
  Verification Workshop}, volume 575 of {\em Lect. Notes in Comp. Sci.}, pages
  376--398. Springer-Verlag, 1991.

\end{thebibliography}