Abstract
We add, to the common combination of a \(\textsc{While}\)-language and a Hoare-style program logic, a constant \(\mathtt{dt}\) that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete.
We are greteful to Naoki Kobayashi and Toshimitsu Ushio for helpful discussions.
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
Preview
Unable to display preview. Download preview PDF.
References
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. Theor. Comp. Sci. 138(1), 3–34 (1995)
Bliudze, S., Krob, D.: Modelling of complex systems: Systems as dataflow machines. Fundam. Inform. 91(2), 251–274 (2009)
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journ. Comput. 7(1), 70–90 (1978)
Hurd, A.E., Loeb, P.A.: An Introduction to Nonstandard Real Analysis. Academic Press, London (1985)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)
Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008)
Rust, H.: Operational Semantics for Timed Systems: A Non-standard Approach to Uniform Modeling of Timed and Hybrid Systems. LNCS, vol. 3456. Springer, Heidelberg (2005)
Suenaga, K., Hasuo, I.: Programming with infinitesimals: A While-language for hybrid system modeling. Extended version with proofs (April 2011)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Suenaga, K., Hasuo, I. (2011). Programming with Infinitesimals: A While-Language for Hybrid System Modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds) Automata, Languages and Programming. ICALP 2011. Lecture Notes in Computer Science, vol 6756. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22012-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-22012-8_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22011-1
Online ISBN: 978-3-642-22012-8
eBook Packages: Computer ScienceComputer Science (R0)