Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2012: FM 2012: Formal Methods pp 471–485Cite as

A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7436))

Abstract

We propose an approach to reduce the optimal controller synthesis problem of hybrid systems to quantifier elimination; furthermore, we also show how to combine quantifier elimination with numerical computation in order to make it more scalable but at the same time, keep arising errors due to discretization manageable and within bounds. A major advantage of our approach is not only that it avoids errors due to numerical computation, but it also gives a better optimal controller. In order to illustrate our approach, we use the real industrial example of an oil pump provided by the German company HYDAC within the European project Quasimodo as a case study throughout this paper, and show that our method improves (up to 7.5%) the results reported in [4] based on game theory and model checking.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Asarin, E., Bournez, O., Dang, T., Maler, O., Pnueli, A.: Effective synthesis of switching controllers for linear systems. Proc. of the IEEE 88(7), 1011–1025 (2000)

    Article  Google Scholar 

  2. Bemporad, A., Morari, M., Dua, V., Pistikopoulos, E.N.: The explicit linear quadratic regulator for constrained systems. Automatica 38(1), 3–20 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  3. Brown, C.W.: QEPCAD B: A program for computing with semi-algebraic sets using CADs. SIGSAM Bulletin 37, 97–108 (2003)

    Article  MATH  Google Scholar 

  4. Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 90–104. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Chatterjee, K., de Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics (full version). Logical Methods in Computer Science 6(3) (2010), http://arxiv.org/abs/0809.4326

  6. Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1-2), 29–35 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  7. Dolzmann, A., Seidl, A., Sturm, T.: Redlog User Manual, 3.1 edition for redlog Version 3.06 (reduce 3.8) (November 2006), http://redlog.dolzmann.de/downloads/

  8. Dolzmann, A., Sturm, T., Weispfenning, V.: Real Quantifier Elimination in Practice. In: Algorithmic Algebra and Number Theory, pp. 221–247. Springer, Heidelberg (1998)

    Google Scholar 

  9. Fotiou, I.A., Rostalski, P., Parrilo, P.A., Morari, M.: Parametric optimization and optimal control using algebraic geometry methods. International Journal of Control 79(11), 1340–1358 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)

    Article  MathSciNet  Google Scholar 

  11. Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Hearn, A.C.: Reduce User’s Manual (February 2004), http://reduce-algebra.com/docs/reduce.pdf , version 3.8

  13. Henzinger, T., Ho, P.H., Wong-Toi, H.: HyTech: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  14. Jensen, P.A., Bard, J.F.: Operations Research Models and Methods. John Wiley & Sons (October 2002)

    Google Scholar 

  15. Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT 2011, pp. 107–116. ACM, New York (2011)

    Google Scholar 

  16. Kanno, M., Yokoyama, K., Anai, H., Hara, S.: Symbolic optimization of algebraic functions. In: ISSAC 2008, pp. 147–154. ACM, New York (2008)

    Chapter  Google Scholar 

  17. Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106. ACM, New York (2011)

    Google Scholar 

  18. Loos, R., Weispfenning, V.: Applying linear quantifier elimination. The Computer Journal 36(5), 450–462 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  19. Monniaux, D.: Mjollnir-2009-07-10, http://www-verimag.imag.fr/~monniaux/mjollnir.html

  20. Monniaux, D.: A Quantifier Elimination Algorithm for Linear Real Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Platzer, A., Clarke, E.M.: Computing Differential Invariants of Hybrid Systems as Fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176–189. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Platzer, A., Clarke, E.M.: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing Invariants for Hybrid Systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539–554. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  24. Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: ISSAC 2011, pp. 329–336. ACM, New York (2011)

    Google Scholar 

  25. Taly, A., Gulwani, S., Tiwari, A.: Synthesizing Switching Logic Using Constraint Solving. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 305–319. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Taly, A., Tiwari, A.: Switching logic synthesis for reachability. In: EMSOFT 2010, pp. 19–28. ACM, New York (2010)

    Google Scholar 

  27. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)

    MATH  Google Scholar 

  28. Tomlin, C.J., Lygeros, J., Sastry, S.S.: A game theoretic approach to controller design for hybrid systems. Proc. of the IEEE 88(7), 949–970 (2000)

    Article  Google Scholar 

  29. Weispfenning, V.: Parametric linear and quadratic optimization by elimination. Tech. rep., Fakultät für Mathematik und Informatik, Universität Passau (1994)

    Google Scholar 

  30. Zhao, H., Zhan, N., Kapur, D., Larsen, K.G.: A “hybrid” approach for synthesizing optimal controllers of hybrid systems: A case study of the oil pump industrial example. CoRR abs/1203.6025 (2012), http://arxiv.org/abs/1203.6025

Download references

Author information

Authors and Affiliations

  1. State Key Lab. of Comput. Sci., Institute of Software, CAS, Beijing, China

    Hengjun Zhao

  2. Graduate University of Chinese Academy of Sciences, Beijing, China

    Hengjun Zhao & Naijun Zhan

  3. Dept. of Comput. Sci., University of New Mexico, Albuquerque, NM, USA

    Deepak Kapur

  4. CISS, CS, Aalborg University, Denmark

    Kim G. Larsen

Authors
  1. Hengjun Zhao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Deepak Kapur
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Ames Research Center, 94035, Moffett Field, CA, USA

    Dimitra Giannakopoulou

  2. Université de Lorraine LORIA, BP 239, 54506, Vandoeuvre lès Nancy, France

    Dominique Méry

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhao, H., Zhan, N., Kapur, D., Larsen, K.G. (2012). A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_38

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32759-9_38

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32758-2

  • Online ISBN: 978-3-642-32759-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation