×
Rönkkö, Mauno; Ravn, Anders P.; Sere, Kaisa

Hybrid action systems. (English) Zbl 1019.68054

Theor. Comput. Sci. 290, No. 1, 937-973 (2003).
In this paper we investigate the use of action systems with differential actions in the specification of hybrid systems. As the main contribution we generalize the definition of a differential action, allowing the use of arbitrary relations over model variables and their time derivatives in modelling continuous-time dynamics. The generalized differential action has an intuitively appealing predicate transformer semantics, which we show to be both conjunctive and monotonic. In addition, we show that differential actions blend smoothly with conventional actions in action systems even under parallel composition. Moreover, as the strength of the action system formalism is the support for stepwise development by refinement, we investigate refinement involving a differential action. We show that, due to the predicate transformer semantics, standard action refinement techniques apply also to the differential action, thus, allowing stepwise development of hybrid systems.

Cited in 12 Documents

MSC:

68Q45 Formal languages and automata

Keywords:

hybrid systems; predicate transformers; action systems; refinement calculus; concurrency
Cite Review PDF
Full Text: DOI

References:

[1] M. Abadi, L. Lamport, An old-fashioned recipe for real-time, ACM Trans. Programming Languages Systems 16(5) (1994) 1543-1571, also appeared in: J.W. de Bakker, C. Huizing, W.-P. de Roever, G. Rozenberg (Eds.), Lecture Notes in Computer Science, Vol. 600, Springer, Berlin, 1992.; M. Abadi, L. Lamport, An old-fashioned recipe for real-time, ACM Trans. Programming Languages Systems 16(5) (1994) 1543-1571, also appeared in: J.W. de Bakker, C. Huizing, W.-P. de Roever, G. Rozenberg (Eds.), Lecture Notes in Computer Science, Vol. 600, Springer, Berlin, 1992.
[2] Back, R. J.R., Refinement calculus, part IIparallel and reactive programs, (de Bakker, J. W.; de Roever, W. P.; Rozenberg, G., Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings. Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings, Lecture Notes in Computer Science, Vol. 430 (1990), Springer: Springer Berlin), 67-93
[3] R.J.R. Back, Atomicity refinement in a refinement calculus framework, Reports on Computer Science and Mathematics, 141, Åbo Akademi, 1993.; R.J.R. Back, Atomicity refinement in a refinement calculus framework, Reports on Computer Science and Mathematics, 141, Åbo Akademi, 1993.
[4] R.J.R. Back, R. Kurki-Suonio, Decentralization of process nets with centralized control, in: Proc. 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, 1983, pp. 131-142.; R.J.R. Back, R. Kurki-Suonio, Decentralization of process nets with centralized control, in: Proc. 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, 1983, pp. 131-142.
[5] Back, R. J.R.; Sere, K., Stepwise refinement of action systems, Struct. Programming, 12, 17-30 (1991)
[6] Back, R. J.R.; von Wright, J., Trace refinement of action systems, (Parrow, J., CONCUR94. CONCUR94, Lecture Notes in Computer Science, Vol. 666 (1994), Springer: Springer Berlin) · Zbl 1093.68007
[7] Back, R. J.R.; von Wright, J., Refinement calculusa systematic introduction, Graduate Texts in Computer Science (1998), Springer: Springer Berlin · Zbl 0949.68094
[8] Bonsangue, M.; Kok, J. N., Semantics, orderings and recursion in the weakest precondition calculus, (de Bakker, J. W.; Rozenberg, G.; de Roever, W. P., Proceedings Rex Workshop on Semantics: Foundations and Applications. Proceedings Rex Workshop on Semantics: Foundations and Applications, Lecture Notes in Computer Science, Vol. 666 (1993), Springer: Springer Berlin), 91-110
[9] Bowman, H., Modelling timeout without timelocks, (Katoen, J.-P., Formal Methods for Real-Time and Probabilistic Systems. Formal Methods for Real-Time and Probabilistic Systems, Lecture Notes in Computer Science, Vol. 1601 (1999), Springer: Springer Berlin)
[10] M.S. Branicky, Studies in hybrid systems: modeling, analysis, and control, Ph.D. Thesis, EECS Department, Massachusetts Institute of Technology, 1995.; M.S. Branicky, Studies in hybrid systems: modeling, analysis, and control, Ph.D. Thesis, EECS Department, Massachusetts Institute of Technology, 1995.
[11] Branicky, M. S., Analyzing and synthesizing hybrid control systems, (Rozenberg, G.; Vaandrager, F., Lectures on Embedded Systems. Lectures on Embedded Systems, Lecture Notes in Computer Science, Vol. 1494 (1998), Springer: Springer Berlin), 74-113
[12] Broy, M.; Nelson, G., Adding fair choice to Dijkstra’s calculus, CM Transactions on Programming Languages Systems, 16, 3, 924-938 (1994)
[13] Butler, M.; Sekerinski, E.; Sere, K., An action system approach to the steam boiler problem, (Abrial, J.-R.; Borger, E.; Langmaack, H., Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science, Vol. 1165 (1996), Springer: Springer Berlin) · Zbl 1060.68501
[14] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall International: Prentice-Hall International Englewood Cliffs, NJ · Zbl 0286.00013
[15] He, J., From CSP to hybrid systems, (Roscoe, A. W., A Classical Mind, Essays in Honour of C.A.R. Hoare (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 171-189
[16] T.A. Henzinger, Hybrid automata with finite bisumaltions, in: Proc. 22nd Internat. Colloq. on Automata, Languages, and Programming (ICALP 1995), Lecture Notes in Computer Science, Vol. 994, Springer-Verlag, 1995, pp. 324-335.; T.A. Henzinger, Hybrid automata with finite bisumaltions, in: Proc. 22nd Internat. Colloq. on Automata, Languages, and Programming (ICALP 1995), Lecture Notes in Computer Science, Vol. 994, Springer-Verlag, 1995, pp. 324-335. · Zbl 1412.68130
[17] T.A. Henzinger, The theory of hybrid automata, in: Proc. 11th Ann. IEEE Symp. on Logic in Computer Science (LICS 1996), 1996, pp. 278-292.; T.A. Henzinger, The theory of hybrid automata, in: Proc. 11th Ann. IEEE Symp. on Logic in Computer Science (LICS 1996), 1996, pp. 278-292. · Zbl 0959.68073
[18] Hoare, C. A.R., Communicating Sequential Processes (1984), Prentice-Hall International: Prentice-Hall International London · Zbl 0841.68042
[19] Jaffe, M.; Leveson, N.; Heimdahl, M.; Melhart, B., Software requirements analysis for real-time process-control systems, IEEE Trans. Software Eng., 17, 3, 241-258 (1991)
[20] Kesten, Y.; Manna, Z.; Pnueli, A., Verification of clocked and hybrid systems, (Rozenberg, G.; Vaandrager, F., Lectures on Embedded Systems. Lectures on Embedded Systems, Lecture Notes in Computer Science, Vol. 1494 (1998), Springer: Springer Berlin), 4-73
[21] La Salle, J.; Lefschetz, S., Stability by Liapunov’s Direct Method with Applications (1961), Academic Press: Academic Press New York · Zbl 0098.06102
[22] Lamport, L., Hybrid systems in \(TLA^+\), (Grossman, R.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 149-178 · Zbl 0825.00044
[23] Lynch, N. A.; Segala, R.; Vaandrager, F. W.; Weinberg, H. B., Hybrid I/O automata, (Alur, R.; Henzinger, T. A.; Sontag, E. D., Hybrid Systems III. Hybrid Systems III, Lecture Notes in Computer Science, Vol. 1066 (1996), Springer: Springer Berlin), 496-510
[24] M.H.A. Newman, Elements of the Topology of Plane Sets of Points,1st Edition, 1939, Cambridge University Press, Cambridge, 1961.; M.H.A. Newman, Elements of the Topology of Plane Sets of Points,1st Edition, 1939, Cambridge University Press, Cambridge, 1961. · Zbl 0021.06704
[25] Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., An approach to the description and analysis of hybrid systems, (Grossman, R.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 149-178
[26] Rönkkö, M.; Li, X., Linear hybrid action systems, Nordic J. Comput., 8, 1, 159-177 (2001) · Zbl 0978.68106
[27] Rönkkö, M.; Ravn, A. P., Switches and jumps in hybrid action systems, Proc. Estonian Acad. Sci. Eng., 4, 2, 106-118 (1998)
[28] Rönkkö, M.; Ravn, A. P., Action systems with continuous behavior, (Antsaklis, P. J.; Kohn, W.; Lemmon, M.; Nerode, A.; Sastry, S., Proceedings of Hybrid Systems V. Proceedings of Hybrid Systems V, Lecture Notes in Computer Science, Vol. 1567 (1999), Springer: Springer Berlin), 304-323 · Zbl 0986.93006
[29] Rönkkö, M.; Sere, K., Refinement and continuous behavior, (Vaandrager, F. W.; van Schuppen, J. H., Proceedings of Hybrid Systems: Computation and Control. Proceedings of Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 1569 (1999), Springer: Springer Berlin), 223-237 · Zbl 0930.68030
[30] Yovine, S., Model-checking timed automata, (Rozenberg, G.; Vaandrager, F., Embedded Systems. Embedded Systems, Lecture Notes in Computer Science, Vol. 1494 (1998), Springer: Springer Berlin)
[31] Zhou, C.; Ji, Wang; Ravn, A. P., A formal description of hybrid systems, (Alur, R.; Henzinger, T.; Sontag, E., Hybrid Systems III. Hybrid Systems III, Lecture Notes in Computer Science, Vol. 1066 (1996), Springer: Springer Berlin), 511-530
[32] Zhou, C.; Ravn, A. P.; Hansen, M. R., An extended duration calculus for hybrid systems, (Grossman, R.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin) · Zbl 0825.00044
[33] Zill, D. G.; Cullen, M. R., Differential Equations with Boundary-value problems (1997), Brooks/Cole Publishing Company: Brooks/Cole Publishing Company Pacific Grove
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.