Abstract
Hybrid systems are dynamical systems that include both continuous and discrete changes. Modeling and simulation of hybrid systems can be challenging due to various kinds of subtleties of their behavior. The declarative modeling language HydLa aims at concise description of hybrid systems by means of constraints and constraint hierarchies. HyLaGI, a publicly available symbolic simulator of HydLa, featured error-free computation with symbolic parameters. Based on symbolic computation, HyLaGI provides various functionalities including nondeterministic execution, handling of infinitesimal quantities, and construction of hybrid automata. Nondeterministic execution in the framework of constraint programming enables us to solve inverse problems by automatic parameter search. This paper introduces these features by means of example programs. This paper also discusses our experiences with HydLa programming, which is unique in that its data and control structures are both based on constraint technologies. We discuss its expressive power and our experiences with modeling using constraint hierarchies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alur, R., et al.: Hierarchical hybrid modeling of embedded systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 14–31. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45449-7_2
Betsuno, K., Matsumoto, S., Ueda, K.: Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection. In: Berger, C., Mousavi, M.R., Wisniewski, R. (eds.) CyPhy 2016. LNCS, vol. 10107, pp. 17–30. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51738-4_2
Borning, A., Freeman-Benson, B., Wilson, M.: Constraint hierarchies. LISP Symb. Comput. 5(3), 233–270 (1992)
Bourke, T., Pouzet, M.: Zélus: a synchronous language with ODEs. In: HSCC 2013, pp. 113–118. ACM (2013)
Carloni, L.P., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1(1/2), 1–193 (2006)
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). https://doi.org/10.1007/978-3-642-39799-8_18
Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_36
Gupta, V., Jagadeesan, R., Saraswat, V., Bobrow, D.G.: Programming in hybrid constraint languages. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 226–251. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60472-3_12
Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE Computer Society (1996)
Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-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
Lee, E.A.: Constructive models of discrete and continuous physical phenomena. IEEE Access 2, 797–821 (2014)
Lunze, J.: Handbook of Hybrid Systems Control: Theory, Tools, Applications. Cambridge University Press, Cambridge (2009)
Matsumoto, S.: Validated simulation of parametric hybrid systems based on constraints. Ph.D. thesis, Waseda University (2017)
Matsumoto, S., Kono, F., Kobayashi, T., Ueda, K.: HyLaGI: symbolic implementation of a hybrid constraint language HydLa. Electron. Notes Theor. Comput. Sci. 317, 109–115 (2015)
Matsumoto, S., Ueda, K.: Symbolic simulation of parametrized hybrid systems with affine arithmetic. In: TIME 2016, pp. 4–11. IEEE Computer Society (2016)
Modelica Association: Modelica - Unified Object-Oriented Language for Systems Modeling: Language Specification (Version 3.4) (2007). https://modelica.org/documents/ModelicaSpec34.pdf
\(\tilde{\text{N}}\)añez, P., Risso, N., Sanfelice, R.G.: A symbolic simulator for hybrid equations. In: Proceedings of SummerSim 2014, pp. 18:1–18:8 (2014)
Taha, W., et al.: Acumen: an open-source testbed for cyber-physical systems research. In: Mandler, B., et al. (eds.) IoT360 2015. LNICST, vol. 169, pp. 118–130. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47063-4_11
Takeguchi, A., Wada, R., Matsumoto, S., Hosobe, H., Ueda, K.: An algorithm for converting hybrid constraint programs to hybrid automata. In: The 29nd JSSST Annual Conference, 2A-3 (2012). https://www.ueda.info.waseda.ac.jp/~ueda/pub/takeguchi_jssst_PPL2012.pdf. (in Japanese)
Ueda, K., Hosobe, H., Ishii, D.: Declarative semantics of the hybrid constraint language HydLa. Comput. Softw. 28(1), 306–311 (2011). English translation: http://arxiv.org/abs/1910.12272
Ueda, K., Matsumoto, S., Takeguchi, A., Hosobe, H., Ishii, D.: HydLa: a high-level language for hybrid systems. In: 2nd Workshop on Logics for System Analysis (LfSA 2012, affiliated with CAV 2012), pp. 3–17 (2012)
Wakatsuki, Y., Matsumoto, S., Ito, T., Wada, T., Ueda, K.: Model analysis by using micro errors in hybrid constraint processing system HyLaGI. In: The 32nd JSSST Annual Conference (2015). http://jssst.or.jp/files/user/taikai/2015/GENERAL/general6-4.pdf. (in Japanese)
Acknowledgments
We would like to thank Shota Matsumoto for leading the development of the core part of HyLaGI. Early versions of HyLaGI are due to previous colleagues including Ken-ichi Hirose. Of the developers of many experimental features, Akira Takeguchi and Yoshiaki Wakatsuki were initial designers and implementors of the features mentioned in this paper. We thank all members of the project, including the above members, for discussions, development, and debugging. Thanks go also to anonymous reviewers for their detailed and constructive comments. The work is partially supported by Grant-in-Aid for Scientific Research (B) JP18H03223, JSPS, Japan.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Appendix
A Appendix
Figure 28 shows the syntax of HydLa with the list notation. As a key extension from Fig. 4, we newly introduce \(\textit{PL}\) (priority list), \(\textit{EL}\) (expression list), \(\textit{LC}\) (list condition) and a list binding notation “:=”. Both \(\textit{PL}\) and \(\textit{EL}\) consist of extensional and list comprehension notations. In the list comprehension notation, one can enumerate elements that satisfy conditions specified by \(\textit{LC}\). We can generate variables with successive serial numbers using range expressions (\(\textit{RE}\) in Fig. 28) and bind them to upper-case variables using “:=”. We can generate a list of module declarations in a similar manner. MPname, ELname, PLname, and Iname stand for names for module priority definitions, expression lists, priority lists, and elements from iterators, respectively.
Syntax of HydLa with list notation.
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Yamada, Y., Sato, M., Ueda, K. (2020). Constraint-Based Modeling and Symbolic Simulation of Hybrid Systems with HydLa and HyLaGI. In: Chamberlain, R., Edin Grimheden, M., Taha, W. (eds) Cyber Physical Systems. Model-Based Design. CyPhy WESE 2019 2019. Lecture Notes in Computer Science(), vol 11971. Springer, Cham. https://doi.org/10.1007/978-3-030-41131-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-41131-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41130-5
Online ISBN: 978-3-030-41131-2
eBook Packages: Computer ScienceComputer Science (R0)