Skip to main content
SpringerLink
Log in

Implementing Hybrid Semantics: From Functional to Imperative

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2020 (ICTAC 2020)

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

Included in the following conference series:

Abstract

Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HybCore with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HybCore as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HybCore, whose semantics is simpler and runnable, and yet intimately related with the semantics of HybCore at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCi for Haskell and UTop for OCaml. The major asset of our implementation is that it formally follows the operational semantic rules.

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. Adámek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories. Wiley, New York (1990)

    MATH  Google Scholar 

  2. Adámek, J., Milius, S., Velebil, J.: Elgot theories: a new perspective on the equational properties of iteration. Math. Structures Comput. Sci. 21(2), 417–480 (2011)

    Article  MathSciNet  Google Scholar 

  3. Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. In: ACM SIGPLAN Notices, vol. 47, pp. 129–138. ACM (2012)

    Google Scholar 

  4. Broman, D.: Hybrid simulation safety: limbos and zero crossings. In: Lohstroh, M., Derler, P., Sirjani, M. (eds.) Principles of Modeling. LNCS, vol. 10760, pp. 106–121. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95246-8_7

    Chapter  Google Scholar 

  5. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MathSciNet  Google Scholar 

  6. Copp, D.A., Sanfelice, R.G.: A zero-crossing detection algorithm for robust simulation of hybrid systems jumping on surfaces. Simulation Modell. Pract. Theory 68, 1–17 (2016)

    Article  Google Scholar 

  7. Diezel, T.L., Goncharov, S.: Towards constructive hybrid semantics. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), vol. 167 of LIPIcs, pp. 24:1–24:19, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik

    Google Scholar 

  8. Elgot, C.: Monadic computation and iterative algebraic theories. In: Studies in Logic and the Foundations of Mathematics, vol. 80, pp. 175–230. Elsevier (1975)

    Google Scholar 

  9. Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J.: Towards a UTP semantics for modelica. In: Bowen, J.P., Zhu, H. (eds.) UTP 2016. LNCS, vol. 10134, pp. 44–64. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52228-9_3

    Chapter  Google Scholar 

  10. Fritzson, P.: Principles of object-oriented modeling and simulation with Modelica 3.3: a cyber-physical approach. Wiley, New York (2014)

    Google Scholar 

  11. Goebel, R., Sanfelice, R.G., Teel, A.R.: Hybrid dynamical systems. IEEE Control Syst. 29(2), 28–93 (2009)

    Article  MathSciNet  Google Scholar 

  12. Goncharov, S., Jakob, J., Neves, R.: A semantics for hybrid iteration. In: 29th International Conference on Concurrency Theory, CONCUR 2018. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)

    Google Scholar 

  13. Goncharov, S., Jakob, J., Neves, R.: A semantics for hybrid iteration. CoRR, abs/1807.01053 (2018)

    Google Scholar 

  14. Goncharov, S., Neves, R.: An adequate while-language for hybrid computation. In: Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019, PPDP 2019, pp. 11:1–11:15, New York, NY, USA, ACM (2019)

    Google Scholar 

  15. Goncharov, S., Neves, R., Proença, J.: Implementing hybrid semantics: From functional to imperative. CoRR, abs/2009.14322 (2020)

    Google Scholar 

  16. Goncharov, S., Schröder, L., Rauch, C., Piróg, M.: Unifying guarded and unguarded iteration. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 517–533. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_30

    Chapter  MATH  Google Scholar 

  17. Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996: Logic in Computer Science, 11th Annual Symposium, New Jersey, USA, July 27–30, 1996, pp. 278–292. IEEE (1996)

    Google Scholar 

  18. Höfner, P., Möller, B.: An algebra of hybrid systems. J. Logic Algebraic Programm. 78(2), 74–97 (2009)

    Article  MathSciNet  Google Scholar 

  19. Huerta, J.J., Munive, Y., Struth, G.: Verifying hybrid systems with modal kleene algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science, pp. 225–243. Springer, Cham (2018)

    Google Scholar 

  20. Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15

    Chapter  Google Scholar 

  21. Liberzon, D., Morse, A.S.: Basic problems in stability and design of switched systems. IEEE Control Syst. 19(5), 59–70 (1999)

    Article  Google Scholar 

  22. Lüth, C., Ghani, N.: Composing monads using coproducts. In: Wand, M., Jones, S.L.P. (eds.) 7th ACM SIGPLAN International Conference ICFP 2002: Functional Programming, Pittsburgh, USA, October 04–06, 2002, pp. 133–144. ACM (2002)

    Google Scholar 

  23. Manes, E., Mulry, P.: Monad compositions I: general constructions and recursive distributive laws. Theory Appl. Categories 18(7), 172–208 (2007)

    MathSciNet  MATH  Google Scholar 

  24. Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), Pacific Grove, California, USA, June 5–8, 1989, pp. 14–23. IEEE Computer Society (1989)

    Google Scholar 

  25. Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)

    Article  MathSciNet  Google Scholar 

  26. Neves, R.: Hybrid programs. Ph.D. thesis, Minho University (2018)

    Google Scholar 

  27. Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time maude. Higher-order Symbolic Comput. 20(1–2), 161–196 (2007)

    Article  Google Scholar 

  28. Platzer, A.: Differential dynamic logic for hybrid systems. J. Automated Reason. 41(2), 143–189 (2008)

    Article  MathSciNet  Google Scholar 

  29. Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)

    Book  Google Scholar 

  30. Rajkumar, R.R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical systems: the next computing revolution. In: DAC 2010: Design Automation Conference, 47th ACM/IEEE Conference, Anaheim, USA, June 13–18, 2010, pp. 731–736. IEEE (2010)

    Google Scholar 

  31. Stein, W., et al.: Sage Mathematics Software (Version 6.4.1). The Sage Development Team (2015). http://www.sagemath.org

  32. Shorten, R., Wirth, F., Mason, O., Wulff, K., King, C.: Stability criteria for switched and hybrid systems. Soc. Ind. Appl. Math. (review) 49(4), 545–592 (2007)

    MathSciNet  MATH  Google Scholar 

  33. Simpson, A., Plotkin, G.: Complete axioms for categorical fixed-point operators. Logic in Comput. Sci. LICS 2000, 30–41 (2000)

    MathSciNet  Google Scholar 

  34. Suenaga, K., Hasuo, I.: Programming with infinitesimals: a While-language for hybrid system modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 392–403. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22012-8_31

    Chapter  MATH  Google Scholar 

  35. Uustalu, T.: Generalizing substitution. RAIRO-Theor. Inf. Appl. 37(4), 315–336 (2003)

    Article  MathSciNet  Google Scholar 

  36. van Glabbeek, R.: The linear time-branching time spectrum (extended abstract). In: Theories of Concurrency, CONCUR 1990, vol. 458, pp. 278–297 (1990)

    Google Scholar 

  37. Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)

    Book  Google Scholar 

  38. Witsenhausen, H.: A class of hybrid-state continuous-time dynamic systems. IEEE Trans. Automatic Control 11(2), 161–167 (1966)

    Article  Google Scholar 

Download references

Acknowledgements

The first author would like to acknowledge support of German Research Council (DFG) under the project A High Level Language for Monad-based Processes (GO 2161/1–2). The second author was financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation – COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT – Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-030947. The third author was partially supported by National Funds through FCT/MCTES, within the CISTER Research Unit (UIDB/04234/2020); by COMPETE 2020 under the PT2020 Partnership Agreement, through ERDF, and by national funds through the FCT, within project POCI-01-0145-FEDER-029946; by the Norte Portugal Regional Operational Programme (NORTE 2020) under the Portugal 2020 Partnership Agreement, through ERDF and also by national funds through the FCT, within project NORTE-01-0145-FEDER-028550; and by the FCT within project ECSEL/0016/2019 and the ECSEL Joint Undertaking (JU) under grant agreement No 876852. The JU receives support from the European Union’s Horizon 2020 research and innovation programme and Austria, Czech Republic, Germany, Ireland, Italy, Portugal, Spain, Sweden, Turkey.

Author information

Authors and Affiliations

  1. Department of Computer Science, FAU Erlangen-Nürnberg, Erlangen, Germany

    Sergey Goncharov

  2. University of Minho and INESC-TEC, Braga, Portugal

    Renato Neves

  3. CISTER/ISEP, Porto, Portugal

    José Proença

Authors
  1. Sergey Goncharov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Renato Neves
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. José Proença
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Renato Neves .

Editor information

Editors and Affiliations

  1. Western Norway University of Applied Sciences, Bergen, Norway

    Violet Ka I Pun

  2. Western Norway University of Applied Sciences, Bergen, Norway

    Volker Stolz

  3. Federal University of Sao Carlos, Sao Carlos, Brazil

    Adenilso Simao

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Goncharov, S., Neves, R., Proença, J. (2020). Implementing Hybrid Semantics: From Functional to Imperative. In: Pun, V.K.I., Stolz, V., Simao, A. (eds) Theoretical Aspects of Computing – ICTAC 2020. ICTAC 2020. Lecture Notes in Computer Science(), vol 12545. Springer, Cham. https://doi.org/10.1007/978-3-030-64276-1_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-64276-1_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-64275-4

  • Online ISBN: 978-3-030-64276-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation