Causal Semantics for BPP Nets with Silent Moves

• Autorzy: Gorrieri Roberto

Identyfikatory

DOI

10.3233/FI-2021-2039

• Języki publikacji: EN

Abstrakty

EN

BPP nets, a subclass of finite Place/Transition Petri nets, are equipped with some causal behavioral semantics, which are variations of fully-concurrent bisimilarity [3], inspired by weak [28] or branching bisimulation [12] on labeled transition systems. Then, we introduce novel, efficiently decidable, distributed semantics, inspired by team bisimulation [17] and h-team bisimulation [19], and show how they relate to these variants of fully-concurrent bisimulation.

Słowa kluczowe

EN

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

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 180, nr 3
• Strony: 179--249
• Opis fizyczny: Bibliogr. 37 poz., rys.

Twórcy

autor

Gorrieri Roberto

• Dipartimento di Informatica — Scienza e Ingegneria, Università di Bologna, Mura A. Zamboni, 7, 40127 Bologna, Italy

Bibliografia

• [1] Basten T, Branching Bisimilarity is an Equivalence Indeed!, Information Processing Letters 58(3): 141-147, 1996. doi:10.1016/0020-0190(96)00034-8.
• [2] Best E, Devillers R, Sequential and Concurrent Behavior in Petri Net Theory, Theoretical Computer Science 55(1):87-136, 1987. doi:10.1016/0304-3975(87)90090-9.
• [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.
• [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.
• [6] Desel J, Reisig W, Place/Transition Petri Nets, in Lectures on Petri Nets I: Basic Models Advances in Petri Nets, LNCS 1491, 122-173, Springer, 1998. doi:10.1007/3-540-65306-6_15.
• [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 ACM 5 (6):345, 1962. doi:10.1145/367766.368168.
• [9] Fröschle S, Jančar P, Lasota S, Sawa Z, Non-interleaving Bisimulation Equivalences on Basic Parallel Processes, Information and Computation 208(1):42-62, 2010. doi:10.1016/j.ic.2009.06.001.
• [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.
• [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üdiger Olderog on the Occasion of His 60th Birthday, LNCS 9360, 99-130, Springer, 2015. doi:10.1007/978-3-319-23506-6_9.
• [12] van Glabbeek R.J, Weijland W.P, Branching Time and Abstraction in Bisimulation Semantics, Journal of the ACM 43(3):555-600, 1996. doi:10.1145/233551.233556.
• [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.
• [14] Groote J.F, Wijs A, An O(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.
• [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.
• [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.
• [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.
• [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.
• [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, An O(m·log n) Algorithm for Branching Bisimilarity on Labelled Transition Systems, in Procs. TACAS’20, LNCS 12079, 3-20, Springer 2020. doi:10.1007/978-3-030-45237-7_1.
• [22] Jančar 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 Computation 86:43-68, 1990. doi:10.1016/0890-5401(90)90025-D.
• [25] Liberato A, A Study on Bisimulation Equivalence and Team Equivalence Master Thesis of the University of Bologna (supervisor R. Gorrieri), October 2019. URL https://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.
• [27] Milner R, A Complete Axiomatisation for Observational Congruence of Finite-state Behaviours, Information and Computation 81: 227-247, 1989. doi:10.1016/0890-5401(89)90070-9.
• [28] Milner R, Communication and Concurrency, Prentice-Hall, 1989.
• [29] Olderog E.R, Nets, Terms and Formulas, Cambridge Tracts in Theoretical Computer Science 23, Cambridge University Press, 1991. doi:10.1017/CBO9780511526589.
• [30] Paige R, Tarjan R.E, Three Partition Refinement Algorithms, SIAM Jour. of Comp. 16(6):973-989, 1987. doi:10.1137/0216062.
• [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.
• [32] Peterson J.L, Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
• [33] 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. URL https://tel.archives-ouvertes.fr/tel-00005141.
• [34] Rabinovich A, Trakhtenbrot B.A, Behavior Structures and Nets, Fundamenta Informaticae 11(4):357-404, 1988.
• [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.
• [36] Reisig W, Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies, Springer, 2013. doi:10.1007/978-3-642-33278-4.
• [37] Valmari A, Bisimilarity Minimization in O(mlogn) Time, in Procs. Applications and theory of Petri nets, LNCS 5606, 123-142, Springer, 2009. doi:10.1007/978-3-642-02424-5_9.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).