×
Gorrieri, Roberto

Causal semantics for BPP nets with silent moves. (English) Zbl 1496.68224

Fundam. Inform. 180, No. 3, 179-249 (2021).
Summary: BPP nets, a subclass of finite Place/Transition Petri nets, are equipped with some causal behavioral semantics, which are variations of fully-concurrent bisimilarity [E. Best et al., Acta Inf. 28, No. 3, 231–264 (1991; Zbl 0718.68034)], inspired by weak [R. Milner, Communication and concurrency. New York etc.: Prentice Hall (1989; Zbl 0683.68008)] or branching bisimulation [R. J. van Glabbeek and W. P. Weijland, J. ACM 43, No. 3, 555–600 (1996; Zbl 0882.68085)] on labeled transition systems. Then, we introduce novel, efficiently decidable, distributed semantics, inspired by team bisimulation [the author, Acta Inf. 58, No. 5, 529–569 (2021; Zbl 1497.68339)] and h-team bisimulation [the author, Lect. Notes Comput. Sci. 12152, 153–175 (2020; Zbl 1498.68185)], and show how they relate to these variants of fully-concurrent bisimulation.

Cited in 1 Review
Cited in 1 Document

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

Petri nets; BPP; causality; team bisimulation; weak and branching bisimulation

Citations:

Zbl 0718.68034; Zbl 0683.68008; Zbl 0882.68085; Zbl 1497.68339; Zbl 1498.68185

Software:

Algorithm 97
Cite Review PDF
Full Text: DOI

References:

[1] Basten T , Branching Bisimilarity is an Equivalence Indeed!,Information Processing Letters58(3): 141-147, 1996. doi:10.1016/0020-0190(96)00034-8. · Zbl 0875.68624
[2] Best E, Devillers R, Sequential and Concurrent Behavior in Petri Net Theory,Theoretical Computer Science55(1):87-136, 1987. doi:10.1016/0304-3975(87)90090-9. · Zbl 0669.68043
[3] Best E, Devillers R, Kiehn A, Pomello L, Concurrent Bisimulations in Petri Nets,Acta Inf.28(3): 231-264, 1991. doi:10.1007/BF01178506. · Zbl 0718.68034
[4] Christensen S,Decidability and Decomposition in Process Algebra, Ph.D. Thesis, University of Edinburgh, 1993.
[5] Degano P, De Nicola R, Montanari U, Partial Ordering Descriptions and Observations of Nondeterministic Concurrent Systems, in (J. W. de Bakker, W. P. de Roever, G. Rozenberg, Eds.)Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 438-466, Springer, 1989. doi:10.1007/BFb0013030. · Zbl 0683.68067
[6] Desel J, Reisig W, Place/Transition Petri Nets, inLectures on Petri Nets I: Basic ModelsAdvances in Petri Nets, LNCS 1491, 122-173, Springer, 1998. doi:10.1007/3-540-65306-6 15. · Zbl 0926.68083
[7] Esparza J, Kiehn A, On the Model Checking Problem for Branching-time Logics and Basic Parallel Processes, in Procs. CAV’95, LNCS 939, Springer, 353-366, 1995. doi:10.1007/3-540-60045-0 62.
[8] Floyd R.W, Algorithm 97: Shortest path,Comm. of the ACM5 (6):345, 1962. doi:10.1145/367766.368168.
[9] Fr¨oschle S, Jan˘car P, Lasota S, Sawa Z, Non-interleaving Bisimulation Equivalences on Basic Parallel Processes,Information and Computation208(1):42-62, 2010. doi:10.1016/j.ic.2009.06.001. · Zbl 1185.68444
[10] van Glabbeek R.J, Goltz U, Equivalence Notions for Concurrent Systems and Refinement of Actions, in Procs. MFCS’89, LNCS 379, 237-248, Springer, 1989. doi:10.1007/3-540-51486-4 71. · Zbl 0755.68095
[11] van Glabbeek R.J, Structure Preserving Bisimilarity - Supporting an Operational Petri Net Semantics of CCSP, in (R. Meyer, A. Platzer, H. Wehrheim, Eds.)Correct System Design— Symposium in Honor of Ernst-R¨udiger Olderog on the Occasion of His 60th Birthday, LNCS 9360, 99-130, Springer, 2015. doi:10.1007/978-3-319-23506-6 9. · Zbl 1444.68125
[12] van Glabbeek R.J, Weijland W.P, Branching Time and Abstraction in Bisimulation Semantics,Journal of the ACM43(3):555-600, 1996. doi:10.1145/233551.233556. · Zbl 0882.68085
[13] Groote J.F, Vaandrager F, An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence, in Procs. ICALP’90, LNCS 443, 626-638, Springer, 1990. doi:10.1007/BFb0032063. · Zbl 0765.68125
[14] Groote J.F, Wijs A, AnO(m·log n)Algorithm for Stuttering Equivalence and Branching Bisimulation, in Procs. TACAS’16, LNCS 9636, 607-624, Springer, 2016. doi:10.1007/978-3-662-49674-9 40. · Zbl 1420.68146
[15] Gorrieri R, Versari C,Introduction to Concurrency Theory: Transition Systems and CCS, EATCS Texts in Theoretical Computer Science, Springer, 2015. doi:10.1007/978-3-319-21491-7. · Zbl 1333.68001
[16] Gorrieri R,Process Algebras for Petri Nets: The Alphabetization of Distributed Systems, EATCS Monographs in Theoretical Computer Science, Springer, 2017. doi:10.1007/978-3-319-55559-1. · Zbl 1377.68002
[17] Gorrieri R, Team Bisimilarity, and its Associated Modal Logic, for BPP Nets,Acta Informatica, 2020, doi:10.1007/s00236-020-00377-4.
[18] Gorrieri R, Team Equivalences for Finite-state Machines with Silent Moves,Information and Computation Vol. 275, 2020, doi:10.1016/j.ic.2020.104603. · Zbl 1498.68184
[19] Gorrieri R, A Study on Team Bisimulations for BPP Nets, in Procs. of Petri Nets 2020, LNCS 12152, 153-175, Springer, 2020. doi:10.1007/978-3-030-51831-8 8. · Zbl 1498.68185
[20] Gorrieri R, A Study on Team Bisimulation and H-team Bisimulation for BPP Nets, submitted, 2020.
[21] Jansen D.N, Groote J.F, Keiren J.J.A, Wijs A, AnO(m·log n)Algorithm for Branching Bisimilarity on Labelled Transition Systems, in Procs. TACAS’20, LNCS 12079, 3-20, Springer 2020. doi:10.1007/9783-030-45237-7 1. · Zbl 1483.68232
[22] Jan˘car P, Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete, in Procs. of the 18th IEEE Symposium on Logic in Computer Science (LICS’03), 218-227, IEEE Computer Society Press, 2003. doi:10.1109/LICS.2003.1210061.
[23] Kanellakis P, Smolka S, CCS Expressions, Finite State Processes, and Three Problems of Equivalence, in Procs. 2nd Annual ACM Symposium on Principles of Distributed Computing, 228-240, ACM Press, 1983. doi:10.1145/800221.806724.
[24] Kanellakis P, Smolka S, CCS Expressions, Finite State Processes and Three Problems of Equivalence, Information and Computation86:43-68, 1990. doi:10.1016/0890-5401(90)90025-D. · Zbl 0705.68063
[25] Liberato A,A Study on Bisimulation Equivalence and Team EquivalenceMaster Thesis of the University of Bologna (supervisor R. Gorrieri), October 2019. URLhttps://amslaurea.unibo.it/id/ eprint/19128.
[26] Milner R, A Complete Inference System for a Class of Regular Behaviors,J. Comput. System Sci.28: 439-466, 1984. doi:10.1016/0022-0000(84)90023-0. · Zbl 0562.68065
[27] Milner R, A Complete Axiomatisation for Observational Congruence of Finite-state Behaviours,Information and Computation81: 227-247, 1989. doi:10.1016/0890-5401(89)90070-9. · Zbl 0688.68050
[28] Milner R,Communication and Concurrency, Prentice-Hall, 1989. R. Gorrieri/Causal Semantics for BPP Nets with Silent Moves249
[29] Olderog E.R,Nets, Terms and Formulas, Cambridge Tracts in Theoretical Computer Science 23, Cambridge University Press, 1991. doi:10.1017/CBO9780511526589. · Zbl 0741.68002
[30] Paige R, Tarjan R.E, Three Partition Refinement Algorithms,SIAM Jour. of Comp.16(6):973-989, 1987. doi:10.1137/0216062. · Zbl 0654.68072
[31] Park D.M.R, Concurrency and Automata on Infinite Sequences, in Proc. 5th GI-Conference on Theoretical Computer Science, LNCS 104, 167-183, Springer, 1981. doi:10.1007/BFb0017309. · Zbl 0457.68049
[32] Peterson J.L,Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981. · Zbl 0461.68059
[33] Pinchinat S,Des bisimulations pour la s´emantique des syst‘emes r´eactifs,G´enie logiciel [cs.SE], Ph.D. thesis, Institut National Polytechnique de Grenoble - INPG, 1993. URLhttps://tel. archives-ouvertes.fr/tel-00005141.
[34] Rabinovich A, Trakhtenbrot B.A, Behavior Structures and Nets,Fundamenta Informaticae11(4):357-404, 1988. · Zbl 0657.68068
[35] Ranzato F, Tapparo F, Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation,Inf. Comput. 206(5):620-651, 2008. doi:10.1016/j.ic.2008.01.001. · Zbl 1197.68054
[36] Reisig W,Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies, Springer, 2013. doi:10.1007/978-3-642-33278-4. · Zbl 1278.68222
[37] Valmari A, Bisimilarity Minimization inO(m log n)Time, in Procs. Applications and theory of Petri nets, LNCS 5606, 123-142, Springer, 2009. doi:10.1007/978-3-642-02424-5 9 · Zbl 1242.68186
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.