Abstract
Closed CCS (CCCS) is a CCS-like algebra of processes with a generalized form of prefixing based on a full-fledged algebra of transitions rather than on basic actions only. The basic idea is that the generalized prefixing operator takes a transition t, or rather its observation ω, a process E and yields the process t.E. From an operational standpoint, the process t.E may evolve to E by performing a transition labelled by ω. By exploiting the algebra of transitions, we define a general form of expansion theorem which is the heart of a finite axiomatization of a strong observational equivalence for finite CCCS agents. By adding the axioms concerning the interpretation of the operations of the algebra of observations, we still obtain a sound and complete axiomatization of the corresponding bisimulation equivalence. For instance, it is possible to define the classical expansion theorem, or versions of it which handle partial ordering based observations.
Work partially supported by ESPRIT Basic Research Action 3011, CEDISYS, and by Progetto Finalizzato Informatica e Calcolo Parallelo, obiettivo LAMBRUSCO
Chapter PDF
Similar content being viewed by others
Keywords
- Equational Theory
- Operational Semantic
- Parallel Composition
- Communicate Sequential Process
- Proper Transition
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Austry, D. Boudol, G. Algebre de Processus et Synchronization, Theoretical Computer Science 30 (1), pp 91–131, 1984.
Boudol, G., Castellani, I., Concurrency and Atomicity, Theoretical Computer Science 59 (1,2), pp. 25–84, 1988.
Boudol, G., Castellani, I., Permutations of Transitions: An Event Structure Semantics for CCS, In Proc. REX School, Workshop on Linear Time Branching Time and Partial Orders in Logics and Models for Concurrency, LNCS 354, pp 411–437 1989.
Boudol, G., Castellani, I., Three Equivalent Semantics Semantics for CCS, In Semantics of Systems of Concurrent Processes, LNCS 469, pp 96–141, 1990.
de Bakker, J.W., Kok, J.N., Uniform Abstraction, Atomicity and Contractions in the Comparative Semantics of Concurrent Prolog, in Proc. of Int. Conf. on Fifth Generation Computer Systems Tokyo, 1988.
Brookes, S.D., Hoare, C.A.R., Roscoe, A.D., A Theory of Communicating Sequential Processes, Journal of ACM 31 (3), pp 560–599, 1984.
Bergstra, J., Klop, W., Process Algebra for Synchronous Communication, Information and Control 60, pp 109–137, 1984.
Bergstra, J., Klop, W., Algebra of Communicating Processes with Abstraction, Theoretical Computer Science, 37, (1), pp 77–121, 1985.
Darondeau, P., Degano, P. Causal Trees, In Proc. ICALP 89, LNCS 372, pp 234–248, 1989.
Darondeau, P., Degano, P., Causal Tree = Interleaving + Causality, In Semantics of Systems of Concurrent Processes, LNCS 469, pp 239–255, 1990.
Degano, P., De Nicola, R., Montanari, U. Partial ordering derivations for CCS, Proc. 5th Int. Conf. Fundamentals of Computation Theory, LNCS 199, pp. 520–533, 1985.
Degano, P. De Nicola, R., Montanari, U. Observational Equivalences for Concurrency Models, in Formal Description of Programming Concepts III, M. Wirsing, ed., North Holland, pp 105–132, 1987.
Degano, P. De Nicola, R., Montanari, U. A Distributed Operational Semantics for CCS Based on Condition/Event Systems. Acta Informatica, 26, pp 59–91, 1988.
Degano, P. De Nicola, R., Montanari, U. On the Consistency of Truly Concurrent Operational and Denotational Semantics. Proc. LICS 88, IEEE Computer Society Press, pp 133–141, 1988.
Degano, P. De Nicola, R., Montanari, U. Partial Ordering Descriptions and Observations of Nondeterministic Concurrent Processes, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, pp 438–466, 1989.
Degano, P. De Nicola, R., Montanari, U. A Partial Ordering Semantics for CCS, Theoretical Computer Science (75), pp. 223–262, 1990.
Degano, P., De Nicola, R., Montanari, U. On the Operational Semantics of Distributed Concurrent Systems in: Declarative Systems (G. David, R.T. Boute, and B.D. Shriver Eds) Proc. IFIP 10.1 Workshop on Concepts and Characteristics of Declarative Systems, North-Holland, Amsterdam, 1990.
Degano, P. De Nicola, R., Montanari, U. Universal Axioms for Bisimulation, Submitted for Publication, 1991.
Degano, P., Gorrieri, R., Atomic Refinement in Process Description Languages, Submitted for Publication, 1990.
Degano, P., Meseguer, J., Montanari, U., Axiomatizing Net Computations and Processes, in LICS 89, IEEE Computer Society Press, pp 175–185, 1989.
Degano, P., Montanari, U., Concurrent Histories: A Basis for Observing Distributed Systems, Journal of Computer and System Sciences 34, pp 422–461, 1987.
Ferrari, G. Unifying Models of Concurrency, PhD Thesis, TD/4-90, Dipartimento di Informatica, Univ. Pisa, 1990.
Ferrari, G., Montanari, U., Towards the Unification of Models for Concurrency, Proc. CAAP'90, LNCS 431, pp 162–176, 1990.
Ferrari, G., Montanari, U., Mowbray, M. On Causality Observed Incrementally, Finally, To appear Proc. TAPSOFT — CAAP 91, LNCS, 1991.
Ferrari, G., Montanari, U., Mowbray, M. Causal Streams: Tracing Causality in Distributed Systems, Submitted for publication, 1991.
Gischer, J. The Equational Theory of Pomsets, Theoretical Computer Science 61, 1988.
Goltz, U. On Representing CCS Programs by Finite Petri Nets, Proc. MFCS 88, LNCS 324, pp 339–350, 1988.
Gorrieri, R. Refinement, Atomicity and Transactions for Process Description Languages, PhD Thesis, Dipartimento di Informatica, Univ. Pisa, 1991.
Grabowski, J. On Partial Languages, Fundamenta Informaticae, IV 2, pp 427–498, 1981.
van Glabbeek, R., Goltz, U., Equivalence Notions for Concurrent Systems and Refinement of Actions, Proc. MFCS '89, LNCS 397, pp 237–248, 1989.
Gorrieri, R., Montanari, U., SCONE: a Simple Calculus of Nets, In Proc. CONCUR'90, LNCS 458, pp 2–30, 1990.
Gorrieri, R., Marchetti, S., Montanari, U. S 2CCS:Atomic Actions for CCS, Theoretical Computer Science, 72, pp 203–223 1990.
Goltz, U., Reisig, W., The Non Sequential Behaviour of Petri Nets, In formation and Computation 57, pp 125–147, 1983.
Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall, 1985.
Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM 32 (1), pp 137–141, 1985.
Hennessy, M. An Algebraic Theory of Processes, MIT Press, 1988.
Milner, R., A Calculus of Communicating Systems, LNCS 92, 1980.
Milner, R., Communication and Concurrency, Prentice Hall, 1989.
Moller, F. The Nonexistence of Finite Axiomatizations for CCS Congruences, Proc. LICS'90, IEEE Press, pp 142–153 1990.
Moller, F. The Importance of the Left Merge Operator in Process Algebras, Proc. ICALP'90, LNCS 443, pp 752–764, 1990.
Meseguer, J. Montanari, U. Petri Nets are Monoids: A new Algebraic Formulation of Net Theory, Information and Computation, 88 (2), pp 105–155, 1990.
Montanari, U. Yankelevich, D. An Algebraic View of Interleaving and Distributed Operational Semantics, In Proc. Third Symposium on Category Theory and Computer Science, LNCS 389, pp 5–20, 1989.
Park, D., Concurrency and Automata on Infinite Sequences, in Proc. GI, LNCS 104, pp 167–183, 1981.
Nielsen, M., Plotkin, G. Winskel, G. Petri Nets, Event Structures and Domains (Part I). Theoretical Computer Science, 13 (1), pp 85–108, 1981.
Olderog, E.-R., Operational Petri Nets Semantics for CCSP, in Advances in Petri Nets 87, LNCS 266, pp 196–223, 1987.
Plotkin, G. A Structured Approach to Operational Semantics, DAIMI FN-19, Computer Science Dept. University of Aarhus, 1981.
Pratt, V., Modelling Concurrency with Partial Orders, Int. Journal of Parallel Programming 15, (1), pp 381–400, 1986.
Rabinovich, A. Trakhtenbrot, B. Behaviour Structures and Nets, Fundamenta Informaticae XI, pp 357–404,1988.
Reisig, W. Petri Nets: An Introduction, EATCS Monograph, Springer, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrari, G.L., Gorrieri, R., Montanari, U. (1991). An extended expansion theorem. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. TAPSOFT 1991. Lecture Notes in Computer Science, vol 494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540539816_56
Download citation
DOI: https://doi.org/10.1007/3540539816_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53981-0
Online ISBN: 978-3-540-46499-0
eBook Packages: Springer Book Archive