Asynchronous Correspondences Between Hybrid Trajectory Semantics | SpringerLink
Skip to main content
Springer Nature Link
Log in

Asynchronous Correspondences Between Hybrid Trajectory Semantics

  • Chapter
  • First Online:
Principles of Systems Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13660))

Abstract

We formalize the semantics of hybrid systems as sets of hybrid trajectories, including those generated by an hybrid transition system. We study the abstraction of hybrid trajectory semantics for verification, static analysis, and refinement. We mainly consider abstractions of hybrid semantics which establish a correspondence between trajectories derived from a correspondence between states such as homomorphisms, simulations, bisimulations, and preservations with progress. We also consider abstractions that cannot be defined stepwise like discretization. All these abstractions are Galois connections between concrete and abstract hybrid trajectory or discrete trace semantics. In contrast to semantic based abstractions, we investigate the problematic trace-based composition of abstractions.

\({{\textit{Dedicated to Thomas Henzinger}} {}}\)

for his 60 \({}^{\textit{th}}\) birthday

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 10295
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12869
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    see an introduction in [11, Ch. 11].

  2. 2.

    Underlined equation or theorem numbers link to proofs given in the ArXiv version.

  3. 3.

    One could argue that the time-evolution low abstraction of (17) applied to the concrete and abstract trajectories would solve the problem of having the same timeline by merging the trajectories into a single configuration, but then the original timelines are hidden in the flow functions, which does not make time-dependent reasonings simpler.

References

  1. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)

    Article  Google Scholar 

  4. Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_1

    Chapter  MATH  Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  6. Banach, R., Butler, M.J., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92–123 (2015)

    Article  Google Scholar 

  7. Caspi, P., Halbwachs, N.: An approach to real time systems modeling. In: ICDCS. IEEE Computer Society, pp. 710–716 (1982)

    Google Scholar 

  8. Chen, X., Sankaranarayanan, S.: Reachability analysis for cyber-physical systems: are we there yet? In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0_6

    Chapter  Google Scholar 

  9. Cheng, Z., Méry, D.: A refinement strategy for hybrid system design with safety constraints. In: Attiogbé, C., Ben Yahia, S. (eds.) MEDI 2021. LNCS, vol. 12732, pp. 3–17. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78428-7_1

    Chapter  Google Scholar 

  10. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1–2), 47–103 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  11. Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)

    MATH  Google Scholar 

  12. D’Innocenzo, A., Julius, A.A., Pappas, G.J., Di Benedetto, M.D., Di Gennaro, S.: Verification of temporal properties on hybrid automata by simulation relations. In: CDC, pp. 4039–4044. IEEE (2007)

    Google Scholar 

  13. Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic rectangular refinement of affine hybrid systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 144–161. Springer, Heidelberg (2005). https://doi.org/10.1007/11603009_13

    Chapter  MATH  Google Scholar 

  14. Frehse, G.: On timed simulation relations for hybrid systems and compositionality. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 200–214. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_15

    Chapter  MATH  Google Scholar 

  15. Girard, A., Julius, A.A., Pappas, G.J.: Approximate simulation relations for hybrid systems. Discret. Event Dyn. Syst. 18(2), 163–179 (2008). https://doi.org/10.1007/s10626-007-0029-9

    Article  MathSciNet  MATH  Google Scholar 

  16. Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control. 17(5–6), 568–578 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  17. Henzinger, T.A., Ho, P.-H.: A note on abstract interpretation strategies for hybrid automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 252–264. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60472-3_13

    Chapter  Google Scholar 

  18. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: STOC, pp. 373–382. ACM (1995)

    Google Scholar 

  19. Isaacson, E., Keller, H.B.: Analysis of Numerical Methods. Dover, Mineola (1994)

    MATH  Google Scholar 

  20. Katok, A., Hasselblatt, B.: Introduction to the Theory of Dynamical Systems. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  21. Lang, S.: Undergraduate Analysis, 2nd edn. Springer, Heidelberg (1997)

    Book  MATH  Google Scholar 

  22. Liberzon, D.: Switching in Systems and Control. Birkhäuser, Basel (2003)

    Book  MATH  Google Scholar 

  23. Lynch, N.: Simulation techniques for proving properties of real-time systems. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 375–424. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58043-3_24

    Chapter  Google Scholar 

  24. MathWorks. Simulation and model-based design. https://www.mathworks.com/products/simulink.html (2022)

  25. Meinicke, L., Hayes, I.J.: Continuous action system refinement. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 316–337. Springer, Heidelberg (2006). https://doi.org/10.1007/11783596_19

    Chapter  Google Scholar 

  26. Milner, R.: An algebraic definition of simulation between programs. In: Proceedings IJCAI, vol. 1971, pp. 481–489 (1971)

    Google Scholar 

  27. Milner, R.: Communication and Concurrency. PHI Series in Computer Science, Prentice Hall, Hoboken (1989)

    MATH  Google Scholar 

  28. Nyquist, H.: Certain topics in telegraph transmission theory. Proc. IEEE 47(2), 617–644 (1928)

    Google Scholar 

  29. Proakis, J.G., Manolakis, D.G.: Digital Signal Processing. Pearson, 4th (edn) (2006)

    Google Scholar 

  30. Robinson, J.C.: An Introduction to Ordinary Differential Equations. Cambridge University Press, Cambridge (2004)

    Book  MATH  Google Scholar 

  31. Rökkö, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theor. Comput. Sci. 290(1), 937–973 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  32. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)

    Book  MATH  Google Scholar 

  33. Shannon, C.E.: Communication in the presence of noise. In: Proceedings of the I.R.E., pp. 10–21 (1949)

    Google Scholar 

  34. Shmuely, Z.: The structure of Galois connections. Pac. J. Math. 54(2), 209–225 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  35. Wen, S., Abrial, J.-R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 94, 164–202 (2014)

    Article  Google Scholar 

  36. Tan, Y.K., Platzer, A.: An axiomatic approach to liveness for differential equations. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 371–388. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_23

    Chapter  Google Scholar 

  37. Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pacific J. of Math. 5, 285–310 (1955)

    Article  MathSciNet  MATH  Google Scholar 

  38. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  39. Zhang, J., Johansson, K.H., Lygeros, J., Sastry, S.: Dynamical systems revisited: hybrid systems with Zeno executions. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 451–464. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46430-1_37

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

I thank Dominique Méry for his suggestions and encouragements, “la discrétisation, c’est coton”. I thank the two anonymous referees for their constructive criticisms.

Author information

Authors and Affiliations

  1. CS, CIMS, New York University, New York, USA

    Patrick Cousot

Authors
  1. Patrick Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Patrick Cousot .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Jean-François Raskin

  2. Institute of Science and Technology Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee

  3. École Normale Supérieure Paris-Saclay, Gif-sur-Yvette, France

    Laurent Doyen

  4. MPI for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Cousot, P. (2022). Asynchronous Correspondences Between Hybrid Trajectory Semantics. In: Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds) Principles of Systems Design. Lecture Notes in Computer Science, vol 13660. Springer, Cham. https://doi.org/10.1007/978-3-031-22337-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-22337-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-22336-5

  • Online ISBN: 978-3-031-22337-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics