×

zbMATH — the first resource for mathematics

An efficiency preorder for processes. (English) Zbl 0790.68039
A simple efficiency preorder for CCS processes is introduced in which \(p\preceq q\) means that \(q\) is at least as fast as \(p\), or more generally, \(p\) uses at least as much resources as \(q\). It is shown to be preserved by all CCS contexts except summation and it is used to analyse a non-trivial example: two different implementations of a bounded buffer. Finally, we give a sound and complete proof system for finite processes.

MSC:
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Proc. International Conference on Theoretical Aspects of Computer Software. (Lect. Notes Comput. Sci., vol. 526, pp. 152-175. Berlin Heidelberg New York: Springer 1991 · Zbl 0790.68039
[2] Beaton, J., Bergstra, J.: Real time process algebra, Technical Report CWI Amsterdam, 1989
[3] Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: A semantics-based verification tool for finite-state systems, Technical Report ECS-LFCS-89-83, University of Edinburgh, 1989
[4] Davies, J., Schneider, S.: An introduction to timed CSP, Technical Report, PRG, Oxford, 1989
[5] Gerth, R., Boucher, A.: A timed failures model for extended communicating sequential processes (Lect. Notes Comput. Sci., vol. 267, pp. 95-114. Berlin Heidelberg New York: Springer 1986
[6] Hennessy, M.: Algebraic theory of processes. Cambridge, MA: MIT Press 1988 · Zbl 0744.68047
[7] Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM32(1), 137-161 (1985) · Zbl 0629.68021 · doi:10.1145/2455.2460
[8] Hennessy, M., Regan, T.: A temporal process algebra. Technical Report 2/90, University of Sussex, 1990 · Zbl 0826.68068
[9] C.A.R. Hoare: Communicating sequential processes. Englewood Cliffs, NJ: Prentice Hall 1985 · Zbl 0637.68007
[10] Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci.25, 267-310 (1983) · Zbl 0512.68026 · doi:10.1016/0304-3975(83)90114-7
[11] Milner, R.: Communicationa and concurrency. Englewood Cliffs, NJ: Prentice Hall 1989 · Zbl 0683.68008
[12] Nicollin, X., Richier, J.L., Sifakis, J., Voiron, J.: ATP: An algebra for timed processes. Technical Report, Grenoble, 1989
[13] Park, D.: Concurrency and automata on infinite sequences. (Lect. Notes Comput. Sci., vol. 104, pp. 167-183) Berlin Heidelberg New York: Springer 1980
[14] Reed, G.M., Roscoe, A.: A timed model for communicating sequential processes (Lect. Notes Comput. Sci., vol. 226, pp. 314-323) Berlin Heidelberg New York: Springer 1986 · Zbl 0594.68025
[15] Rudkin, S., Smith, C.R.: A temporal enhancement for LOTOS. British Telecom, 1988
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.