Abstract
Recently, J.C.M. Baeten and J.A. Bergstra extended ACP with real time, resulting in a Real Time Process Algebra, called ACPρ [BB91]. They introduced an equational theory and an operational semantics. However, their work does not contain a completeness result nor does it contain the definitions to give proofs in detail. In this paper we introduce some machinery and a completeness result.
The operational semantics of [BB91] contains the notion of an idle step reflecting that a process can do nothing more then passing the time before performing a concrete action at a certain point in time. This idle step corresponds nicely to our intuition but it results in infinitary transition systems. In this paper we give a more abstract operational semantics, by abstracting from the idle step. Due to this simplification we can prove soundness and completeness easily. These results hold for the semantics of [BB91] as well, since both operational semantics induce the same equivalence relation between processes.
(Extended Abstract)
Note: This work is in part sponsored by ESPRIT Basic Research Action 3006, CONCUR.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J.C.M. Baeten and J.A. Bergstra. Process algebra with signals and conditions. Report P9008, University of Amsterdam, Amsterdam, 1990.
J.C.M. Baeten and J.A. Bergstra. Real time process algebra. Journal of Formal Aspects of Computing Science, 3(2):142–188, 1991.
J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Computation, 60(1/3):109–137, 1984.
J.C.M. Baeten and W.P. Weijland. Process algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
R.J. van Glabbeek. Bounded nondeterminism and the approximation induction principle in process algebra. In F.J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors, Proceedings STACS 87, volume 247 of Lecture Notes in Computer Science, pages 336–347. Springer-Verlag, 1987.
J.F. Groote. Transition system specifications with negative premises. Report CS-R8950, CWI, Amsterdam, 1989. An extended abstract appeared in J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, LNCS 458, pages 332–341. Springer-Verlag, 1990.
J.F. Groote. Specification and verification of real time systems in ACP. Report CS-R9015, CWI, Amsterdam, 1990. An extended abstract appeared in L. Logrippo, R.L. Probert and H. Ural, editors, Proceedings 10 th International Symposium on Protocol Specification, Testing and Verification, Ottawa, pages 261–274, 1990.
A. Jeffrey. Discrete timed CSP. Technical Report Memo 78, Chalmers University, Goteborg, 1991. This document also appeared in this volume.
A.S. Klusener. Completeness in realtime process algebra. Report CS-R9106, CWI, Amsterdam, 1991.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
F. Moller and C. Tofts. A temporal calculus of communicating systems. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science, pages 401–415. Springer-Verlag, 1990.
X. Nicollin and J. Sifakis. ATP: An algebra for timed processes. Technical Report RT-C26, IMAG, Laboratoire de Génie informatique, Grenoble, 1990. An earlier version (RT-C16) appeared in M. Broy and C.B. Jones, editors, Proceedings IFIP Working Conference on Programming Concepts and Methods, Sea of Gallilea, Israel. North-Holland, 1990.
D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5th GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, 1981.
G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
M. Reed and A.W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 58:249–261, 1988.
Y. Wang. Real time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science, pages 502–520. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klusener, A.S. (1991). Completeness in real time process algebra. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_101
Download citation
DOI: https://doi.org/10.1007/3-540-54430-5_101
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54430-2
Online ISBN: 978-3-540-38357-4
eBook Packages: Springer Book Archive