A distributed operational semantics of CCS based on condition/event systems. (English) Zbl 0656.68061

Degano, Pierpaolo; Di Nicola, Rocco; Montanari, Ugo

Acta Inf. 26, No. 1-2, 59-91 (1988).

A new set of inference rules for the guarded version of Milner’s calculus of communicating systems is proposed. They not only describe the actions agents may perform when in a given state, but also say which parts of the agents move when the global state changes. From the transition relation a particular Petri net, namely a condition/event system called \(\Sigma_{CCS}\), is immediately derived. Our construction gives a semantics which is consistent with the interleaving semantics of CCS and exhibits full parallelism. The proof consists of relating the case graph of \(\Sigma_{CCS}\) with the original and with the multiset (step) transition systems of the calculus.

MSC:

68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N25	Theory of operating systems
68Q60	Specification and verification (program logics, model checking, etc.)
68Q65	Abstract data types; algebraic specification

Keywords:

operational semantics; inference rules; calculus of communicating systems; Petri net; condition/event system; interleaving semantics; parallelism

References:

[1]	Austry, D., Boudol, G.P.: Algébre de Processus et Synchronization. Theor. Comput. Sci.30, 91–131 (1984) · Zbl 0533.68026
[2]	Boudol, G., Castellani, I.: On the semantics of concurrency: partial orders and transition systems. In: Ehrig H., Kowalski R., Levi G., Montanari U. (eds.), Proc. TAPSOFT ’87 (Lect. Notes Comput. Sci., vol. 249, pp. 123–137). Berlin Heidelberg New York: Springer 1987 · Zbl 0614.68023
[3]	De Cindio, F., De Michelis, G., Pomello, L., Simone, C.: Milner’s communicating systems and Petri Nets. In: Pagnoni A., Rozenberg G. (eds.) Selected papers from the 3rd European Workshop on Applications and Theory of Petri Nets. (Informatik-Fachberichte, Bd. 66, pp. 40–59). Berlin Heidelberg New York: Springer 1983 · Zbl 0521.68059
[4]	Degano, P., De Nicola, R., Montanari, U.: Partial ordering derivations for CCS. In: Budach L. (ed.) Proc 5th Int. Conf. on Fundamentals of Computation Theory. (Lect. Notes Comput. Sci., vol. 199, pp. 520–523) Berlin Heidelberg New York: Springer 1985 · Zbl 0571.68016
[5]	Degano, P., De Nicola, R., Montanari, U.: Observational equivalences for concurrency models. In: Wirsing M. (ed.) Formal description of programming concepts III, pp. 105–132, Amsterdam Oxford New York: North-Holland 1987
[6]	Degano, P., De Nicola, R., Montanari, U.: CCS is an (augmented) contact-free C/E System. In: Venturini Zilli M. (ed.) (Lect. Notes Comput. Sci. vol. 280, pp. 144–165). Berlin Heidelberg New York: Springer 1987 · Zbl 0635.68058
[7]	Degano, P., De Nicola, R., Montanari, U.: A partial ordering semantics for CCS. Dipartimento di Informatica, Univ. of Pisa, Technical Report TR-3-88 · Zbl 0701.68073
[8]	Degano, P., Montanari, U.: Concurrent histories: a basis for observing distributed systems. J. Comput. Syst. Sci.,34, 422–461 (1987) · Zbl 0619.68017
[9]	De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci.34, 83–133 (1984) · Zbl 0985.68518
[10]	Genrich, H.J., Lautenbach, K., Thiagarajan, P.S.: Elements of general net theory. In: Brauer W., (ed.) Net theory and applications, (Lect. Notes Comput. Sci., vol. 84, pp. 21–163). Berlin Heidelberg New York: Springer 1980 · Zbl 0441.68064
[11]	Glabbeek, R. van, Vaandrager, F.: Petri net models for algebraic theories of concurrency. In: Bakker, J.W. de, Nejman A.J., Treleaven P.C. (eds.) Proc. PARLE Conf. (Lect. Notes Comput. Sci. vol. 259). Berlin Heidelberg New York: Springer 1987. · Zbl 0633.68054
[12]	Goltz, U., Mycroft, A.: On the relationships of CCS and Petri Nets. In: Paredaens, J. (ed.) Proc. 11th ICALP. (Lect. Notes Comput Sci., vol. 172, pp. 196–208). Berlin, Heidelberg New York: Springer 1984 · Zbl 0562.68049
[13]	Keller, R.: Formal verification of parallel programs. Commun. ACM7, 561–572 (1976) · Zbl 0329.68016
[14]	Milner, R.: A calculus of communicating systems. Lect. Notes Comput. Sci., vol. 92. Berlin Heidelberg New York: Springer 1980 · Zbl 0452.68027
[15]	Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci.25, 267–310 (1983) · Zbl 0512.68026
[16]	Milner, R.: Notes on a calculus for communicating systems. In: Broy M. (ed.) Control flow and data flow: concepts of distributed programming. (NATO ASI Series F: vol. 14, pp. 205–228). Berlin Heidelberg New York: Springer 1984.
[17]	Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, Part 1: Theor. Comput. Sci.13, 85–108 (1981) · Zbl 0452.68067
[18]	Olderog, E.-R.: Operational Petri Net semantics for CCSP. In: Rozenberg G. (ed.) Advances in Petri nets 1987. (Lect. Notes Comput. Sci., vol. 266, pp. 196–223) Berlin Heidelberg New York: Springer 1987
[19]	Plotkin, G.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Department of Computer Science, Aarhus, 1981
[20]	Reisig, W.: Petri Nets: an introduction. EACTS Monographs on Theoretical Computer Science, Berlin Heidelberg New York: Springer 1985 · Zbl 0555.68033
[21]	Winskel, G.: Event structure semantics for CCS and related languages. In: Nielsen M., Schmidt E.M. (eds.) Proc 9th ICALP (Lect. Notes Comput. Sci., vol. 140, pp. 561–567). Berlin Heidelberg New York: Springer 1982 · Zbl 0518.68045
[22]	Winskel, G.: Categories of models of concurrency. In: Brookes, S.D., Roscoe A.W. (eds.) Seminar on concurrency (Lect. Notes Comput. Sci., vol. 197, pp. 246–267). Berlin Heidelberg New York: Springer 1985 · Zbl 0567.68017
[23]	Winskel, G.: Petri nets, algebras, morphisms and compositionality. Info. Control72, 197–238 (1987) · Zbl 0622.68052