Skip to main content
SpringerLink
Log in

Time-Triggered Conversion of Guards for Reachability Analysis of Hybrid Automata

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10419))

Abstract

A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. We address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we prove the overapproximation error in the conversion can be made arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.

DISTRIBUTION A. Approved for public release; Distribution unlimited. (Approval AFRL PA #88ABW-2017-1923, 25 APR 2017).

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and 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

Institutional subscriptions

References

  1. Althoff, M.: An introduction to CORA 2015. In: Proceeding of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120–151 (2015)

    Google Scholar 

  2. Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Hybrid Systems: Computation and Control, HSCC 2012, Beijing, China, 17–19 April 2012, pp. 45–54 (2012)

    Google Scholar 

  3. Althoff, M., Le Guernic, C., Krogh, B.H.: Reachable set computation for uncertain time-varying linear systems. In: Hybrid Systems: Computation and Control, pp. 93–102 (2011)

    Google Scholar 

  4. Althoff, M., Rajhans, A., Krogh, B.H., Yaldiz, S., Li, X., Pileggi, L.: Formal verification of phase-locked loops using reachability analysis and continuization. In: Proceeding of the International Conference on Computer Aided Design, pp. 659–666 (2011)

    Google Scholar 

  5. Althoff, M., Stursberg, O., Buss, M.: Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Anal. Hybrid Syst. 4(2), 233–249 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  6. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138(1), 3–34 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bak, S.: Reducing the wrapping effect in flowpipe construction using pseudo-invariants. In: 4th ACM SIGBED International Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems (CyPhy 2014), pp. 40–43 (2014)

    Google Scholar 

  8. Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 155–164. ACM, New York (2016)

    Google Scholar 

  9. Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), pp. 128–133. ACM (2015)

    Google Scholar 

  10. Bak, S., Duggirala, P.S.: Direct verification of linear systems with over 10000 dimensions. In: 4th International Workshop on Applied Verification for Continuous and Hybrid Systems (2017)

    Google Scholar 

  11. Bak, S., Duggirala, P.S.: Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 173–178. ACM (2017)

    Google Scholar 

  12. Bak, S., Johnson, T.T.: Periodically-scheduled controller analysis using hybrid systems reachability and continuization. In: 36th IEEE Real-Time Systems Symposium (RTSS), San Antonio, Texas. IEEE Computer Society, December 2015

    Google Scholar 

  13. Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume-guarantee verification of nonlinear hybrid systems with ARIADNE. Int. J. Robust Nonlinear Control 24, 699–724 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  14. Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Cham (2014). doi:10.1007/978-3-319-13338-6_10

    Google Scholar 

  15. Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 479–494. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_35

    Chapter  Google Scholar 

  16. Bogomolov, S., Mitrohin, C., Podelski, A.: Composing reachability analyses of hybrid systems for safety and stability. In: Proceeding of the 8th International Symposium on Automated Technology for Verification and Analysis, pp. 67–81 (2010)

    Google Scholar 

  17. Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73–88. Springer, Heidelberg (2000). doi:10.1007/3-540-46430-1_10

    Chapter  Google Scholar 

  18. Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: complexity and fixed points. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 55–70. Springer, Cham (2013). doi:10.1007/978-3-319-02444-8_6

    Chapter  Google Scholar 

  19. Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: Bach 2: bounded reachability checker for compositional linear hybrid systems. In: Proceeding of Design, Automation & Test in Europe, pp. 1512–1517 (2010)

    Google Scholar 

  20. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_18

    Chapter  Google Scholar 

  21. Chen, X., Sankaranarayanan, S., Ábrahám, E.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceeding of the 33rd IEEE Real-Time Systems Symposium (2012)

    Google Scholar 

  22. Chen, X., Schupp, S., Makhlouf, I.B., Ábrahám, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 408–414. Springer, Cham (2015). doi:10.1007/978-3-319-17524-9_29

    Google Scholar 

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

    Google Scholar 

  24. Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71493-4_16

    Chapter  Google Scholar 

  25. Fränzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Methods Syst. Des. 30(3), 179–198 (2007)

    Article  MATH  Google Scholar 

  26. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31954-2_17

    Chapter  Google Scholar 

  27. Frehse, G., Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  28. Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187–200. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78929-1_14

    Chapter  Google Scholar 

  29. Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 203–212. ACM (2013)

    Google Scholar 

  30. Frehse, G., Ray, R.: Flowpipe-guard intersection for reachability computations with support functions. In: Proceeding of Analysis and Design of Hybrid Systems, pp. 94–101 (2012)

    Google Scholar 

  31. Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Proceeding of the 27th International Conference on Computer Aided Verification, pp. 212–226 (2010)

    Google Scholar 

  32. Girard, A., Le Guernic, C.: Efficient reachability analysis for linear systems using support functions. In: Proceeding of the 17th IFAC World Congress, pp. 8966–8971 (2008)

    Google Scholar 

  33. Girard, A., Guernic, C.: Zonotope/Hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215–228. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78929-1_16

    Chapter  Google Scholar 

  34. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: the next generation. In: Proceeding. of the 16th IEEE Real-Time Systems Symposium, pp. 56–65 (1995)

    Google Scholar 

  35. Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceeding of the Conference on Certified Programs and Proofs, pp. 129–136 (2015)

    Google Scholar 

  36. Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Proceeding of Tools and Algorithms for the Construction and Analysis of Systems, pp. 200–205 (2015)

    Google Scholar 

  37. Kurzhanski, A., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Dayawansa, W.P., Lindquist, A., Zhou, Y. (eds.) New Directions and Applications in Control Theory, vol. 321, pp. 193–205. Springer, Heidelberg (2005). doi:10.1007/10984413_12

    Chapter  Google Scholar 

  38. Lagerberg, A.: A benchmark on hybrid control of an automotive powertrain with backlash. Technical report R005/2007, Signals and Systems, Chalmers University of Technology (2007)

    Google Scholar 

  39. Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  40. Maïga, M., Ramdani, N., Travé-Massuyès, L., Combastel, C.: A CSP versus a zonotope-based method for solving guard set intersection in nonlinear hybrid reachability. Math. Comput. Sci. 8, 407–423 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  41. Mitchell, I.M., Susuki, Y.: Level set methods for computing reachable sets of hybrid systems with differential algebraic equation dynamics. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 630–633. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78929-1_51

    Chapter  Google Scholar 

  42. Nordin, M., Gutman, P.-O.: Controlling mechanical systems with backlash - a survey. Automatica 38, 1633–1649 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  43. Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14509-4

    Book  MATH  Google Scholar 

  44. Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5(2), 149–162 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  45. Schupp, S., Ábrahám, E., Chen, X., Ben Makhlouf, I., Frehse, G., Sankaranarayanan, S., Kowalewski, S.: Current challenges in the verification of hybrid systems. In: Proceeding of the Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, pp. 8–24 (2015)

    Google Scholar 

  46. Smirnov, G.V.: Introduction to the Theory of Differential Inclusions. American Mathematical Society (2002)

    Google Scholar 

Download references

Acknowledgment

This work was partly supported by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems), the German Research Foundation (DFG) grant number AL 1185/5-1, and the Air Force Office of Scientific Research (AFOSR).

Author information

Authors and Affiliations

  1. Air Force Research Laboratory, Dayton, OH, USA

    Stanley Bak

  2. Australian National University, Canberra, Australia

    Sergiy Bogomolov

  3. Technische Universität München, Munich, Germany

    Matthias Althoff

Authors
  1. Stanley Bak
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sergiy Bogomolov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matthias Althoff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stanley Bak .

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, United Kingdom

    Alessandro Abate

  2. Dept. d’Informatique, Université Libre de Bruxelles, Brussels, Belgium

    Gilles Geeraerts

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bak, S., Bogomolov, S., Althoff, M. (2017). Time-Triggered Conversion of Guards for Reachability Analysis of Hybrid Automata. In: Abate, A., Geeraerts, G. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2017. Lecture Notes in Computer Science(), vol 10419. Springer, Cham. https://doi.org/10.1007/978-3-319-65765-3_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65765-3_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65764-6

  • Online ISBN: 978-3-319-65765-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation