×

zbMATH — the first resource for mathematics

Concurrent bisimulations in Petri nets. (English) Zbl 0718.68034
Bisimulations defined in terms of execution sequences cannot distinguish between a concurrent system and its sequential simulation. The authors consider a model of concurrency, Petri nets, which display concurrency in an explicit way, and introduce a concept of bisimulation, fully concurrent bisimulation or FC-bisimulation, that is stronger than ordinary bisimulation, is equivalent to ordinary bisimulation in the sequential case, and, under some conditions, is preserved by refinement of atomic actions.
For net systems sequential bisimulation is defined in terms of a relation which puts states into correspondence, among which the initial ones, such that the visible evolutions of them are the same and lead to correspondent states. Equivalently, this bisimulation can be defined in terms of simple transitions or in terms of occurrence sequences. The failure of sequential bisimulation (as well as of bisimulations considering general step sequences instead of interleavings) in the case of systems containing concurrent actions suggests generalizations based on partial orderings, i.e. on sets of processes. A first proposal is concurrent bisimulation which puts states into correspondence, among which the initial ones, such that visible concurrent evolutions of them are order isomorphic and lead to correspondent states. This bisimulation, which is similar to CCS pomset bisimulation, does not withstand a refinement.
Finally, FC-bisimulation is defined requiring that there is a relation between processes such that initial processes are related, related processes have order isomorphic abstractions and any extension of a process \(\pi\) is related to an extension of a process related to \(\pi\). The resulting notion corresponds to BS-bisimulation introduced for behaviour structures and to history peserving bisimulation defined for event structures. FC-bisimulation implies concurrent bisimulation and the above mentioned bisimulation definitions collapse for sequential systems. Besides properties preserved also by sequential bisimulations (like liveness of any visible operation and generated language), FC- bisimulation preserves the absence of auto-concurrency and auto- concurrent actions. For other properties, one may wonder whether for any system which does not enjoy the property there is one which has it. So the authors prove that for a system without auto-concurrency there exists one which is strict. Finally, FC-bisimulation is shown to be a congruence for many kinds of refinement and under some conditions on nets.

MSC:
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aceto, L., Hennessy, M.: Towards action-refinement in process algebras. Report 3/88, Computer Science Department, University of Sussex (1988). Also in Proc. LICS 89 (Asilomar, California), IEEE Computer Society Press, pp. 138-145 (1989) · Zbl 0716.68034
[2] Best, E.: COSY: Its relation to nets and to CSP. In: Brauer, W., et al. (eds.) Advances in Petri Nets 1986. Proc. of Advanced Course on Petri Nets, Bad Honnef (1986) (Lect. Notes Comput. Sci., vol. 255, pp. 216-220) Berlin Heidelberg New York: Springer 1987
[3] Best, E., Devillers, R.: Sequential and concurrent behaviour in Petri net theory. TCS55, No. 1 (1988) · Zbl 0669.68043
[4] Best, E., Fernández, C.: Notation and terminology on Petri net theory. Arbeitspapiere der GMD Nr. 195 (1987)
[5] Boudol, G., Castellani, I.: On the semantics of concurrency: Partial orders and transition systems. In: Ehrig, H. (ed.) Proceedings TAPSOFT 87, Vol. 1 (Lect. Notes Comput. Sci., vol. 249, pp. 123-137. Berlin Heidelberg New York: Springer 1987 · Zbl 0614.68023
[6] Brauer, W., Gold, R., Vogler, W.: Behaviour and equivalence preserving refinements of Petri Nets. Draft paper, Techn. Univ. München, submitted to Advances in Petri Nets 1990 (Lect. Notes Comput. Sci.). Berlin Heidelberg New York: Springer (accepted for publication)
[7] Castellano, L., de Michelis, G., Pomello, L.: Concurrency vs. interleaving: an instructive example. Bull. EATCS31, 12-15 (1987) · Zbl 1023.68635
[8] Darondeau, Ph., Degano, P.: Event structures, causal trees and refinements. In: Rovan, B. (ed.) Proc. of Mathematical Foundations of Computer Science 90. (Lect. Notes Comput. Sci., vol. 452, pp. 237-245). Berlin Heidelberg New York: Springer 1990 · Zbl 0733.68027
[9] de Cindio, F., de Michelis, G., Pomello, L., Simone, C.: A Petri net model of CSP. Proc. CIL’81, Barcelona (1981) · Zbl 0521.68059
[10] de Cindio, F., de Michelis, G., Pomello, L., Simone, C.: Milner’s communicating systems and Petri Nets. In: Pagnoni, A., Rozenberg, G. (eds.), Application and Theory of Petri Nets (Inf. Fachber., vol. 66, pp. 40-59). Berlin Heidelberg New York: Springer 1983 · Zbl 0521.68059
[11] Degano, P., de Nicola, R., Montanari, U.: Observational equivalences for concurrency models. Formal descr. of programming concepts III. Wirsing, M. (ed.), pp. 105-132. Amsterdam: North Holland 1987
[12] Degano, P., de Nicola, R., Montanari, U.: A distributed operational semantics for CCS based on condition/event systems. Acta Inf.26, 59-91 (1988) · Zbl 0656.68061
[13] Degano, P., Gorrieri, R., Marchetti, S.: An exercise in concurrency: A CSP process as a condition/event system: In: Rozenberg, G. (ed.) Advances in Petri Nets 1988. (Lect. Notes Comput. Sci., vol. 340, pp. 85-105) Berlin Heidelberg New York: Springer 1988 · Zbl 0668.68069
[14] Devillers, R.: On the definition of a bisimulation notion based on partial words. Petri Net Newsletter29, 16-19 (1988)
[15] Devillers, R.: Maximality preserving bisimulation. Technical Report LIT-214, Univ. Bruxelles (1990) · Zbl 0780.68036
[16] van Glabbeek, R.: The refinement theorem for ST-bisimulation semantics. Proc. IFIP Working Group Conference on Programming Concepts and Methods. Broy, M., Jones, C.B. (eds.) (to appear 1990)
[17] van Glabbeek, R., Goltz, U.: Equivalence notions for concurrent systems and refinement of actions. Arbeitspapiere der GMD 366 (1989) Extended abstract in: Kreczmar, A., Mirkowska, G. (eds.) Mathematical Foundations of Computer Science (Lect. Notes Comput. Sci., vol. 379, pp. 237-248). Berlin Heidelberg New York: Springer 1989 · Zbl 0755.68095
[18] van Glabbeek, R., Goltz, U.: Refinement of actions in causality based models. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.). Stepwise refinement of distributed systems. Models, formalisms, correctness (Lect. Notes Comput. Sci., vol. 430, pp. 267-300). Berlin Heidelberg New York: Springer 1990
[19] van Glabbeek, R., Goltz, U.: Equivalence notions and refinement of actions for flow event structures. In DEMON deliverables. Esprit BRA 3148 (1990) · Zbl 0969.68081
[20] van Glabbeek, R., Vaandrager, F.: Petri net models for algebraic concurrency. Proc. of PARLE Conference. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE. Parallel Architectures and Languages Europe. Vol. 2. (Lect. Notes Comput. Sci., vol. 259, pp. 224-242). Berlin Heidelberg New York: Springer 1987 · Zbl 0633.68054
[21] van Glabbeek, R., Weijland, W.: Refinement in branching time semantics. Proceedings of the International Conference on Algebraic Methodology and Software Technology-Iowa City, USA (1989) · Zbl 0882.68085
[22] Goltz, U.: On representing CCS programs by finite Petri nets. Arbeitspapiere der GMD (1988) · Zbl 0649.68015
[23] Goltz, U., Reisig, W.: CSP programs as nets with individual tokens (Lect. Notes Comput. Sci., vol. 188, pp. 169-196). Berlin Heidelberg New York: Springer 1985 · Zbl 0571.68044
[24] Lauer, P.E., Campbell, R.: Formal semantics of a class of high-level primitives for coordinating concurrent processes. Acta Inf.5, 297-332 (1975) · Zbl 0312.68012
[25] Milner, R.: A calculus of communicating systems (Lect. Notes Comput. Sci., vol. 92). Berlin Heidelberg New York: Springer 1980 · Zbl 0452.68027
[26] Nielsen, M., Thiagarajan, P.S.: Degrees of non-determinism and concurrency: A Petri net view. 4th Conf. on Found. of Softw. Techn. and Theor. Comp. Science, pp. 89-117. Berlin Heidelberg New York: Springer 1984 · Zbl 0595.68051
[27] Park, D.: Concurrency and automata on finite sequences. Computer Science Department, University of Warwick (1981) · Zbl 0457.68049
[28] Pomello, L.: Some equivalence notions for concurrent systems. An overview. In: Rozenberg, G. (ed.) Advances in Petri nets 1985 (Lect. Notes Comput. Sci. vol. 222, pp. 381-400). Berlin Heidelberg New York: Springer 1986
[29] Pomello, L.: Observing net behaviour. In: Voss, K., et al. (eds.) Concurrency and nets, pp. 403-421. Berlin Heidelberg New York: Springer 1987 · Zbl 0641.68084
[30] Pomello, L.: Osservatore, reti di Petri, Processi. Ph.D. Thesis, University of Milano and Torino-Italy (1988)
[31] Pomello, L., Simone, C.: A survey of equivalence notions for net based systems. Draft paper, Univ. Milano. In: Rozenberg, G. (ed.) Advances in Petri nets 1991 (Lect. Notes Comput. Sci.). Berlin Heidelberg New York: Springer (to be published)
[32] Pomello, L., Simone, C.: A state transformation preorder over a class of EN systems. In: Rozenberg, G. (ed.) Advances in Petri nets 1990 (Lect. Notes Comput. Sci.). Berlin Heidelberg New York: Springer 1990
[33] Rozenberg, G., Verraedt, R.: Subset languages of Petri nets (Lect. Notes Comput. Sci., vol. 66) (also: TCS 26, pp. 301-323, 1983). Berlin Heidelberg New York: Springer 1978 · Zbl 0531.68029
[34] Rabinovitch, A., Trakhtenbrot, B.A.: Behaviour structures and nets. Fundamenta Informaticae XI, 357-404 (1988) · Zbl 0657.68068
[35] Vogler, W.: Failures semantics based on interval semiwords is a congruence for refinement. In: Choffrut, C., Lengauer, T. (eds.) Proc. STACS 90 (Lect. Notes Comput. Sci., vol. 415, pp. 285-297). Berlin Heidelberg New York: Springer 1990 · Zbl 0729.68069
[36] Vogler, W.: Bisimulation and action refinement. SFB-Bericht 342/10/90A, Techn. Univ. München (1990) · Zbl 0773.68052
[37] Vogler, W.: Failures semantics of Petri nets and the refinement of places and transitions. Technical Report TUM-I9003, Techn. Univ. München (1990)
[38] Voss, K.: System specification with labelled nets and the notion of interface equivalence. Arbeitspapiere der GMD 211 (1986)
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.