A Process Calculus with Finitary Comprehended Terms
- PDF / 797,263 Bytes
- 24 Pages / 439.37 x 666.142 pts Page_size
- 29 Downloads / 171 Views
A Process Calculus with Finitary Comprehended Terms J.A. Bergstra · C.A. Middelburg
Published online: 21 April 2013 © Springer Science+Business Media New York 2013
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. Keywords ACP process algebra · Meadow enriched ACP process algebra · Variable-binding operator · Comprehended term · Process calculus
1 Introduction In many formalisms proposed for the description and analysis of processes in which data are involved, algebraic specifications of the data types concerned have to be given over and over again. This is also the case with the principal ACP-based formalisms proposed for the description and analysis of processes in which data are involved, to wit μCRL [16, 17] and PSF [23]. There is a mismatch between the process J.A. Bergstra · C.A. Middelburg () Informatics Institute, Faculty of Science, University of Amsterdam, Science Park 904, 1098 XH Amsterdam, The Netherlands e-mail: [email protected] J.A. Bergstra e-mail: [email protected]
646
Theory Comput Syst (2013) 53:645–668
specification part and the data specification part of these formalisms. Firstly, there is a choice of one built-in type of processes, whereas there is a choice of all types of data that can be specified algebraically. Secondly, the semantics of the data specification part is its initial algebra in the case of PSF and its class of minimal Boolean preserving algebras in the case of μCRL, whereas the semantics of the process specification part is a model based on transition systems and bisimulation equivalence. Sticking to this mismatch, no lasting axiomatizations in the style of ACP has emerged for process algebras that have to do with processes in which data are involved. Our first main objective is to obtain a lasting axiomatization in the style of ACP for process algebras that have to do with processes in which data are involved. To achieve this objective, we first introduce the notion of an ACP process algebra and then the notion of a meadow enriched ACP process algebra. ACP process algebras are essentially models of the axiom system ACP. Meadow enriched ACP process algebras are data enriched ACP process algebras in which the mathematical structure for data is a meadow. Meadows were def
Data Loading...
