\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{SGSAL98}

\bibitem[ACH{\etalchar{+}}95]{AlurEtAl95}
R.~Alur, C.~Courcoubetis, N.~Halbwachs, T.~A. Henzinger, P.~H. Ho, X.~Nicollin,
  A.~Olivero, J.~Sifakis, and S.~Yovine.
\newblock The algorithmic analysis of hybrid systems.
\newblock {\em Theoretical Computer Science}, 138(1):3--34, 1995.

\bibitem[AD94]{AlurD94}
Rajeev Alur and David~L. Dill.
\newblock A theory of timed automata.
\newblock {\em Theoretical Computer Science}, 126(2):183--235, April 1994.

\bibitem[AH97]{AlurH-97}
Rajeev Alur and Thomas~A. Henzinger.
\newblock Modularity for timed and hybrid systems.
\newblock In {\em Proceedings of Ninth International Conference on Concurrency
  Theory}, volume 1243 of {\em Lecture Notes in Computer Science}, 1997.

\bibitem[AH99]{AlurHenzinger-reactive}
R.~Alur and T.~A. Henzinger.
\newblock Reactive modules.
\newblock {\em Formal Methods in System Design}, 15(1):7--48, 1999.
\newblock Earlier version in {\em Proceedings of the 11th IEEE Symposium on
  Logic in Computer Science}, pp. 207-218, 1996. \verb+URL
  www.cis.upenn.edu/~alur/Lics96T.ps.gz+.

\bibitem[AHH96]{RTSS93j}
R.~Alur, T.~A. Henzinger, and P.~H. Ho.
\newblock Automatic symbolic verification of embedded systems.
\newblock {\em IEEE Transactions on Software Engineering}, 22(3):181--201,
  1996.

\bibitem[AL93]{AbadiLamport-compose}
Martin Abadi and Leslie Lamport.
\newblock Composing specifications.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  15(1):73--132, January 1993.
\newblock Also appeared as SRC Research Report 66.

\bibitem[Alu]{Alur-nato}
Rajeev Alur.
\newblock Timed automata.
\newblock NATO summer school, 1998. \verb+URL
  www.cis.upenn.edu/~alur/Nato97.ps.gz+.

\bibitem[BDL96]{BranickyDL96}
Michael~S. Branicky, Ekaterina Dolginova, and Nancy Lynch.
\newblock A toolbox for proving and maintaining hybrid specifications.
\newblock In {\em HS'96: Hybrid Systems}, Cornell University, Ithacs, NY,
  October 1996.
\newblock To be published in Springer-Verlag, Lecture Notes in Computer Science
  series.

\bibitem[Bra95]{Branicky}
Michael~S. Branicky.
\newblock {\em Studies in Hybrid Systems: Modeling, Analysis, and Control}.
\newblock PhD thesis, Department of Electrical Engineering and Computer
  Science, Massachusetts Institute of Technology, Cambridge, MA, June 1995.

\bibitem[CGL94]{ClarkeOL-94}
E.~M. Clarke, Orna Grumberg, and D.~E. Long.
\newblock Verification tools for finite-state concurrent systems.
\newblock In {\em A Decade of Concurrency: Reflections and Perspectives},
  volume 803 of {\em Lecture Notes in Computer Science}. Springer-Verlag, 1994.

\bibitem[CGP99]{ClarkeGP-99}
E.~M. Clarke, Orna Grumberg, and Doron Peled.
\newblock {\em Model Checking}.
\newblock MIT Press, December 1999.

\bibitem[CM88]{ChandyM88}
K.~Mani Chandy and Jayadev Misra.
\newblock {\em Parallel Program Design: A Foundation}.
\newblock Addison-Wesley Publishing Co., Reading, MA, 1988.

\bibitem[CMT89]{Trivedietal-spnp}
G.~Ciardo, J.~K. Muppala, and K.~S. Trivedi.
\newblock S{PNP}: Stochastic petri net package.
\newblock In {\em Proc. of 3rd International Workshop on Petri Nets and
  Performance Models}, pages 142--150, Kyoto, Japan, December 1989.

\bibitem[dRE98]{deRoeverEngelhardt}
Willem-Paul de~Roever and Kai Engelhardt.
\newblock {\em Data Refinement: Model-Oriented Proof Methods and their
  Comparison}.
\newblock Cambridge University Press, 1998.

\bibitem[Eme90]{Emerson90}
E.~A. Emerson.
\newblock Temporal and modal logic.
\newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer
  Science: Volume B, Formal Models and Semantics}, pages 995--1072. North
  Holland Pub. Co./MIT Press, 1990.
\newblock Chapter 16.

\bibitem[GL00]{IOA-leavens}
Stephen~J. Garland and Nancy~A. Lynch.
\newblock {\em Using {I/O} Automata for Developing Distributed Systems},
  chapter~13, pages 285--312.
\newblock Cambridge University Press, USA, 2000.

\bibitem[GLV97]{GLV-IOA-manual}
Stephen~J. Garland, Nancy~A. Lynch, and Mandana Vaziri.
\newblock I{OA}: A language for specifying, programming and validating
  distributed systems, December 1997.
\newblock User and Reference Manual. \verb+URL
  http://sds.lcs.mit.edu/~garland/ioaLanguage.html+.

\bibitem[Har87]{Harel-statecharts}
David Harel.
\newblock Statecharts: A visual formalism for complex systems.
\newblock {\em Science of Computer Programming}, 8:231--274, 1987.

\bibitem[Har88]{Harel-cacm88}
D.~Harel.
\newblock On visual formalisms.
\newblock {\em Communications of the ACM}, 31(5):514--530, 1988.
\newblock (Reprinted in {\em Diagrammatic Reasoning} (Chandrasekaran et al.,
  eds), AAAI Press and MIT Press, 1995, pp. 235-271, and in {\em High Integrity
  System Specification and Design} (Bowen and Hinchey, eds.), Springer-Verlag,
  London, 1999, pp. 623-657.).

\bibitem[Hen96]{Henzinger-lics96}
Thomas~A. Henzinger.
\newblock The theory of hybrid automata.
\newblock In {\em Proceedings of the 11th Annual IEEE Symposium on Logic in
  Computer Science (LICS 1996)}, pages 278--292, 1996.
\newblock \verb+URL
  www-cad.eecs.berkeley.edu/~tah/Publications/the_theory_of_hybrid_automata.ht%
ml+.

\bibitem[HHWT97]{HenzingerHoToi}
Thomas~A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
\newblock Hy{T}ech: a model checker for hybrid systems.
\newblock {\em Software Tools for Technology Transfer}, 1:110--122, 1997.
\newblock \verb+URL
  http://www-cad.eecs.berkeley.edu/~tah/Publications/hytech.html+.

\bibitem[HKPV98]{HenzingerKPV-jcss}
Thomas~A. Henzinger, Peter~W. Kopke, Anuj Puri, and Pravin Varaiya.
\newblock What's decidable about hybrid automata?
\newblock {\em Journal of Computer and System Sciences}, 57:94--124, 1998.
\newblock \verb+URL
  www-cad.eecs.berkeley.edu/~tah/Publications/whats_decidable_about_hybrid_aut%
omata.html+.

\bibitem[Hoa85]{Hoare85}
C.~A.~R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice-Hall International, United Kingdom, 1985.

\bibitem[Hol91]{SPIN-Holzmann}
Gerard~J. Holzmann.
\newblock {\em Design and Validation of Computer Protocols}.
\newblock Prentice Hall Software Series, New Jersey, 1991.

\bibitem[Jen99]{Jensen97}
Henrik~Ejersbo Jensen.
\newblock {\em Abstraction-Based Verification of Distributed Systems}.
\newblock PhD thesis, Department of Computer Science, Institute for Electronic
  Systems, Aalborg University, Aalborg, Denmark, June 1999.
\newblock R-99-5005.

\bibitem[KKLS00]{KKLS}
Idit Keidar, Roger Khazan, Nancy Lynch, and Alex Shvartsman.
\newblock An inheritance-based technique for building simulation proofs
  incrementally.
\newblock In {\em 22nd International Conference on Software Engineering
  (ICSE)}, pages 478--487, Limerick, Ireland, June 2000.
\newblock Also, invited as a journal submission to {\em ACM Transactions on
  Software Engineering and Methodology}, 2000.

\bibitem[Lam94]{Lamport91}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  16(3):872--923, May 1994.

\bibitem[Lam98]{Lamport-harder}
Leslie Lamport.
\newblock Composition: A way to make proofs harder.
\newblock In Willem-Paul de~Roever, Hans Langmaack, and Amir Pnueli, editors,
  {\em Compositionality: The Significant Difference (Proceedings of the
  COMPOS'97 Symposium)}, volume 1536 of {\em Lecture Notes in Computer
  Science}, pages 402--423, 1998.

\bibitem[Lam00a]{Lamport-chap1-7}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+} preliminary draft, December
  2000.
\newblock Chapters 1-7.

\bibitem[Lam00b]{Lamport-chap12-13}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+} preliminary draft, December
  2000.
\newblock Chapters 12-13.

\bibitem[Lam00c]{Lamport-chap10}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+} preliminary draft, December
  2000.
\newblock Chapter 10.

\bibitem[Lam00d]{Lamport-chap9}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+} preliminary draft, December
  2000.
\newblock Chapter 9.

\bibitem[LSV]{LynchSV00}
Nancy Lynch, Roberto Segala, and Frits Vaandraager.
\newblock Hybrid {I/O} automata.
\newblock Submitted for publication.

\bibitem[LT89]{LynchT89}
Nancy~A. Lynch and Mark~R. Tuttle.
\newblock An introduction to input/output automata.
\newblock {\em CWI-Quarterly}, 2(3):219--246, September 1989.
\newblock Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.
  Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science, Massachusetts
  Institute of Technology, Cambridge, MA 02139, November 1988.

\bibitem[LV95]{LV93I}
Nancy Lynch and Frits Vaandrager.
\newblock Forward and backward simulations --- {P}art {I}: Untimed systems.
\newblock {\em Information and Computation}, 121(2):214--233, September 1995.

\bibitem[LV96]{LV95II-jour}
Nancy Lynch and Frits Vaandrager.
\newblock Forward and backward simulations --- {P}art {II}: Timing-based
  systems.
\newblock {\em Information and Computation}, 128(1):1--25, July 1996.

\bibitem[Lyn96a]{Lynch-bookchap8}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 8.

\bibitem[Lyn96b]{Lynch-bookchap23}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 23.

\bibitem[Lyn00]{6042-fall00}
Nancy Lynch.
\newblock 6.042 lecture notes, Fall 2000.
\newblock Lectures 8, 9, 10. URL
  http://theory.lcs.mit.edu/classes/6.042/fall00/handouts/homepage.html.

\bibitem[M\"a]{Mueller-temporal}
Olaf M\"uller.
\newblock A verification environment for {I/O} automata - part i: Temporal
  logic and abstraction.
\newblock Submitted for publication.

\bibitem[M\"b]{Mueller-theorem}
Olaf M\"uller.
\newblock A verification environment for {I/O} automata - part ii: Theorem
  proving and model checking.
\newblock Submitted for publication.

\bibitem[M\"98]{Mueller-phd}
Olaf M\"uller.
\newblock {\em A Verification Environment for I/O Automata Based on Formalized
  Meta-Theory}.
\newblock PhD thesis, Technische Universitat Munchen, 1998.

\bibitem[MBSU98]{MBSU-amast}
Zohar Manna, Anca Browne, Henny~B. Sipma, and Tomas~E. Uribe.
\newblock Visual abstractions for temporal verification.
\newblock In {\em AMAST'98}, volume 1548 of {\em Lecture Notes in Computer
  Science}, pages 28--41. Springer-Verlag, 1998.

\bibitem[McM92]{SMV-McMillan}
K.L. McMillan.
\newblock {\em Symbolic Model Checking: an Approach to the State Explosion
  Problem}.
\newblock PhD thesis, Carnegie Mellon University, 1992.
\newblock CMU-CS-92-131.

\bibitem[Mil89]{Milner89}
Robin Milner.
\newblock {\em Communication and Concurrency}.
\newblock Prentice-Hall International, United Kingdom, 1989.

\bibitem[MMP92]{MalerMP91}
Oded Maler, Zohar Manna, and Amir Pnueli.
\newblock From timed to hybrid systems.
\newblock In J.~W. de~Bakker, C.~Huizing, and G.~Rozenberg, editors, {\em
  Real-Time: Theory in Practice (REX Workshop, Mook, The Netherlands, June
  1991)}, volume 600 of {\em Lecture Notes in Computer Science}, pages
  447--484. Springer-Verlag, 1992.

\bibitem[MP92a]{MannaP92}
Zohar Manna and Amir Pnueli.
\newblock {\em The Temporal Logic of Reactive and Concurrent Systems:
  Specification}.
\newblock Springer-Verlag, New York, 1992.

\bibitem[MP92b]{MannaP92-liveness}
Zohar Manna and Amir Pnueli.
\newblock {\em The Temporal Logic of Reactive and Concurrent Systems:
  Specification}.
\newblock Springer-Verlag, New York, 1992.
\newblock The liveness parts.

\bibitem[MP95]{MannaP95}
Zohar Manna and Amir Pnueli.
\newblock {\em Temporal Verification of Reactive Systems: Safety}.
\newblock Springer-Verlag, New York, 1995.

\bibitem[PSL00]{PSL98-jour}
Anna Pogosyants, Roberto Segala, and Nancy Lynch.
\newblock Verification of the randomized consensus algorithm of {A}spnes and
  {H}erlihy: a case study.
\newblock {\em Distributed Computing}, 13, July 2000.

\bibitem[Seg95]{Segala95}
Roberto Segala.
\newblock {\em Modeling and Verification of Randomized Distributed Real-Time
  Systems}.
\newblock PhD thesis, Department of Electrical Engineering and Computer
  Science, Massachusetts Institute of Technology, May 1995.
\newblock Also, MIT/LCS/TR-676.

\bibitem[SGSAL98]{GLSS93-jour}
Roberto Segala, Rainer Gawlick, J{\o}rgen S{\o}gaard-Andersen, and Nancy Lynch.
\newblock Liveness in timed and untimed systems.
\newblock {\em Information and Computation}, 141(2):119--171, March 1998.

\bibitem[Yov98]{Yovine}
Yovine.
\newblock Model checking timed automata.
\newblock In {\em Lectures on Embedded Systems}, volume 1494 of {\em Lecture
  Notes in Computer Science}, October 1998.

\end{thebibliography}
