×

Process algebra for hybrid systems. (English) Zbl 1080.68073

Summary: We propose a process algebra obtained by extending a combination of the process algebra with continuous relative timing from J. C. M. Baeten and C. A. Middelburg [Process algebra with timing (2002; Zbl 1021.68063), Chapter 4] and the process algebra with propositional signals from J. C. M. Baeten and J. A. Bergstra [Theor. Comput. Sci. 177, 381–405 (1977; Zbl 0901.68117)]. The proposed process algebra makes it possible to deal with the behaviour of hybrid systems, i.e. systems in which the instantaneous state transitions caused by performing actions are alternated with continuous state evolutions. This process algebra has, in addition to equational axioms, rules to derive equations with the help of real analysis.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

HyTech
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Aceto, L.; Fokkink, W. J.; Verhoef, C., Structural operational semantics, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier: Elsevier Amsterdam), 197-292 · Zbl 1062.68074
[2] 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, Theoret. Comput. Sci., 138, 3-34 (1995) · Zbl 0874.68206
[3] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P.-H., Hybrid automataan algorithmic approach to the specification and verification of hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 209-229
[4] Alur, R.; Dill, D. L., Automata for modeling real-time systems, (Paterson, M. S., Proc. 17th ICALP, Lecture Notes in Computer Science, Vol. 443 (1990), Springer: Springer Berlin), 322-335 · Zbl 0765.68150
[5] Alur, R.; Dill, D. L., A theory of timed automata, Theoret. Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071
[6] Alur, R.; Grosu, R.; Lee, I.; Sokolsky, O., Compositional refinement for hierarchical hybrid systems, (Di Benedetto, M. D.; Sangiovanni-Vincentelli, A., HSCC 2001, Lecture Notes in Computer Science, Vol. 2034 (2001), Springer: Springer Berlin), 33-48 · Zbl 0991.93057
[7] Alur, R.; Henzinger, T. A.; Ho, P.-H., Automatic symbolic verification of embedded systems, IEEE Trans. Software Eng., 22, 3, 181-201 (1996)
[8] Baeten, J. C.M.; Bergstra, J. A., Real time process algebra, Formal Aspects Comput., 3, 2, 142-188 (1991) · Zbl 0719.68020
[9] Baeten, J. C.M.; Bergstra, J. A., Real space process algebra, Formal Aspects Comput., 5, 6, 481-529 (1993) · Zbl 0942.68607
[10] Baeten, J. C.M.; Bergstra, J. A., Real time process algebra with infinitesimals, (Ponse, A.; Verhoef, C.; van Vlijmen, S. F.M., Algebra of Communicating Processes 1994, Workshops in Computing Series (1995), Springer: Springer Berlin), 148-187 · Zbl 0719.68020
[11] Baeten, J. C.M.; Bergstra, J. A., Process algebra with propositional signals, Theoret. Comput. Sci., 177, 381-405 (1997) · Zbl 0901.68117
[12] Baeten, J. C.M.; Bergstra, J. A.; Reniers, M. A., Discrete time process algebra with silent step, (Plotkin, G. D.; Stirling, C.; Tofte, M., Proof, Language and InteractionEssays in Honour of Robin Milner (2000), MIT Press: MIT Press Cambridge, MA), 535-569
[13] Baeten, J. C.M.; Middelburg, C. A., Process algebra with timingreal time and discrete time, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier: Elsevier Amsterdam), 627-684 · Zbl 1006.68100
[14] J.C.M. Baeten, C.A. Middelburg, Process Algebra with Timing, Monographs in Theoretical Computer Science, An EATCS Series, Springer, Berlin, 2002.; J.C.M. Baeten, C.A. Middelburg, Process Algebra with Timing, Monographs in Theoretical Computer Science, An EATCS Series, Springer, Berlin, 2002. · Zbl 1021.68063
[15] J.C.M. Baeten, C.A. Middelburg, M.A. Reniers, A new equivalence for processes with timing—with an application to protocol verification, Computer Science Report 02-10, Department of Mathematics and Computer Science, Eindhoven University of Technology, October 2002.; J.C.M. Baeten, C.A. Middelburg, M.A. Reniers, A new equivalence for processes with timing—with an application to protocol verification, Computer Science Report 02-10, Department of Mathematics and Computer Science, Eindhoven University of Technology, October 2002.
[16] Baeten, J. C.M.; Weijland, W. P., Process algebra, (Cambridge Tracts in Theoretical Computer Science, Vol. 18 (1990), Cambridge University Press: Cambridge University Press Cambridge) · Zbl 0716.68002
[17] Bergstra, J. A.; Fokkink, W. J.; Middelburg, C. A., Algebra of timed frames, Internat. J. Comput. Math., 61, 227-255 (1996) · Zbl 1001.68518
[18] Bergstra, J. A.; Klop, J. W., The algebra of recursively defined processes and the algebra of regular processes, (Paredaens, J., Proc. 11th ICALP, Lecture Notes in Computer Science, Vol. 172 (1984), Springer: Springer Berlin), 82-95 · Zbl 0561.68019
[19] Bergstra, J. A.; Klop, J. W., Verification of an alternating bit protocol by means of process algebra, (Bibel, W.; Jantke, K. P., Mathematical Methods of Specification and Synthesis of Software Systems, Lecture Notes in Computer Science, Vol. 215 (1986), Springer: Springer Berlin), 9-23 · Zbl 0595.68024
[20] J.A. Bergstra, C.A. Middelburg, Process algebra for hybrid systems, Computer Science Report 03-06, Department of Mathematics and Computer Science, Eindhoven University of Technology, June 2003.; J.A. Bergstra, C.A. Middelburg, Process algebra for hybrid systems, Computer Science Report 03-06, Department of Mathematics and Computer Science, Eindhoven University of Technology, June 2003.
[21] J.A. Bergstra, C.A. Middelburg, Continuity controlled hybrid automata, Computer Science Report 04-11, Department of Mathematics and Computer Science, Eindhoven University of Technology, April 2004.; J.A. Bergstra, C.A. Middelburg, Continuity controlled hybrid automata, Computer Science Report 04-11, Department of Mathematics and Computer Science, Eindhoven University of Technology, April 2004. · Zbl 1088.68085
[22] J.A. Bergstra, C.A. Middelburg, Located actions in process algebra with timing, Fund. Inform. 61 (3-4) (2004) 183-211.; J.A. Bergstra, C.A. Middelburg, Located actions in process algebra with timing, Fund. Inform. 61 (3-4) (2004) 183-211. · Zbl 1098.68085
[23] Bergstra, J. A.; Middelburg, C. A.; Usenko, Y. S., Discrete time process algebra and the semantics of SDL, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier: Elsevier Amsterdam), 1209-1268 · Zbl 1020.68063
[24] Browder, A., Mathematical AnalysisAn Introduction (1996), Springer: Springer Berlin
[25] Chaochen, Z.; Hoare, C. A.R.; Ravn, A. P., A calculus of durations, Inform. Process. Lett., 40, 269-276 (1991) · Zbl 0743.68097
[26] Chaochen, Z.; Ravn, A. P.; Hansen, M. R., An extended duration calculus for hybrid real-time systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 36-59
[27] Chen, L., An interleaving model for real-time systems, (Nerode, A.; Taitslin, M., Symp. on Logical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 620 (1992), Springer: Springer Berlin), 81-92 · Zbl 0977.68553
[28] P.J.L. Cuijpers, M.A. Reniers, Topological (bi-)simulation, Computer Science Report 02-04, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, April 2001.; P.J.L. Cuijpers, M.A. Reniers, Topological (bi-)simulation, Computer Science Report 02-04, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, April 2001. · Zbl 1271.68177
[29] P.J.L. Cuijpers, M.A. Reniers, Hybrid process algebra, Computer Science Report 03-07, Department of Mathematics and Computer Science, Eindhoven University of Technology, July 2003.; P.J.L. Cuijpers, M.A. Reniers, Hybrid process algebra, Computer Science Report 03-07, Department of Mathematics and Computer Science, Eindhoven University of Technology, July 2003. · Zbl 1090.68071
[30] Davies, J., Timed CSPtheory and practice, (de Bakker, J. W.; Huizing, C.; de Roever, W. P.; Rozenberg, G., Real TimeTheory and Practice, Lecture Notes in Computer Science, Vol. 600 (1992), Springer: Springer Berlin), 640-675
[31] van Glabbeek, R. J., The linear time—branching time spectrum I, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier: Elsevier Amsterdam), 3-99 · Zbl 1035.68073
[32] Groote, J. F.; Ponse, A., Process algebra with guardscombining Hoare logic with process algebra, Formal Aspects Comput., 6, 2, 115-164 (1994) · Zbl 0806.68078
[33] Groote, J. F.; van Wamel, J. J., Analysis of three hybrid systems in timed \(\mu\) CRL, Sci. Comput. Programming, 39, 2/3, 215-247 (2001) · Zbl 0971.68113
[34] Hennessy, M.; Regan, T., A process algebra for timed systems, Inform. Comput., 117, 221-239 (1995) · Zbl 0826.68068
[35] T.A. Henzinger, The theory of hybrid automata, in: LICS’96, IEEE Computer Society Press, Los Altos, CA, 1996, pp. 278-292.; T.A. Henzinger, The theory of hybrid automata, in: LICS’96, IEEE Computer Society Press, Los Altos, CA, 1996, pp. 278-292. · Zbl 0959.68073
[36] Henzinger, T. A., Assume-guarantee reasoning for hierarchical hybrid systems, (Di Benedetto, M. D.; Sangiovanni-Vincentelli, A., HSCC 2001, Lecture Notes in Computer Science, Vol. 2034 (2001), Springer: Springer Berlin), 275-290 · Zbl 0991.93002
[37] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., HyTecha model checker for hybrid systems, Internat. J. Tools Technol. Transfer, 1, 1/2, 110-122 (1997) · Zbl 1060.68603
[38] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., Algorithmic analysis of nonlinear hybrid systems, IEEE Trans. Automat. Control, 43, 278-292 (1998)
[39] Henzinger, T. A.; Horowitz, B.; Majumdar, R.; Wong-Toi, H., Beyond HyTechhybrid systems analysis using interval numerical methods, (Lynch, N.; Krogh, B. H., HSCC 2000, Lecture Notes in Computer Science, Vol. 1790 (2000), Springer: Springer Berlin), 130-144 · Zbl 0938.93552
[40] Henzinger, T. A.; Manna, Z.; Pnueli, A., Towards refining temporal specifications into hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 60-76
[41] Jifeng, H., From CSP to hybrid systems, (Roscoe, A. W., A Classical MindEssays in Honour of C.A.R. Hoare (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 171-189
[42] Lynch, N.; Segala, R.; Vaandrager, F. W., Hybrid I/O automata, Inform. Comput., 185, 1, 105-157 (2003) · Zbl 1069.68067
[43] Middelburg, C. A., Truth of duration calculus formulae in timed frames, Fund. Inform., 36, 2/3, 235-263 (1998) · Zbl 0930.68089
[44] Middelburg, C. A., Variable binding operators in transition system specifications, J. Logic Algebraic Programming, 47, 1, 15-45 (2001) · Zbl 0970.68117
[45] Middelburg, C. A., Process algebra with nonstandard timing, Fund. Inform., 53, 1, 55-77 (2002) · Zbl 1050.68106
[46] Middelburg, C. A., Revisiting timing in process algebra, J. Logic Algebraic Programming, 54, 1/2, 109-127 (2003) · Zbl 1051.68110
[47] Middelburg, C. A., An alternative formulation of operational conservativity with binding terms, J. Logic Algebraic Programming, 55, 1/2, 1-19 (2003) · Zbl 1048.68056
[48] Milner, R., Communicating and Mobile SystemsThe \(\pi \)-Calculus (1999), Cambridge University Press: Cambridge University Press Cambridge
[49] Moller, F.; Tofts, C., A temporal calculus of communicating systems, (Baeten, J. C.M.; Klop, J. W., CONCUR’90, Lecture Notes in Computer Science, Vol. 458 (1990), Springer: Springer Berlin), 401-415
[50] Nicollin, X.; Sifakis, J., The algebra of timed processes ATPtheory and application, Inform. Comput., 114, 1, 131-178 (1994) · Zbl 0811.68093
[51] Quemada, J.; de Frutos, D.; Azcorra, A., TICa timed calculus, Formal Aspects Comput., 5, 3, 224-252 (1993) · Zbl 0797.68059
[52] Rounds, W. C.; Song, Hosung, (Maler, O.; Pnueli, A., The \(\phi \)-calculusa language for distributed control of reconfigurable embedded systems. The \(\phi \)-calculusa language for distributed control of reconfigurable embedded systems, HSCC 2003, Lecture Notes in Computer Science, Vol. 2623 (2003), Springer: Springer Berlin), 435-449 · Zbl 1032.93036
[53] J.J. Vereijken, A process algebra for hybrid systems, extended abstract of talk presented at Second European Workshop on Real-Time and Hybrid Systems, Grenoble, France, 1995.; J.J. Vereijken, A process algebra for hybrid systems, extended abstract of talk presented at Second European Workshop on Real-Time and Hybrid Systems, Grenoble, France, 1995.
[54] J.J. Vereijken, Discrete time process algebra, Ph.D. Thesis, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, 1997.; J.J. Vereijken, Discrete time process algebra, Ph.D. Thesis, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, 1997. · Zbl 0948.68518
[55] Yi, W., Real-time behaviour of asynchronous agents, (Baeten, J. C.M.; Klop, J. W., CONCUR’90, Lecture Notes in Computer Science, Vol. 458 (1990), Springer: Springer Berlin), 502-520
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.