A process calculus with finitary comprehended terms

DOI10.1007/S00224-013-9468-XMaRDI QIDQ385508zbMATH OpenOpenAlexFDO

Authors C. A. Middelburg, J. A. Bergstra

Publication date 2 December 2013

Published in Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0903.2914

ACP process algebra comprehended term meadow enriched ACP process algebra process calculus variable-binding operator

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

Abstract: We introduce the notion of an ACP process algebra and the notion of a meadow enriched ACP process algebra. The former notion originates from the models of the axiom system ACP. The latter notion is a simple generalization of the former notion to processes in which data are involved, the mathematical structure of data being a meadow. Moreover, for all associative operators from the signature of meadow enriched ACP process algebras that are not of an auxiliary nature, we introduce variable-binding operators as generalizations. These variable-binding operators, which give rise to comprehended terms, have the property that they can always be eliminated. Thus, we obtain a process calculus whose terms can be interpreted in all meadow enriched ACP process algebras. Use of the variable-binding operators can have a major impact on the size of terms.

Review text

The notion of an ACP process algebra based on the axiom system ACP is introduced (there is no need of having constants for each atomic action) as well as the ACP process algebra enriched by data, where the mathematical structure of data is a meadow (it is a field with the multiplicative inverse operation made total by imposing that the multiplicative inverse of zero is zero). For all associative operators from the signature of meadow enriched ACP process algebra that are not of an auxiliary nature, variable-binding operators as generalizations are introduced. It is shown that the use of variable-binding operators that bind variables with a two-valued range can already have a major impact on the size of terms, and that impact can be further increased if an identity element for sequential composition is added. Moreover, it is shown that all variable-binding operators of the calculus associated with meadow enriched ASP process algebra can be eliminated from all terms of the calculus by means of its axioms, and all terms of the calculus can be directly interpreted in meadow enriched ACP process algebra.

Recommendations

Cites work

Cited in

(6)

This page was built for publication: A process calculus with finitary comprehended terms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q385508)