Skip to main content
SpringerLink
Log in

Computational Techniques for the Verification and Control of Hybrid Systems

  • Conference paper
Multidisciplinary Methods for Analysis Optimization and Control of Complex Systems

Part of the book series: Mathematics in Industry ((TECMI,volume 6))

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior. Princeton University Press, 1947.

    Google Scholar 

  2. A. Church, “Logic, arithmetic, and automata,” in Proceedings of the International Congress of Mathematicians, pp. 23–35, 1962.

    Google Scholar 

  3. R. Isaacs, Differential Games. John Wiley, 1967.

    Google Scholar 

  4. S. Osher and J. A. Sethian, “Fronts propagating with curvature-dependent speed: Algorithms based on Hamilton-Jacobi formulations,” Journal of Computational Physics, vol. 79, pp. 12–49, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  5. I. Mitchell, A. M. Bayen, and C. J. Tomlin, “Computing reachable sets for continuous dynamic games using level set methods,” IEEE Transactions on Automatic Control, December 2001. Submitted.

    Google Scholar 

  6. C. J. Tomlin, J. Lygeros, and S. Sastry, “A game theoretic approach to controller design for hybrid systems,” Proceedings of the IEEE, vol. 88, no. 7, pp. 949–970, July 2000.

    Article  Google Scholar 

  7. I. Mitchell, Application of Level Set Methods to Control and Reachability Problems in Continuous and Hybrid Systems. PhD thesis, Scientific Computing and Computational Mathematics, Stanford University, August 2002.

    Google Scholar 

  8. A. M. Bayen, I. Mitchell, M. Oishi, and C. J. Tomlin, “Automatic envelope protection and cockpit interface analysis of an autoland system using hybrid system theory.” Submitted to the AIAA Journal of Guidance, Control, and Dynamics, December 2002.

    Google Scholar 

  9. M. Oishi, I. Mitchell, A. M. Bayen, C. J. Tomlin, and A. Degani, “Hybrid verification of an interface for an automatic landing,” in Proceedings of the IEEE Conference on Decision and Control, (Las Vegas, NV), December 2002.

    Google Scholar 

  10. M. Oishi, C. J. Tomlin, and A. Degani, “Verification of user interfaces for hybrid systems.” Submitted as a NASA Technical Memorandum, Ames Research Center, November 2002.

    Google Scholar 

  11. S. S. Sastry, Nonlinear Systems: Analysis, Stability and Control. New York: Springer Verlag, 1999.

    MATH  Google Scholar 

  12. J. Doyle, B. Francis, and A. Tannenbaum, Feedback Control Theory. New York: Macmillan, 1992.

    Google Scholar 

  13. P. J. G. Ramadge and W. M. Wonham, “The control of discrete event dynamical systems,” Proceedings of the IEEE, vol. Vol. 77, no. 1, pp. 81–98, 1989.

    Article  Google Scholar 

  14. J. R. Büchi and L. H. Landweber, “Solving sequential conditions by finite-state operators,” in Proceedings of the American Mathematical Society, pp. 295–311, 1969.

    Google Scholar 

  15. C. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. Boston: Kluwer, 1999.

    MATH  Google Scholar 

  16. R. Brockett, “Hybrid models for motion control systems,” in Perspectives in Control (H. Trentelman and J. Willems, eds.), pp. 29–54, Boston: Birkhauser, 1993.

    Google Scholar 

  17. M. S. Branicky, Control of Hybrid Systems. PhD thesis, Department of Electrical Engineering and Computer Sciences, Massachusetts Institute of Technology, 1994.

    Google Scholar 

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

    Google Scholar 

  19. A. Nerode and W. Kohn, “Models for hybrid systems: Automata, topologies, controllability, observability,” in Hybrid Systems (R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, eds.), LNCS 736, pp. 317–356, New York: Springer Verlag, 1993.

    Google Scholar 

  20. R. Alur and D. Dill, “A theory of timed automata,” Theoretical Computer Science, vol. 126, pp. 183–235, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  21. R. Alur, C. Courcoubetis, T. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, “The algorithmic analysis of hybrid systems,” in Proceedings of the 11th International Conference on Analysis and Optimization of Systems: Discrete-event Systems (G. Cohen and J.-P. Quadrat, eds.), no. 199 in LNCS, pp. 331–351, Springer Verlag, 1994.

    Google Scholar 

  22. 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.

    Google Scholar 

  23. A. Puri and P. Varaiya, “Decidability of hybrid systems with rectangular differential inclusions,” in CAV94: Computer-Aided Verification, no. 818 in LNCS, pp. 95–104, Stanford, CA: Springer Verlag, 1995.

    Google Scholar 

  24. O. Shakernia, G. J. Pappas, and S. S. Sastry, “Decidable controller synthesis for classes of linear systems,” in Hybrid Systems: Computation and Control (B. Krogh and N. Lynch, eds.), LNCS 1790, pp. 407–420, Springer Verlag, 2000.

    Google Scholar 

  25. N. Lynch, R. Segala, and F. Vaandraager, “Hybrid I/O automata,” 2002. Submitted. Also, Technical Report MIT-LCS-TR-827b, MIT Laboratory for Computer Science, Cambridge, MA 02139.

    Google Scholar 

  26. D. L. Dill, “The Murφ verification system,” in Conference on Computer-Aided Verification, LNCS, pp. 390–393, Springer-Verlag, July 1996.

    Google Scholar 

  27. S. Owre, J. M. Rushby, and N. Shankar, “PVS: A prototype verification system,” in 11th International Conference on Automated Deduction (CADE) (D. Kapur, ed.), vol. 607 of Lecture Notes in Artificial Intelligence, (Saratoga, NY), pp. 748–752, Springer-Verlag, June 1992.

    Google Scholar 

  28. J. Burch, E. M. Clarke, K. McMillan, D. Dill, and L. Hwang, “Symbolic model checking: 1020 states and beyond,” Information and Computation, vol. 98, pp. 142–170, June 1992.

    Article  MathSciNet  MATH  Google Scholar 

  29. G. Holzmann, “The model checker Spin,” IEEE Transactions on Software Engineering, vol. 23, pp. 279–295, May 1997. Special issue on Formal Methods in Software Practice.

    Article  Google Scholar 

  30. M. G. Crandall, L. C. Evans, and P.-L. Lions, “Some properties of viscosity solutions of Hamilton-Jacobi equations,” Transactions of the American Mathematical Society, vol. 282, no. 2, pp. 487–502, 1984.

    MathSciNet  MATH  Google Scholar 

  31. S. Osher and R. Fedkiw, The Level Set Method and Dynamic Implicit Surfaces. Springer-Verlag, 2002.

    Google Scholar 

  32. G.-S. Jiang and D. Peng, “Weighted ENO schemes for Hamilton-Jacobi equations,” SIAM Journal on Scientific Computing, vol. 21, pp. 2126–2143, 2000.

    Article  MathSciNet  MATH  Google Scholar 

  33. S. Osher and C.-W. Shu, “High-order essentially nonoscillatory schemes for Hamilton-Jacobi equations,” SIAM Journal of Numerical Analysis, vol. 28, no. 4, pp. 907–922, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  34. J. A. Sethian, Level Set Methods and Fast Marching Methods. New York: Cambridge University Press, 1999.

    MATH  Google Scholar 

  35. M. G. Crandall and P.-L. Lions, “Two approximations of solutions of Hamilton-Jacobi equations,” Mathematics of Computation, vol. 43, no. 167, pp. 1–19, 1984.

    MathSciNet  MATH  Google Scholar 

  36. C.-W. Shu and S. Osher, “Efficient implementation of essentially non-oscillatory shock-capturing schemes,” Journal of Computational Physics, vol. 77, pp. 439–471, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  37. I. Mitchell, A. M. Bayen, and C. J. Tomlin, “Validating a Hamilton-Jacobi approximation to hybrid system reachable sets,” in Hybrid Systems: Computation and Control (M. D. D. Benedetto and A. Sangiovanni-Vincentelli, eds.), LNCS 2034, pp. 418–432, Springer Verlag, 2001.

    Google Scholar 

  38. T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata,” in Proceedings of the 27th Annual ACM Symposium on Theory of Computing, 1995.

    Google Scholar 

  39. K. Larsen, P. Pettersson, and W. Yi, “Uppaal in a nutshell,” Software Tools for Technology Transfer, vol. 1, 1997.

    Google Scholar 

  40. S. Yovine, “Kronos: A verification tool for real-time systems,” Software Tools for Technology Transfer, vol. 1, pp. 123–133, 1997.

    Article  MATH  Google Scholar 

  41. R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho, “Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems,” in Hybrid Systems (R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, eds.), LNCS, pp. 366–392, New York: Springer Verlag, 1993.

    Google Scholar 

  42. T. A. Henzinger, P. Ho, and H. Wong-Toi, “HyTech: A model checker for hybrid systems,” Software Tools for Technology Transfer, vol. 1, pp. 110–122, 1997.

    MATH  Google Scholar 

  43. O. Maler, A. Pnueli, and J. Sifakis, “On the synthesis of discrete controllers for timed systems,” in STACS 95: Theoretical Aspects of Computer Science (E. W. Mayr and C. Puech, eds.), no. 900 in LNCS, pp. 229–242, Munich: Springer Verlag, 1995.

    Google Scholar 

  44. E. Asarin, O. Maler, and A. Pnueli, “Symbolic controller synthesis for discrete and timed systems,” in Proceedings of Hybrid Systems II, Volume 999 of LNCS (P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, eds.), Cambridge: Springer Verlag, 1995.

    Google Scholar 

  45. H. Wong-Toi, “The synthesis of controllers for linear hybrid automata,” in Proceedings of the IEEE Conference on Decision and Control, (San Diego, CA), 1997.

    Google Scholar 

  46. A. Bemporad and M. Morari, “Verification of hybrid systems via mathematical programming,” in Hybrid Systems: Computation and Control (F. Vaandrager and J. H. van Schuppen, eds.), no. 1569 in LNCS, pp. 30–45, Berlin: Springer Verlag, 1999.

    Google Scholar 

  47. P. Cardaliaguet, M. Quincampoix, and P. Saint-Pierre, “Set-valued numerical analysis for optimal control and differential games,” in Stochastic and Differential Games: Theory and Numerical Methods (M. Bardi, T. Parthasarathy, and T. E. S. Raghavan, eds.), vol. 4 of Annals of International Society of Dynamic Games, Birkhäuser, 1999.

    Google Scholar 

  48. J.-P. Aubin, J. Lygeros, M. Quincampoix, S. Sastry, and N. Seube, “Impulse differential inclusions: A viability approach to hybrid systems,” IEEE Transactions on Automatic Control, vol. 47, no. 1, pp. 2–20, 2002.

    Article  MathSciNet  Google Scholar 

  49. A. M. Bayen, E. Crück, and C. J. Tomlin, “Guaranteed overapproximation of unsafe sets for continuous and hybrid systems: Solving the Hamilton-Jacobi equation using viability techniques,” in Hybrid Systems: Computation and Control (C. J. Tomlin and M. R. Greenstreet, eds.), LNCS 2289, pp. 90–104, Springer Verlag, 2002.

    Google Scholar 

  50. T. Dang, Vérification et synthèse des systèmes hybrides. PhD thesis, Institut National Polytechnique de Grenoble (Verimag), 2000.

    Google Scholar 

  51. E. Asarin, O. Bournez, T. Dang, and O. Maler, “Approximate reachability analysis of piecewise-linear dynamical systems,” in Hybrid Systems: Computation and Control (B. Krogh and N. Lynch, eds.), LNCS 1790, pp. 21–31, Springer Verlag, 2000.

    Google Scholar 

  52. A. Chutinan and B. H. Krogh, “Verification of infinite-state dynamic systems using approximate quotient transition systems,” IEEE Transactions on Automatic Control, vol. 46, no. 9, pp. 1401–1410, 2001.

    MathSciNet  MATH  Google Scholar 

  53. O. Botchkarev and S. Tripakis, “Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations,” in Hybrid Systems: Computation and Control (B. Krogh and N. Lynch, eds.), LNCS 1790, pp. 73–88, Springer Verlag, 2000.

    Google Scholar 

  54. R. Vidal, S. Schaffert, J. Lygeros, and S. S. Sastry, “Controlled invariance of discrete time systems,” in Hybrid Systems: Computation and Control (B. Krogh and N. Lynch, eds.), LNCS 1790, pp. 437–450, Springer Verlag, 2000.

    Google Scholar 

  55. A. Balluchi, M. D. Benedetto, C. Pinello, C. Rossi, and A. Sangionvanni-Vincentelli, “Hybrid control for automotive engine management: The cut-off case,” in Hybrid Systems: Computation and Control (T. Henzinger and S. Sastry, eds.), no. 1386 in LNCS, pp. 13–32, New York: Springer Verlag, 1998.

    Google Scholar 

  56. Esprit, “Verification of Hybrid Systems: Results of a European Union Esprit Project,” in European Journal of Control (O. Maler, ed.), Vol. 7, Issue 4, 2001.

    Google Scholar 

  57. C. J. Tomlin, I. Mitchell, and R. Ghosh, “Safety verification of conflict resolution maneuvers,” IEEE Transactions on Intelligent Transportation Systems, vol. 2, no. 2, pp. 110–120, 2001. June.

    Article  Google Scholar 

  58. M. Oishi, C. J. Tomlin, V. Gopal, and D. Godbole, “Addressing multiobjective control: Safety and performance through constrained optimization,” in Hybrid Systems: Computation and Control (M. D. D. Benedetto and A. Sangiovanni-Vincentelli, eds.), LNCS 2034, pp. 459–472, Springer Verlag, 2001.

    Google Scholar 

  59. T. Dang and O. Maler, “Reachability analysis via face lifting,” in Hybrid Systems: Computation and Control (S. Sastry and T. Henzinger, eds.), no. 1386 in LNCS, pp. 96–109, Springer Verlag, 1998.

    Google Scholar 

  60. A. Degani, Modeling Human-Machine Systems: On Modes, Error, and Patterns of Interaction. PhD thesis, Department of Industrial and Systems Engineering, Georgia Institute of Technology, 1996.

    Google Scholar 

  61. C. J. Tomlin, Hybrid Control of Air Traffic Management Systems. PhD thesis, Department of Electrical Engineering, University of California, Berkeley, 1998.

    Google Scholar 

  62. I. M. Kroo, Aircraft Design: Synthesis and Analysis. Stanford, California: Desktop Aeronautics Inc., 1999.

    Google Scholar 

  63. J. Anderson, Fundamentals of Aerodynamics. New York: McGraw Hill Inc., 1991.

    Google Scholar 

  64. United States Federal Aviation Administration, Federal Aviation Regulations, 1990. Section 25.125 (landing).

    Google Scholar 

  65. T. Lambregts, “Automatic flight control: Concepts and methods.” FAA National Resource Specialist, Advanced Controls, 1995.

    Google Scholar 

  66. I. Hwang, D. Stipanovic, and C. Tomlin, “Polyhedral reachable sets for continuous and hybrid systems.” Submitted to the 2003 American Control Conference, August 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Hybrid Systems Laboratory, Department of Aeronautics and Astronautics, Stanford University, Stanford, CA, 94305-4035, USA

    Claire J. Tomlin, Alexandre M. Bayen & Meeko K. M. Oishi

  2. Computer Science Department, University of British Columbia, Vancouver, BC, CANADA, V6T 1Z4

    Ian M. Mitchell

Authors
  1. Claire J. Tomlin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ian M. Mitchell
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandre M. Bayen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Meeko K. M. Oishi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. MIRIAM & Department of Mathematics, University of Milano, Via C. Saldini 50, 20133, Milano, Italy

    Vincenzo Capasso

  2. Pole Scientifique — Dassault Aviation, UPMC Dassault Aviation, 78 Quai Marcel Dassault, 99214, Saint-Cloud, France

    Jacques Périaux

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tomlin, C.J., Mitchell, I.M., Bayen, A.M., Oishi, M.K.M. (2005). Computational Techniques for the Verification and Control of Hybrid Systems. In: Capasso, V., Périaux, J. (eds) Multidisciplinary Methods for Analysis Optimization and Control of Complex Systems. Mathematics in Industry, vol 6. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-27167-8_3

Download citation

Publish with us

Policies and ethics

Search

Navigation