×

zbMATH — the first resource for mathematics

Bisimulations for a calculus of broadcasting systems. (English) Zbl 0915.68065
Summary: We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence, we study are justified in terms of a characterization as the largest CBS congruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over finite terms. The first system we give contains an infinitary proof rule to accommodate input prefixes. We improve on this by presenting a finitary proof system where judgements are relative to properties of the data domain.

MSC:
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Amadio, R.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, (), 147-162
[2] Groote, J.F.; Ponse, A., The syntax and semantics of μCRL, ()
[3] Hennessy, M., A proof system for communicating processes with value-passing, J. formal aspects comput. sci., 3, 346-366, (1991) · Zbl 0736.68057
[4] Hennessy, M.; Ingólfsdóttir, A., Communicating processes with value-passing and assignment, J. formal aspects comput. sci., 5, 432-466, (1993) · Zbl 0784.68055
[5] Hennessy, M.; Lin, H., Proof systems for message-passing process algebras, (), 202-216 · Zbl 0857.68040
[6] Hennessy, M.; Lin, H., Symbolic bisimulations, Theoret. comput. sci., 138, 353-389, (1995) · Zbl 0874.68187
[7] Hennessy, M.; Plotkin, G.D., A term model for CCS, (), 261-274 · Zbl 0479.68011
[8] Hennessy, M.; Rathke, J., Strong bisimulations for a calculus of broadcasting systems, () · Zbl 0915.68065
[9] Hennessy, M.; Rathke, J., Weak bisimulations for a calculus of broadcasting systems, () · Zbl 0915.68065
[10] ()
[11] Lin, H., A verification tool for value-passing processes, ()
[12] Milner, R., Communication and concurrency, (1989), Prentice-Hall International Englewood Cliffs, NJ · Zbl 0683.68008
[13] Milner, R.; Sangiorgi, D., Barbed bisimulation, ()
[14] Paczkowski, P., Verifying CBS processes using symbolic semantics, (), 310-323
[15] Prasad, K.V.S., A calculus of broadcast systems, () · Zbl 1260.68276
[16] Prasad, K.V.S., A calculus of value broadcasts, Tech. rep. dept. of computer science, (1992), Chalmers
[17] Prasad, K.V.S., Programming with broadcasts, ()
[18] Sangiorgi, D., Expressing mobility in process algebras: first-order and higher-order paradigms, () · Zbl 0956.68081
[19] Weichert, M., A forked calculus of broadcasting systems, Licentiate thesis, (1995), Chalmers
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.