Branching place bisimilarity: a decidable behavioral equivalence for finite Petri nets with silent moves. (English) Zbl 1490.68140
Peters, Kirstin (ed.) et al., Formal techniques for distributed objects, components, and systems. 41st IFIP WG 6.1 international conference, FORTE 2021, held as part of the 16th international federated conference on distributed computing techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12719, 80-99 (2021).
Summary: Place bisimilarity \(\sim_p\) is a behavioral equivalence for finite Petri nets, proposed in
[C. Autant et al., “Strong bisimilarity on nets revisited”, Lect. Notes Comput. Sci. 506, 295–312 (1991; doi:10.1007/3-540-54152-7_71)]
and proved decidable in
[the author, “Revisiting the place bisimulation idea: towards formal verification with Petri nets”, Preprint, arXiv:2104.01392].
In this paper we propose an extension to finite Petri nets with silent moves of the place bisimulation idea, yielding branching place bisimilarity \(\approx_p\), following the intuition of branching bisimilarity
[R. J. van Glabbeek and W. P. Weijland, J. ACM 43, No. 3, 555–600 (1996; Zbl 0882.68085)]
on labeled transition systems. We prove that \(\approx_p\) is a decidbale equivalence relation. Moreover, we argue that it is strictly finer than branching fully-concurrent bisimilarity
[the author, Fundam. Inform. 180, No. 3, 179–249 (2021; Zbl 1496.68224);
S. Pinchinat, Des bisimulations pour la sémantique des systèmes réactifs. Grenoble: Institut National Polytechnique de Grenoble (INPG) (PhD Thesis) (1993)],
essentially because \(\approx_p\) does not consider as unobservable those \(\tau \)-labeled net transitions with pre-set size larger than one, i.e., those resulting from multi-party interaction.
For the entire collection see [Zbl 1482.68037].
For the entire collection see [Zbl 1482.68037].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Autant, C.; Belmesk, Z.; Schnoebelen, P.; Aarts, EHL; van Leeuwen, J.; Rem, M., Strong bisimilarity on nets revisited, PARLE ’91 Parallel Architectures and Languages Europe, 295-312 (1991), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-54152-7_71 |
| [2] | Basten, T., Branching bisimilarity is an equivalence indeed!, Inf. Process. Lett., 58, 3, 141-147 (1996) · Zbl 0875.68624 · doi:10.1016/0020-0190(96)00034-8 |
| [3] | Best, E.; Devillers, R.; Kiehn, A.; Pomello, L., Concurrent bisimulations in Petri nets, Acta Inf., 28, 3, 231-264 (1991) · Zbl 0718.68034 · doi:10.1007/BF01178506 |
| [4] | Desel, J.; Reisig, W.; Reisig, W.; Rozenberg, G., Place/transition petri nets, Lectures on Petri Nets I: Basic Models, 122-173 (1998), Heidelberg: Springer, Heidelberg · Zbl 0926.68083 · doi:10.1007/3-540-65306-6_15 |
| [5] | Esparza, J.; Reisig, W.; Rozenberg, G., Decidability and complexity of Petri net problems — an introduction, Lectures on Petri Nets I: Basic Models, 374-428 (1998), Heidelberg: Springer, Heidelberg · Zbl 0926.68087 · doi:10.1007/3-540-65306-6_20 |
| [6] | van Glabbeek, RJ; Weijland, WP, Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600 (1996) · Zbl 0882.68085 · doi:10.1145/233551.233556 |
| [7] | Glabbeek, RJ; Meyer, R.; Platzer, A.; Wehrheim, H., Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP, Correct System Design, 99-130 (2015), Cham: Springer, Cham · Zbl 1444.68125 · doi:10.1007/978-3-319-23506-6_9 |
| [8] | Gorrieri, R.; Versari, C., Introduction to Concurrency Theory (2015), Cham: Springer, Cham · Zbl 1333.68001 · doi:10.1007/978-3-319-21491-7 |
| [9] | Gorrieri, R.: Process Algebras for Petri Nets: The Alphabetization of Distributed Systems. EATCS Monographs in Computer Science, Springer, Heidelberg (2017). doi:10.1007/978-3-319-55559-1 · Zbl 1377.68002 |
| [10] | Gorrieri, R.: Team bisimilarity, and its associated modal logic, for BPP nets. Acta Informatica 1-41 (2020). doi:10.1007/s00236-020-00377-4 · Zbl 1497.68339 |
| [11] | Gorrieri, R.: Team equivalences for finite-state machines with silent moves. Inf. Comput. 275 (2020). doi:10.1016/j.ic.2020.104603 · Zbl 1498.68184 |
| [12] | Gorrieri, R.: Causal semantics for BPP nets with silent moves. Fundam. Inform. (2020, to appear) · Zbl 1496.68224 |
| [13] | Gorrieri, R.: Place bisimilarity is decidable, indeed!, arXiv:2104.01392, April 2021 |
| [14] | Hopcroft, JE; Karp, RM, An \(n^{5/2}\) algorithm for maximum matchings in bipartite graphs, SIAM J. Comput., 2, 4, 225-231 (1973) · Zbl 0266.05114 · doi:10.1137/0202019 |
| [15] | Janc̆ar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theoret. Comput. Sci. 148(2), 281-301 (1995) · Zbl 0873.68147 |
| [16] | Keller, R., Formal verification of parallel programs, Commun. ACM, 19, 7, 561-572 (1976) · Zbl 0329.68016 · doi:10.1145/360248.360251 |
| [17] | Milner, R.: Communication and Concurrency. Prentice-Hall (1989) · Zbl 0683.68008 |
| [18] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Inf. Comput., 100, 1, 1-77 (1992) · Zbl 0752.68036 · doi:10.1016/0890-5401(92)90008-4 |
| [19] | Olderog, E.R.: Nets, Terms and Formulas, Cambridge Tracts in Theoretical Computer Science 23. Cambridge University Press (1991) · Zbl 0741.68002 |
| [20] | Park, D.; Deussen, P., Concurrency and automata on infinite sequences, Theoretical Computer Science, 167-183 (1981), Heidelberg: Springer, Heidelberg · Zbl 0457.68049 · doi:10.1007/BFb0017309 |
| [21] | Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice-Hall (1981) · Zbl 0461.68059 |
| [22] | Pinchinat, S.: Des bisimulations pour la sémantique des systèmes réactifs, Génie logiciel [cs.SE]. Ph.D. thesis, Institut National Polytechnique de Grenoble - INPG (1993) |
| [23] | Reisig, W.: Petri Nets: An Introduction, EATCS Monographs in Theoretical Computer Science, Springer, Heidelberg (1985). doi:10.1007/978-3-642-69968-9 · Zbl 0555.68033 |
| [24] | Sangiorgi, D., Walker, D.: The \(\pi \)-calculus: A Theory of Mobile Processes. Cambridge University Press (2001) · Zbl 0981.68116 |
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.
