zbMATH — the first resource for mathematics

Modular specification of process algebras. (English) Zbl 0770.68092
Summary: This paper proposes a modular approach to the algebraic specification of process algebras. This is done by means of the notion of a module. The simplest modules are building blocks of operators and axioms, each block describing a feature of concurrency in a certain semantical setting. These modules can then be combined by means of a union operator +, an export operator \(\square\), allowing to forget some operators in a module, an operator \(H\), changing semantics by taking homomorphic images, and an operator \(S\) which takes subalgebras. These operators enable us to combine modules in a subtle way, when the direct combination would be inconsistent.
We give a presentation of equational logic, infinitary conditional equational logic – of which we also prove the completeness – and first- order logic and show how the notion of a formal proof of a formula from a theory can be generalized to that of a proof of a formula from a module. This module logic is then applied in process algebra. We show how auxiliary process algebra operators can be hidden when this is needed. Moreover, we demonstrate how new process combinators can be defined in terms of more elementary ones in a clean way. As an illustration of our approach, we specify some FIFO-queues and verify several of their properties.

68Q65 Abstract data types; algebraic specification
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI
[1] Aceto, L., A theory of testing for ACP, Computer science report 3/90, (1990), University of Sussex Brighton
[2] America, P., Definition of the programming language POOL-T, ESPRIT project 415, document no. 91, (1985), Philips Research Laboratories Eindhoven
[3] Austry, D.; Boudol, G., Algèbre de processus et synchronisations, Theoret. comput. sci., 30, 91-131, (1984) · Zbl 0533.68026
[4] Baeten, J.C.M.; Bergstra, J.A., Global renaming operators in concrete process algebra, Inform. and comput., 78, 205-245, (1988) · Zbl 0651.68031
[5] Baeten, J.C.M.; Bergstra, J.A., Recursive process definitions with the state operator, report CS-R8920, (), 285-302 · Zbl 0724.68035
[6] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Conditional axions and α/β calculus in process algebra, (), 53-75, Proc. 3rd IFIP WG 2.2 Working Conf., Ebberup , 1986 · Zbl 0617.68027
[7] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., On the consistency of Koomen’s fair abstraction rule, Theoret. comput. sci., 51, 129-176, (1987) · Zbl 0621.68010
[8] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Ready-trace semantics for concrete process algebra with the priority operator, Comput. J., 30, 498-506, (1987) · Zbl 0627.68016
[9] Baeten, J.C.M.; van Glabbeek, R.J., Merge and termination in process algebra, (), 153-172, Pune, India, Lecture Notes in Computer Science · Zbl 0636.68024
[10] Baeten, J.C.M.; Weijland, W.P., Cambridge tracts in theoret. comput. sci., Process algebra, 18, (1990), Cambridge Univ. Press Cambridge
[11] Bergstra, J.A.; Heering, J.; Klint, P., Module algebra, J. ACM, 37, 335-372, (1990) · Zbl 0696.68040
[12] Bergstra, J.A.; Klop, J.W., Algebra of communicating processes with abstraction, Theoret. comput. sci., 37, 77-121, (1985) · Zbl 0579.68016
[13] Bergstra, J.A.; Klop, J.W., Process algebra: specification and verification in bisimulation semantics, (), 61-94, CWI Monograph 4 · Zbl 0625.68023
[14] Bergstra, J.A.; Klop, J.W.; Olderog, E.-R., Failures without chaos: a new process semantics for fair abstraction, (), 77-103
[15] Bergstra, J.A.; Tiuryn, J., Process algebra semantics for queues, Fund. inform., 10, 213-224, (1987), also appeared as MC Report IW 241, Amsterdam, 1983 · Zbl 0636.68025
[16] Birkhoff, G., On the structure of abstract algebras, Proc. Cambridge philos. soc., 31, 433-454, (1935) · Zbl 0013.00105
[17] Brookes, S.D.; Roscoe, A.W., An improved failures model for communicating processes, (), 281-305, Lecture Notes in Computer Science · Zbl 0565.68023
[18] Broy, M., Views on queues, Sci. comput programming, 11, 65-86, (1988) · Zbl 0665.68014
[19] Recommendation Z.200 (CHILL language definition), CCITT study group XI, (1980)
[20] Denvir, T.; Harwood, W.; Jackson, M.; Ray, M., The analysis on concurrent systems, Lecture notes in computer science, 207, (1985), Springer Berlin, Proc. of a Tutorial and Workshop, Cambridge Univ., 1983 · Zbl 0581.68002
[21] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. comput. sci., 34, 83-133, (1984) · Zbl 0985.68518
[22] van Glabbeeck, R.J., Bounded nondeterminism and the approximation induction principle in process algebra, (), 336-347, Lecture Notes in Computer Science
[23] van Glabbeek, R.J., The linear time – branching time spectrum, (), 278-297
[24] van Glabbeek, R.J., Comparative concurrency semantics and refinement of actions, Ph.D. thesis, (1990), Free Univ., Amsterdam
[25] van Glabbeek, R.J.; Vaandrager, F.W., Modular specifications in process algebra – with curious queues (extended abstract), (), 465-506, Lecture Notes in Computer Science
[26] van Glabbeek, R.J.; Weijland, W.P., Branching time and abstraction in bisimulation semantics, Report TUM-I9052, (1990), Technical Univ. of Munich, [24, Chapter 3] · Zbl 0882.68085
[27] Hennessy, M., Algebraic theory of processes, (1988), MIT Press Cambridge, MA · Zbl 0744.68047
[28] Hoare, C.A.R., Communicating sequential processes, (), 229-254 · Zbl 0841.68042
[29] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[30] Jifeng, He; Hoare, C.A.R., Algebraic specification and proof of a distributed recovery algorithm, Distributed computing, 2, 1-12, (1987) · Zbl 0621.68008
[31] Larsen, K.G.; Milner, R., A complete protocol verification using relativized bisimulation, (), 126-135
[32] Mauw, S., An algebraic specification of process algebra, including two examples, (), 507-554
[33] Mauw, S.; Veltink, G.J., A process specification formalism, Fund. informa., 13, 85-139, (1990) · Zbl 0705.68075
[34] Milner, R., A calculus of communicating systems, Lecture notes in computer science, 92, (1980), Springer Berlin · Zbl 0452.68027
[35] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[36] Monk, J.D., Mathematical logic, (1976), Springer Berlin · Zbl 0354.02002
[37] Olderog, E.-R.; Hoare, C.A.R., Specification-oriented semantics for communicating processes, Acta inform., 23, 9-66, (1986) · Zbl 0569.68019
[38] Phillips, I.C.C., Refusal testing, Theoret. comput. sci., 50, 241-284, (1987) · Zbl 0626.68011
[39] Pratt, V.R., Modeling concurrency with partial orders, Internat. J. parallel programming, 15, 33-71, (1986) · Zbl 0622.68034
[40] Robinson, A., On the mechanization of the theory equations, Bull. res. council Israel, 9F, 47-70, (1960)
[41] Sannella, D.T.; Tarlecki, A., Toward formal development of programs from algebraic specifications: implementations revisited, Acta informa., 25, 233-281, (1988) · Zbl 0621.68004
[42] Sannella, D.T.; Wirsing, M., A kernel language for algebraic specification and implementation, (), 413-427, (extended abstract)
[43] Selman, A., Completeness of calculii for axiomatically defined classes of algebras, Algebra universalis, 2, 20-32, (1972) · Zbl 0251.08005
[44] Vaandrager, F.W., Verification of two communication protocols by means of process algebra, Report CS-R8608, (1986), CWI Amsterdam
[45] Vaandrager, F.W., Process algebra semantics of POOL, (), 173-236
[46] Vaandrager, F.W., Algebraic techniques for concurrency and their application, Ph.D. thesis, (1990), Univ. of Amsterdam
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.