●Verificaiton Systems

○Hytech

T.A. Henzinger, P.-H. Ho, and H. Wong-Toi.  HyTech: A Model Checker
for Hybrid Systems.  Software Tools for Technology Transfer 1:110-122,
1997.

○STeP

Nikolaj Bjorner, Zohar Manna, Henny B. Sipma and Tomas E. Uribe.
Deductive Verification of Real-time Systems Using STeP.  Presented at
ARTS 97.

○Uppaal

Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Petersson, and Wang
Yi.  Uppaal -- a tool suite for automatic verification of real-time
systems.  In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag,
editors, Hybrid Systems III, LNCS 1066, pages 232--243, Berlin,
1996. Springer-Verlag.

○KRONOS

C. Daws, A. Olivero, S. Tripakis, and S. Yovine.  The tool KRONOS.  In
Hybrid Systems III, Verification and Control, volume 1066 of Lecture
Notes in Computer Science, pages 208--219. Springer-Verlag, 1996.

○PVS

N. Shankar.  Verification of real-time systems using PVS.  In Computer
Aided Verification: Fifth International Conference, CAV'93, number 697
in Lecture Notes in Computer Science, pages 280--291, Elounda, Greece,
June/July 1993. Springer-Verlag.

●More Basics

R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense
real-time. Information and Computation, 104(1):2--34, May 1993.

R. Alur and D. L. Dill, "A Theory of Timed Automata", Theoretical
Computer Science, Vol. 126, pp. 183-235, 1994.

Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio
Yovine. Symbolic model checking for real-time systems. Information and
Computation, 111(2):193-244, June 1994.

R. Alur, T.A. Henzinger, and P.-H. Ho.  Automatic Symbolic
Verification of Embedded Systems.  IEEE Transactions on Software
Engineering 22:181-201, 1996.

●Parametric Verification

Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi.  Parametric
Real-time Reasoning.  In Proceedings of the Twenty-Fifth Annual ACM
Symposium on the Theory of Computing, pages 592-601, 1993.

B. B'erard and L. Fribourg.  Automated verification of a parametric
real-time program: the ABR conformance protocol.  In Proc. 11th
Int. Conf. Computer Aided Verification (CAV'99), LNCS 1633, 1999,
pp. 96-107.

Thomas Hune, Judi Romijn, Marielle Stoelinga, and Frits Vaandrager.
Linear parametric model checking of timed automata.  Accpeted for
Tools and Algorithms for the Construction and Analysis of Systems,
2001.

●Rectangular Automata

T. Henzinger and P. Kopke.  State equivalences for rectangular hybrid
automata.  In U. Montanari and V. Sassone, editors, CONCUR 96:
Concurrency Theory, Lecture Notes in Computer Science 1119, pages
530--545. Springer-Verlag, 1996.

T.A. Henzinger and P.W. Kopke.  Discrete-time control for rectangular
hybrid automata.  Theoretical Computer Science, vol. 221, pp. 369-392,
1999.

Thomas A. Henzinger and Rupak Majumdar.  Symbolic Model Checking for
Rectangular Hybrid Systems.  Proceedings of the Sixth International
Workshop on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS 2000), Lecture Notes in Computer Science 1785,
Springer-Verlag, 142-156, 2000.

●Priced Timed Automata

Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen,
Paul Pettersson, Judi Romijn, Frits W.  Vaandrager: Minimum-Cost
Reachability for Priced Timed Automata.  HSCC 2001, Lecture Notes in
Computer Science, volume 2034, 2001, 147-161.

Rajeev Alur, Salvatorre La Torre, and George J. Pappas.  Optimal paths
in weighted timed automata.  HSCC 2001, Lecture Notes in Computer
Science, volume 2034, Springer, 2001, 49-62.

●Refinement of Hybrid Systems

R. Alur and R. Grosu.  Modular refinement of hierarchic reactive
machines.  In Proceedings of the 27th Annual ACM Symposium on
Principles of Programming Languages, pages 390--402, 2000.

Thomas A. Henzinger.  Masaccio: a formal model for embedded
components.  Proceedings of the First IFIP International Conference on
Theoretical Computer Science, Lecture Notes in Computer Science 1872,
Springer-Verlag, 2000, pp. 549-563.