×

zbMATH — the first resource for mathematics

Algebra of communicating processes with abstraction. (English) Zbl 0579.68016
This paper presents an equational axiom system \(ACP_{\tau}\), for communicating processes with silent actions (\(\tau\)-steps). The system is an extension of ACP, Algebra of Communicating Processes [see the authors, Inf. Control 60, 109-137 (1984)] with Milner’s \(\tau\)-laws [see R. Milner, A calculus of communicating processes (Berlin 1980; Zbl 0452.68027)] and an explicit abstraction (’hiding’) operator. By means of a model of finite acyclic process graphs syntactic properties such as consistency and conservativity over ACP are proved. Also, the Expansion Theorem (which breaks down a parallel composition of n processes) is proved. By means of a term rewriting analysis using Dershowitz’s recursive path orderings, termination of rewriting terms according to the \(ACP_{\tau}\) axioms is proved.

MSC:
68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68Q65 Abstract data types; algebraic specification
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] De Bakker, J.W.; Zucker, J.I., Processes and the denotational semantics of concurrency, Information and control, 54, 1/2, 70-120, (1982) · Zbl 0508.68011
[2] Bergstra, J.A.; Klop, J.W., Process algebra for synchronous communication, Information and control, 60, 1-3, 109-137, (1984) · Zbl 0597.68027
[3] Bergstra, J.A.; Klop, J.W., An abstraction mechanism for process algebras, () · Zbl 0579.68016
[4] Bergstra, J.A.; Klop, J.W., Algebra of communicating processes, (), to appear · Zbl 0605.68013
[5] Bergstra, J.A.; Tucker, J.V., Top-down design and the algebra of communicating processes, Sci. comput. program., 5, 2, 171-199, (1985) · Zbl 0606.68021
[6] Brookes, S.D.; Rounds, W.C., Behavioural equivalence relations induced by programming logics, (), 97-108 · Zbl 0536.68042
[7] Dershowitz, N., Ordering for term-rewriting systems, Theoret. comput. sci., 17, 279-301, (1982) · Zbl 0525.68054
[8] Dershowitz, N., A note on simplification ordering, Inform. process. lett., 9, 5, 212-215, (1979) · Zbl 0433.68044
[9] Graf, S.; Sifakis, J., A modal characterization of observational congruence on finite terms of CCS, (), 222-234 · Zbl 0551.68034
[10] Hennessy, M., A term model for synchronous processes, Information and control, 51, 1, 58-75, (1981) · Zbl 0503.68022
[11] Hoare, C.A.R., A model for communicating sequential processes, (), 229-243 · Zbl 0841.68042
[12] Milner, R., A calculus for communicating systems, () · Zbl 0609.68021
[13] Winskel, G.; Winskel, G., Synchronisation trees, (), Theoret. comput. sci., 34, 1, 2, 33-82, (1984), see in: · Zbl 0985.68514
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.