References

1

Hybrid Systems IV, edited by P. Antsaklis, W. Kohn, A. Nerode and S. Sastry, Springer Verlag Lecture Notes in Computer Science, 1997, Vol. 1273.

2

T. Henzinger, ``The theory of hybrid automata,'' in Proceedings of the 11th Annual Symposium on Logic in Computer Science, pp. 278-292, IEEE Computer Society Press, 1996.

3

J. Lygeros, Hierarchical, Hybrid Control of Large Scale Systems. PhD thesis, Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, 1996.

ACH95

Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine, ``The algorithmic analysis of hybrid systems,'' Theoretical Computer Science 138, 1995, pp. 3-34.

4

J. Lygeros, D. N. Godbole, and S. Sastry, ``A verified hybrid controller for automated vehicles,'' Tech. Rep. UCB-ITS-PRR-97-9, Institute of Transportation Studies, University of California, Berkeley, 1997. To appear in the IEEE Transactions on Automatic Control, Special Issue on Hybrid Systems, April 1998.

5

J. Lygeros, C. Tomlin, and S. Sastry, ``Multiobjective hybrid controller synthesis,'' in Hybrid and Real-Time Systems (O. Maler, ed.), Lecture Notes in Computer Science 1201, pp. 109-123, Grenoble: Springer-Verlag, 1997. UCB/ERL Memo M97/59, submitted to Automatica.

6

J. Kosecka, C. Tomlin, G. Pappas and S. Sastry, ``Conflict Resolution for Aircraft using Potential Fields'', IN: Proceedings of the International Conference on Intelligent Robotics and Systems, Grenoble, Sept. 1997.

7

Tomlin, C.; Pappas, G.; Lygeros, J.; Godbole, D., and S. Sastry, "Hybrid control models of next generation air traffic management", IN: Hybrid Systems IV, Ithaca, NY, USA, 12-14 Oct. 1996). Edited by: Antsaklis, P.; Kohn, W.; Nerode, A.; Sastry, S. Berlin, Germany: Springer-Verlag, 1997. p. 378-404.

8

Lygeros, J.; Tomlin, C.; Sastry, S. "Multiobjective hybrid controller synthesis", IN: Hybrid and Real- Time Systems. International Workshop, HART'97. Proceedings, Grenoble, France, 26-28 March 1997). Edited by: Maler, O. Berlin, Germany: Springer-Verlag, 1997. p. 109-23.

9

Lygeros, J.; Godbole, D.N.; Sastry, S. "A game-theoretic approach to hybrid system design", IN: Hybrid Systems III. Verification and Control, New Brunswick, NJ, USA, 22-25 Oct. 1995). Edited by: Alur, R.; Henzinger, T.A.; Sontag, E.D. Berlin, Germany: Springer-Verlag, 1996. p. 1-12.

AH97

Rajeev Alur, Thomas A. Henzinger, ``Modularity for timed and hybrid systems,'' Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR 97), Lecture Notes in Computer Science 1243, Springer-Verlag, 1997, pp. 74-88.

http://www.eecs.berkeley.edu/~ tah/Publications/modularity_for_timed_and_hybrid_systems.html

BB91

A. Benveniste, G. Berry, ``The synchronous approach to reactive and real-time systems,'' Proceedings of the IEEE 79, 1991, pp. 1270-1282.

C93

C. Cassandras, Discrete Event Systems: Modeling and Performance Analysis, Irwin, Homewood IL, 1993.

GLL97

A. Girault, B. Lee, E.A. Lee, A Preliminary Study of Hierarchical Finite State Machines with Multiple Concurrency Models, ERL Memorandum UCB/ERL-M97/57, University of California, Berkeley, CA 94720, August 1997.

http://ptolemy.eecs.berkeley.edu/papers/97/preliminaryStarcharts

GHJ97

Vineet Gupta, Thomas A. Henzinger, Radha Jagadeesan, ``Robust timed automata,'' Proceedings of the First International Workshop on Hybrid and Real-time Systems (HART 97), Lecture Notes in Computer Science 1201, Springer-Verlag, 1997, pp. 331-345.

http://www.eecs.berkeley.edu/~ tah/Publications/robust_timed_automata.html

H987

D. Harel, ``Statecharts: a visual formalism for complex systems,'' Science of Computer Programming 8, 1987, pp. 231-274.

LP95

E.A. Lee, T.M. Parks, ``Dataflow process networks,'', Proceedings of the IEEE 83, 1995, pp. 773-801.

http://ptolemy.eecs.berkeley.edu/papers/processNets

LS97

E.A. Lee, A. Sangiovanni-Vincentelli, A Denotational Framework for Comparing Models of Computation, ERL Memorandum UCB/ERL-M97/11, University of California, Berkeley, CA 94720, January 1997.

http://ptolemy.eecs.berkeley.edu/papers/97/denotational

10

G. Holzmann, Design and Validation of Computer Protocols. Prentice-Hall, 1991.

11

R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho, ``Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems,'' in Hybrid Systems I (R. Grossman, A. Nerode, A. Ravn, and H. Rischel, eds.), Lecture Notes in Computer Science 736, pp. 209-229, Springer-Verlag, 1993.

12

J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, ``Symbolic model checking: states and beyond,'' Information and Computation, vol. 98, no. 2, pp. 142-170, 1992.

13

Z. Har'El and R. Kurshan, Cospan User's Guide. AT&T Bell Laboratories, 1987.

14

R. Alur and D. Dill, ``A theory of timed automata,'' Theoretical Computer Science, vol. 126, pp. 183-235, 1994.

15

T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, ``Symbolic model checking for real-time systems,'' Information and Computation, vol. 111, no. 2, pp. 193-244, 1994.

16

C. Daws and S. Yovine, ``Two examples of verification of multirate timed automata with KRONOS,'' in Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95, (Pisa, Italy), IEEE Computer Society Press, Dec. 1995.

17

K. Larsen, P. Pettersson, and W. Yi, ``Compositional and symbolic model checking of real-time systems,'' in Proceedings of the 16th Annual Real-time Systems Symposium, pp. 76-87, IEEE Computer Society Press, 1995.

18

R. P. Kurshan, Computer-aided verification of coordinating processes; the automata-theoretic approach. Princeton University Press, 1994.

19

F. Balarin, K. Petty, and A. L. Sangiovanni-Vincentelli, ``Formal verification of the PATHO real-time operating system,'' in IEEE Control and Decision Conference, pp. 2459-2465, 1994.

20

R. Alur, T. Henzinger, and P.-H. Ho, ``Automatic symbolic verification of embedded systems,'' IEEE Transactions on Software Engineering, to appear.

21

T. Henzinger, P.-H. Ho, and H. Wong-Toi, ``A user guide to HYTECH,'' in TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems (E. Brinksma, W. Cleaveland, K. Larsen, T. Margaria, and B. Steffen, eds.), Lecture Notes in Computer Science 1019, pp. 41-71, Springer-Verlag, 1995. Full version available as Technical Report CSD-TR-95-1532, Cornell University.

22

R. Alur and T. Henzinger, ``Local liveness for compositional modeling of fair reactive systems,'' in CAV 95: Computer-aided Verification (P. Wolper, ed.), Lecture Notes in Computer Science 939, pp. 166-179, Springer-Verlag, 1995.

23

T. Henzinger and P.-H. Ho, ``Algorithmic analysis of nonlinear hybrid systems,'' in CAV 95: Computer-aided Verification (P. Wolper, ed.), Lecture Notes in Computer Science 939, pp. 225-238, Springer-Verlag, 1995.

24

T. Henzinger and H. Wong-Toi, ``Linear phase-portrait approximations for nonlinear hybrid systems.'' To appear in the Proceedings of the 1995 DIMACS Workshop on Verification and Control of Hybrid Systems, 1996.

25

O. Maler, A. Pnueli, and J. Sifakis, ``On the synthesis of discrete controllers for timed systems,'' in STACS 95 (E. Mayr and C. Puech, eds.), Lecture Notes in Computer Science 900, pp. 229-242, Springer-Verlag, 1995.

26

X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, ``An approach to the description and analysis of hybrid systems,'' in Hybrid System (R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, eds.), no. 736 in LNCS, pp. 149-178, New York: Springer Verlag, 1993.

27

T. Henzinger, P. Kopke, A. Puri, and P. Varaiya, ``What's decidable about hybrid automata,'' in Annual Symposium on the Theory of Computing, STOC'95, pp. 373-382, ACM Press, 1995.

28

R. P. Kurshan, Computer-aided verification of coordinating processes; the automata-theoretic approach. Princeton University Press, 1994.

29

C. Daws, A. Olivero, and S. Yovine, ``Verifying ET-LOTOS programs with KRONOS,'' in Proc. 7th. IFIP WG G.1 International Conference of Formal Description Techniques, FORTE'94 (D. Hogrefe and S. Leue, eds.), (Bern, Switzerland), pp. 227-242, Formal Description Techniques VII, Chapman & Hall, Oct. 1994.

30

T. A. Henzinger, P. H. Ho, and H. W. Toi, ``A user guide to HYTECH,'' in TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems (E. Brinksma, W. Cleaveland, K. Larsen, T. Margaria, and B. Steffen, eds.), no. 1019 in LNCS, pp. 41-71, Springer Verlag, 1995.

31

C. Heitmayer and N. Lynch, ``The generalized railroad crossing: A case study in formal verification of real-time systems,'' in Proc. ICCC Real-Time Systems Symposium, (San Juan, Puerto Rico), 1994.

32

Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety. New York: Springer-Verlag, 1995.

33

G. Pappas and S. Sastry, `` Straightening Rectangular Inclusions'', accepted to appear in Systems and Control Letters, 1998.

34

M. Branicky, E. Dolginova, and N. Lynch, ``A toolbox for proving and maintaining hybrid specifications.'' preprint, 1996. presented in Workshop on Hybrid Systems, Cornell University, October 12-16.

35

Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: specification. Berlin: Springer-Verlag, 1992.

36

N. Lynch, R. Segala, F. Vaandrager, and H. Weinberg, ``Hybrid I/O automata,'' in Hybrid Systems III, no. 1066 in LNCS, pp. 496-510, Springer Verlag, 1996.

37

C. Tomlin, G. Pappas, and S. Sastry, ``Conflict resolution for air traffic management: A case study in multi-agent hybrid systems,'' tech. rep., UCB/ERL M97/33, Electronics Research Laboratory, University of California, Berkeley, 1997. To appear in the IEEE Transactions on Automatic Control, Special Issue on Hybrid Systems, April 1998.

38

C. J. Tomlin, J. L. Lygeros and S. S. Sastry, ``Synthesizing Controllers for Nonlinear Hybrid Systems'', to appear in Hybrid Systems, Computation and Control, SPringer Verlag Lecture Notes in Computer Science, 1998.

39

A. Aiken, M. Fähndrich and Z. Su, "Detecting Races in Relay Ladder Logic Programs", Submitted for conference publication.

40

R. Alur and C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine, "The Algorithmic Analysis of Hybrid Systems", in Theoretical Computer Science, 1995, Vol. 138, pages 3-34.

41

R. W. Brockett, ``Hybrid models for motion control systems,'' in Perspectives in Control (H. Trentelman and J. Willems, eds.), Birkhäuser, 1993.

42

A. Nerode and W. Kohn, ``Models for hybrid systems: Automata, topologies, controllability, observability,'' in Hybrid System (R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, eds.), no. 736 in LNCS, pp. 317-356, New York: Springer Verlag, 1993.

43

M. S. Branicky, Control of Hybrid Systems. PhD thesis, Massachussets Institute of Technology, 1994.

44

L. Tavernini, ``Differential automata and their simulators,'' Nonlinear Analysis, Theory, Methods and Applications, vol. 11(6), pp. 665-683, 1987.

45

A. Deshpande, A. Gollu, and L. Semenzato, ``The SHIFT programming language and run-time system for dynamic networks of hybrid automata,'' Tech. Rep. UCB-ITS-PRR-97-7, Institute of Transportation Studies, University of California, Berkeley, 1997.

46

M. Anderson, D. Bruck, S. E. Mattsson, and T. Schonthal, ``Omsim- an integrated interactive environment for object-oriented modeling and simulation,'' in IEEE/IFAC joint symposium on computer aided control system design, pp. 285-90, 1994.

47

L. Hou, A. Michel, and H. Ye, ``Stability analysis of switched systems,'' in IEEE Conference on Decision and Control, pp. 1208-1214, 1996.

48

O. Maler, A. Pnueli, and J. Sifakis, ``On the synthesis of discrete controllers for timed systems,'' in Theoretical Aspects of Computer Science, no. 900 in LNCS, pp. 229-242, Springer Verlag, 1995.

49

M. Heymann, F. Lin, and G. Meyer, ``Control synthesis for a class of hybrid systems subject to configuration-based safety constraints,'' in Hybrid and Real Time Systems, no. 1201 in LNCS, pp. 376-391, Springer Verlag, 1997.

50

M. Lemmon, J. A. Stiver, and P. J. Antsaklis, ``Event identification and intelligent hybrid control,'' in Hybrid System (R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, eds.), no. 736 in LNCS, pp. 268-296, New York: Springer Verlag, 1993.

51

A. Nerode and W. Kohn, ``Multiple agent hybrid control architecture,'' in Hybrid System (R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, eds.), no. 736 in LNCS, pp. 297-316, New York: Springer Verlag, 1993.

52

J. Lygeros, D. N. Godbole, and S. Sastry, ``Multiagent hybrid system design using game theory and optimal control,'' in IEEE Conference on Decision and Control, pp. 1190-1195, 1996.

53

E.M. Clarke and E.A. Emerson, "Design and synthesis of synchronization skeletons using branching-time temporal logic", in Workshop on Logic of Programs, Springer Verlag Lecture Notes in Computer Science 131, 1981, pg. 52-71.

54

J. Queille and J. Sifakis, "Specification and verification of concurrent systems in CESAR'', in Fifth International Symposium on Programming, ed, Dezani-Ciancaglini, M. and U. Montanari, Springer Verlag Lecture Notes in Computer Science 137, 1981, pages 337-351.

55

J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and L.J. Hwang, "Symbolic model checking: states and beyond", Information and Computation, Vol. 98, 1992, pp. 142-170.

56

C. Daws, A. Olivero, S. Tripakis and S. Yovine, `` The tool KRONOS", in Hybrid Systems III, ed, R. Alur,T.A. Henzinger and E.D. Sontag, Springer Verlag Lecture Notes in Computer Science 1066, 1996, pages 208-219.

57

R. Alur and R.P. Kurshan, "Timing analysis in COSPAN", in Hybrid Systems III, ed, R. Alur,T.A. Henzinger and E.D. Sontag, Springer Verlag Lecture Notes in Computer Science 1066, 1996, pages 220-231.

58

J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, UPPAAL: a tool-suite for automatic verification of real-time systems, in Hybrid Systems III, ed, R. Alur,T.A. Henzinger and E.D. Sontag, Springer Verlag Lecture Notes in Computer Science 1066, 1996, pages 232-243.

59

D.L. Dill and Wong-Toi, H., "Verification of real-time systems by successive over- and underapproximation", in CAV 95: Computer-aided Verification, ed. P. Wolper, Lecture Notes in Computer Science 939, Springer-Verlag, 1995, pages 409-422

60

N. Halbwachs, P. Raymond and Y.-E. Proy, "Verification of linear hybrid systems by means of convex approximation", in SAS 94: Static Analysis Symposium, ed. B. LeCharlier, Lecture Notes in Computer Science 864, Springer-Verlag, 1994, pages 223-237

61

A. Deshpande, A. Göllü and L. Semenzato", "The SHIFT programming language and run-time system for dynamic networks of hybrid automata", PATH Report, 1996, www-path.eecs.berkeley.edu/shift/doc/ieeshift.ps.gz",

62

Jan Vitt and Josef Hooman, "Assertional specification and verification using PVS of the steam boiler control system", "Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control", in Springer Verlag, LNCS 1165, pages 453-472, 1996

63

R. Alur, T.A. Henzinger and O. Kupferman, "Alternating-time temporal logic", in Proceedings of the 38th Annual Symposium on Foundations of Computer Science 1997, pages 100-109.

64

T.A. Henzinger, O. Kupferman and S.K. Rajamani, "Fair simulation", CONCUR 97: Concurrency Theory, ed, A. Mazurkiewicz and J. Winkowski, Springer Verlag Lecture Notes in Computer Science 1243, 1997, pages 273-287.

65

R. Alur, T.A. Henzinger and S. Rajamani, "Efficient symbolic state exploration using transition hierarchies", in TACAS 98: Tools and Algorithms for the Construction and Analysis of Systems, Springer Verlag Lecture Notes in Computer Science, to appear, 1998.

66

T.A. Henzinger,P.-H. Ho and H. Wong-Toi, "Algorithmic analysis of nonlinear hybrid systems", IEEE Transactions on Automatic Control, 1998, to appear.

67

T.A. Henzinger and V. Rusu, ``Hybrid Automata in PVS", in Hybrid Systems 98: Computation and Control, Springer Verlag Lecture Notes in Computer Science, 1998, to appear.

68

S. Nadjm-Tehrani and J.-E. Strömberg", "Proving dynamic properties in an aerospace application", in Proceedings of the 16th Annual Real-time Systems Symposium, 1995, pages 2-10.

69

J.C. Corbett, ``Timing analysis of ADA tasking programs", IEEE Transactions on Software Engineering, volume 22, 1996, pp. 461-483.

70

T. Stauner and O. Müller and M. Fuchs, "Using HYTECH to verify an automotive control system", in HART 97: Hybrid and Real-time Systems, ed. O. Maler, Springer Verlag Lecture Notes in Computer Science 1201, 1997, pages 139-153.

71

T.A. Henzinger and P.-H. Ho, "HYTECH: The Cornell Hybrid Technology Tool", in Hybrid Systems II, ed. P. Antsaklis, A. Nerode,W. Kohn and S. Sastry, Springer Verlag Lecture Notes in Computer Science 999, 1995, pages 265-293.

72

T.A. Henzinger, P.-H. Ho and H. Wong-Toi, HYTECH: the next generation, in Proceedings of the 16th Annual Real-time Systems Symposium, IEEE Computer Society Press, 1995, pages 56-65.

73

T.A. Henzinger and H. Wong-Toi, ``Linear phase-portrait approximations for nonlinear hybrid systems", in Hybrid Systems III, Springer Verlag Lecture Notes in Computer Science, 1066, ed. R. Alur T.A. Henzinger and E.D. Sontag. 1996, pages 377-388.

74

T.A. Henzinger and H. Wong-Toi, "Using HYTECH to synthesize control parameters for a steam boiler", Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, ed. J.-R. Abrial and E. Börger and H. Langmaack, Springer Verlag Lecture Notes in Computer Science 1165, 1996, pages 265-282.