×

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

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
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Austry, D.; Boudol, G. P., Algébre de Processus et Synchronization, Theor. Comput. Sci., 30, 91-131 (1984) · Zbl 0533.68026 · doi:10.1016/0304-3975(84)90067-7
[2] Boudol, G.; Castellani, I.; Ehrig, H.; Kowalski, R.; Levi, G.; Montanari, U., On the semantics of concurrency: partial orders and transition systems, Proc. TAPSOFT ’87, 123-137 (1987), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0614.68023
[3] De Cindio, F.; De Michelis, G.; Pomello, L.; Simone, C.; Pagnoni, A.; Rozenberg, G., Milner’s communicating systems and Petri Nets, Selected papers from the 3^rd European Workshop on Applications and Theory of Petri Nets, 40-59 (1983), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0521.68059
[4] Degano, P.; De Nicola, R.; Montanari, U.; Budach, L., Partial ordering derivations for CCS, Proc 5^th Int. Conf. on Fundamentals of Computation Theory, 520-523 (1985), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0571.68016 · doi:10.1007/BFb0028836
[5] Degano, P.; De Nicola, R.; Montanari, U.; Wirsing, M., Observational equivalences for concurrency models, Formal description of programming concepts III, 105-132 (1987), Amsterdam Oxford New York: North-Holland, Amsterdam Oxford New York
[6] Degano, P.; De Nicola, R.; Montanari, U.; Venturini Zilli, M., CCS is an (augmented) contact-free C/E System, Lect. Notes Comput. Sci. vol. 280, 144-165 (1987), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · 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 · doi:10.1016/0022-0000(87)90032-8
[9] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518 · doi:10.1016/0304-3975(84)90113-0
[10] Genrich, H. J.; Lautenbach, K.; Thiagarajan, P. S.; Brauer, W., Elements of general net theory, Net theory and applications, 21-163 (1980), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0456.45001
[11] van Glabbeek, R.; Vaandrager, F.; de Bakker, J. W.; Nejman, A. J.; Treleaven, P. C., Petri net models for algebraic theories of concurrency, Proc. PARLE Conf (1987), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York
[12] Goltz, U.; Mycroft, A.; Paredaens, J., On the relationships of CCS and Petri Nets, Proc. 11^th ICALP, 196-208 (1984), Berlin, Heidelberg New York: Springer, Berlin, Heidelberg New York
[13] Keller, R., Formal verification of parallel programs, Commun. ACM, 7, 561-572 (1976)
[14] Milner, R., A calculus of communicating systems (1980), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0452.68027
[15] Milner, R., Calculi for synchrony and asynchrony, Theor. Comput. Sci., 25, 267-310 (1983) · Zbl 0512.68026 · doi:10.1016/0304-3975(83)90114-7
[16] Milner, R.; Broy, M., Notes on a calculus for communicating systems, Control flow and data flow: concepts of distributed programming, 205-228 (1984), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0609.68021
[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 · doi:10.1016/0304-3975(81)90112-2
[18] Olderog, E.-R.; Rozenberg, G., Operational Petri Net semantics for CCSP, Advances in Petri nets 1987, 196-223 (1987), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0636.68072
[19] Plotkin, G., A structural approach to operational semantics (1981), Aarhus: Aarhus University, Department of Computer Science, Aarhus
[20] Reisig, W., Petri Nets: an introduction. EACTS Monographs on Theoretical Computer Science (1985), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0555.68033
[21] Winskel, G.; Nielsen, M.; Schmidt, E. M., Event structure semantics for CCS and related languages, Proc 9^th ICALP (Lect. Notes Comput. Sci., vol. 140, 561-567 (1982), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0518.68045
[22] Winskel, G.; Brookes, S. D.; Roscoe, A. W., Categories of models of concurrency, Seminar on concurrency, 246-267 (1985), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York
[23] Winskel, G., Petri nets, algebras, morphisms and compositionality, Info. Control, 72, 197-238 (1987) · Zbl 0622.68052
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.