AbstractAction systems have been used successfully to describe discrete systems, i.e., systems with discrete control acting upon a discrete state space. In this paper we define continuous action systems that extend the action system approach to also model hybrid systems, i.e., systems with d iscrete control over a continuously evolving state. The semantics of continuous action systems is defined in terms of traditional action systems and their properties are proved using standard action systems proof techniques. We describe the essential features of continuous action systems, s how that they can be used to describe a diverse range of hybrid systems and illustrate the framework by a collection of examples.
Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic; D.2.4 [Software Engineering]: Program Verification
Additional Key Words and Phrases: refinement calculus, action systems, hybrid systems
Selected references
- R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pages 131-142, Montreal, Quebec, Canada, 17-19 August 1983.