Abstract
In this paper we introduce a novel approach to the specification of real-time behaviour with process algebras. In contrast to the usual pattern, involving a fixed, measurable, and global notion of time, we suggest to represent real-time constraints indirectly through uninterpreted clocks enforcing broadcast synchronization between processes. Our approach advocates the use of asynchronous process algebras, which admit the faithful representation of nondeterministic and distributed computations.
Technically, we present a non-trivial extension of the Calculus of Communicating Systems CCS [Mil89a] by multiple clocks with associated timeout and clock ignore operators. We illustrate the flexibility of the proposed process algebra, called PMC, by presenting examples of rather different nature. The timeout operators generalize the timeout of ATP [NS90] to multiple clocks. The main technical contribution is a complete axiomatization of strong bisimulation equivalence for a class of finite-state processes and a complete axiomatization of observation congruence for finite processes.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. Dill. The theory of timed automata. In de Bakker et al. [dBHdRR91], pages 45–73.
L. Aceto and D. Murphy. On the ill-timed but well-caused. In E. Best, editor, Proc. Concur'93, pages 97–111. Springer LNCS 715, 1993.
H. R. Andersen and M. Mendler. A process algebra with multiple clocks. Technical Report ID-TR:1993-122, Department of Computer Science, Technical University of Denmark, August 1993.
A. Benveniste, M. Le Borgne, and P. Le Guernic. Hybrid systems: The Signal approach. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 230–254. Springer LNCS 736, 1993.
G. Berry and L. Cosserat. The esterel synchronous programming language and its mathematical semantics. In S. D. Brookes, A. W. Roscoe, and G. Winskel, editors, Seminar on Concurrency, pages 389–448. Springer LNCS 197, 1984.
J.C.M. Baeten and J.W. Klop, editors. Proceedings of CONCUR '90, volume 458 of LNCS. Springer-Verlag, 1990.
T. Bolognesi and F. Lucidi. Timed process algebras with urgent interactions and a unique powerful binary operator. In de Bakker et al. [dBHdRR91], pages 124–148.
L. Birkedal, N. Rothwell, M. Tofte, and D. N. Turner. The ML Kit, Version 1. Technical Report, DIKU, March 1993.
Daniel M. Chapiro. Reliable high-speed arbitration and synchronization. IEEE Transaction on Computers, C-36(10):1251–1255, October 1987.
J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors. Real-Time: Theory in Practice, volume 600 of LNCS. Springer-Verlag, 1991.
M. Hennessy. Timed process algebras: A tutorial. Technical Report 93∶02, Department of Computer Science, University of Sussex, January 1993.
N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.-C. Glory. Specifying, programming and verifying real-time systems using a synchronous declarative language. In Workshop on automatic verification methods for finite state systems, Grenoble, France, June 12–14 1989. Springer LNCS 407.
M. Hennessy and T. Regan. A process algebra for timed systems. Computer Science Technical Report 91∶05, Department of Computer Science, University of Sussex, April 1991. To appear in Information and Computation.
A. S. Klusener. Abstraction in real time process algebra. In de Bakker et al. [dBHdRR91], pages 325–352.
Chen Liang. An interleaving model for real-time systems. Technical Report ECS-LFCS-91-184, Laboratory for Foundations of Computer Science, University of Edinburgh, November 1991.
Robin Milner. A complete inference system for a class of regular behaviours. J. of Computer and System Sciences, 28(3):439–466, June 1984.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Robin Milner. A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation, 81:227–247, 1989.
Faron Moller and Chris Tofts. A temporal calculus of communicating systems. In Baeten and Klop [BK90], pages 401–415.
F. Moller and Ch. Tofts. Behavioural abstraction in TCCS. In W. Kuich, editor, Proc. ICALP'92, pages 559–570. Springer LNCS 623, 1992.
X. Nicollin and J. Sifakis. The algebra of timed processes ATP: theory and application. Technical Report RT-C26, LGI-IMAG, Grenoble, France, December 1990.
X. Nicollin and J. Sifakis. From ATP to timed graphs and hybrid systems. In de Bakker et al. [dBHdRR91], pages 549–572.
X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In de Bakker et al. [dBHdRR91], pages 526–548.
S. Schneider, J. Davies, D.M. Jackson, G.M. Reed, J.N. Reed, and A.W. Roscoe. Timed CSP: Theory and practice. In de Bakker et al. [dBHdRR91], pages 526–548.
Yi Wang. Real-time behaviour of asynchronous agents. In Baeten and Klop [BK90].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andersen, H.R., Mendler, M. (1994). An asynchronous process algebra with multiple clocks. In: Sannella, D. (eds) Programming Languages and Systems — ESOP '94. ESOP 1994. Lecture Notes in Computer Science, vol 788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57880-3_4
Download citation
DOI: https://doi.org/10.1007/3-540-57880-3_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57880-2
Online ISBN: 978-3-540-48376-2
eBook Packages: Springer Book Archive