Team bisimilarity, and its associated modal logic, for BPP nets. (English) Zbl 1497.68339
Summary: BPP nets, a subclass of finite Place/Transition Petri nets, are equipped with an efficiently decidable, truly concurrent, bisimulation-based, behavioral equivalence, called team bisimilarity. This equivalence is a very intuitive extension of classic bisimulation equivalence (over labeled transition systems) to BPP nets and it is checked in a distributed manner, without necessarily building a global model of the overall behavior of the marked BPP net. An associated distributed modal logic, called team modal logic (TML, for short), is presented and shown to be coherent with team bisimilarity: two markings are team bisimilar if and only if they satisfy the same TML formulae. As the process algebra BPP (with guarded summation and guarded body of constants) is expressive enough to represent all and only the BPP nets, we provide algebraic laws for team bisimilarity as well as a finite, sound and complete, axiomatization.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
| 03B70 | Logic in computer science |
Software:
SLMCReferences:
| [1] | Acciai, L., Boreale, M., Zavattaro, G.: On the relationship between spatial logics and behavioral simulations. In: Proceedings of the Fossacs’10, LNCS, vol. 6014, pp. 146-160. Springer, Berlin (2010) · Zbl 1284.03204 |
| [2] | Aceto, L., Relating distributed, temporal and causal observations of simple processes, Fundam. Inf., 17, 4, 319-331 (1992) · Zbl 0847.68032 |
| [3] | Aceto, L.; Ingólfsdóttir, A.; Larsen, K.; Srba, J., Reactive Systems: Modelling, Specification and Verification (2007), Cambridge: Cambridge University Press, Cambridge · Zbl 1141.68043 · doi:10.1017/CBO9780511814105 |
| [4] | Autant, C., Belmesk, Z., Schnoebelen, Ph.: Strong bisimilarity on nets revisited. In: Proceedings of the PARLE’91, vol. II: Parallel Languages, LNCS, vol. 506, pp. 295-312. Springer, Berlin (1991) |
| [5] | Autant, C., Schnoebelen, Ph.: Place bisimulations in Petri nets. In: Proceedings of the Application and Theory of Petri Nets 1992, LNCS, vol. 616, pp. 45-61. Springer, Berlin (1992) |
| [6] | Best, E.; Devillers, R., Sequential and concurrent behavior in Petri net theory, Theor. Comput. Sci., 55, 1, 87-136 (1987) · Zbl 0669.68043 · doi:10.1016/0304-3975(87)90090-9 |
| [7] | 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 |
| [8] | Baldan, P.; Crafa, S., A logic for true concurrency, J. ACM, 61, 4, 24:1-24:36 (2014) · Zbl 1321.68355 · doi:10.1145/2629638 |
| [9] | Bednarczyk, M.: Hereditary History Preserving Bisimulation or What is the Power of the Future Perfect in Program Logics, Technical report. Polish Academy of Sciences, Gdansk (1991) |
| [10] | Bradfield, JC; Fröschle, SB, Independence-friendly modal logic and true concurrency, Nord. J. Comput., 9, 1, 102-117 (2002) · Zbl 1020.68061 |
| [11] | Caires, L.; Cardelli, L., A spatial logic for concurrency (part I), Inf. Comput., 186, 2, 194-235 (2003) · Zbl 1068.03022 · doi:10.1016/S0890-5401(03)00137-8 |
| [12] | Castellani, I.; Hennessy, M., Distributed bisimulations, J. ACM, 36, 4, 887-911 (1989) · Zbl 0697.68076 · doi:10.1145/76359.76369 |
| [13] | Castellani, I.; Bergstra, JA; Ponse, A.; Smolka, SA, Process algebras with localities, Chap 15 Handbook of Process Algebra, 945-1046 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0971.00006 · doi:10.1016/B978-044482830-9/50033-3 |
| [14] | Christensen, S.: Decidability and Decomposition in Process Algebra, Ph.D. Thesis, University of Edinburgh (1993) |
| [15] | Darondeau, Ph., Degano, P.: Causal trees. In: Proceedings of the ICALP’89, LNCS, vol. 372, pp. 234-248. Springer, Berlin (1989) |
| [16] | Degano, P.; De Nicola, R.; Montanari, U.; de Bakker, JW; de Roever, WP; Rozenberg, G., Partial ordering descriptions and observations of nondeterministic concurrent systems, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, REX School/Workshop, 438-466 (1989), Berlin: Springer, Berlin · Zbl 0683.68067 · doi:10.1007/BFb0013030 |
| [17] | Davey, BA; Priestley, HA, Introduction to Lattices and Order (2002), Cambridge: Cambridge University Press, Cambridge · Zbl 1002.06001 · doi:10.1017/CBO9780511809088 |
| [18] | Esparza, J., Kiehn, A.: On the model checking problem for branching-time logics and basic parallel processes. In: Proceedings of the CAV’95, LNCS, vol. 939, pp. 353-366. Springer, Berlin (1995) |
| [19] | Esparza, J.: Decidability and complexity of Petri net problems: an introduction. In: Lectures on Petri Nets I: Basic Models, LNCS, vol. 1491, pp. 374-428. Springer, Berlin (1998) · Zbl 0926.68087 |
| [20] | Fröschle, S.: Decidability of plain and hereditary history-preserving bisimulation for BPP. In: Proceedings of the EXPRESS’99, ENTCS 27 (1999) · Zbl 0958.68101 |
| [21] | Fröschle, S.: Composition and decomposition in true-concurrency. In: Proceedings of the Fossacs’05, LNCS, vol. 3441, pp. 333-347. Springer, Berlin (2005) · Zbl 1118.68570 |
| [22] | Fröschle, S., Lasota, S.: Decomposition and complexity of hereditary history preserving bisimulation on BPP. In: Proceedings of the CONCUR’05, LNCS, vol. 3656, pp. 263-277. Springer, Berlin (2005) · Zbl 1134.68434 |
| [23] | Fröschle, S., Janc̆ar, P., Lasota, S., Sawa, Z.: Non-interleaving bisimulation equivalences on basic parallel processes. Inf. Comput. 208(1), 42-62 (2010) · Zbl 1185.68444 |
| [24] | Gorrieri, R.; Roccetti, M.; Stancampiano, E., A theory of processes with durational actions, Theor. Comput. Sci., 140, 1, 73-94 (1995) · Zbl 0874.68113 · doi:10.1016/0304-3975(94)00205-W |
| [25] | Gorrieri, R., Versari, C.: Introduction to concurrency theory: transition systems and CCS. In: EATCS Texts in Theoretical Computer Science. Springer, Berlin (2015) · Zbl 1333.68001 |
| [26] | Gorrieri, R.: Process algebras for Petri nets: the alphabetization of distributed systems. In: EATCS Monographs in Theoretical Computer Science. Springer, Berlin (2017) · Zbl 1377.68002 |
| [27] | Gorrieri, R., Verification of finite-state machines: a distributed approach, J. Log. Algebr. Methods Program., 96, 65-80 (2018) · Zbl 1430.68152 · doi:10.1016/j.jlamp.2017.11.005 |
| [28] | Gorrieri, R.: Axiomatizing team equivalence for finite-state machines. In: The Art of Modeling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Catuscia Palamidessi’s Festschrift, LNCS, vol. 11760, pp. 14-32. Springer, Berlin (2019) · Zbl 1535.68162 |
| [29] | Gorrieri, R.: A Study on Team Bisimulations for BPP nets, submitted for publication (2020) |
| [30] | Gorrieri, R.: Interleaving vs True Concurrency: Some Instructive Security Examples, submitted for publication (2020) · Zbl 1503.68191 |
| [31] | Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021 · doi:10.1145/2455.2460 |
| [32] | Hopcroft, JE; Motwani, R.; Ullman, JD, Introduction to Automata Theory, Languages and Computation (2001), Reading: Addison-Wesley, Reading · Zbl 0980.68066 |
| [33] | Janc̆ar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281-301 (1995) · Zbl 0873.68147 |
| [34] | Janc̆ar, P.: Strong bisimilarity on basic parallel processes is PSPACE-complete. In: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS’03), pp. 218-227. IEEE Computer Society Press (2003) |
| [35] | Joyal, A.; Nielsen, M.; Winskel, G., Bisimulation from open maps, Inf. Comput., 127, 164-185 (1996) · Zbl 0856.68067 · doi:10.1006/inco.1996.0057 |
| [36] | Keller, R., Formal verification of parallel programs, Commun. ACM, 19, 7, 561-572 (1976) · Zbl 0329.68016 · doi:10.1145/360248.360251 |
| [37] | Kozen, D., Results on the propositional mu-calculus, Theor. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6 |
| [38] | Lasota, S., Decidability of performance equivalence for basic parallel processes, Theor. Comput. Sci., 360, 1-3, 172-192 (2006) · Zbl 1099.68070 · doi:10.1016/j.tcs.2006.02.020 |
| [39] | Liberato, A.: A Study on Bisimulation Equivalence and Team Equivalence, Master Thesis of the University of Bologna (supervisor R. Gorrieri) (2019) |
| [40] | Milner, R., A complete inference systems for a class of regular behaviors, J. Comput. Syst. Sci., 28, 439-466 (1984) · Zbl 0562.68065 · doi:10.1016/0022-0000(84)90023-0 |
| [41] | Milner, R., Communication and Concurrency (1989), Englewood Cliffs: Prentice-Hall, Englewood Cliffs · Zbl 0683.68008 |
| [42] | Milner, R.; Moller, F., Unique decomposition of processes, Theor. Comput. Sci., 107, 2, 357-363 (1993) · Zbl 0777.68037 · doi:10.1016/0304-3975(93)90176-T |
| [43] | Olderog, ER, Nets, Terms and Formulas, Cambridge Tracts in Theoretical Computer Science (1991), Cambridge: Cambridge University Press, Cambridge · Zbl 0741.68002 · doi:10.1017/CBO9780511526589 |
| [44] | Park, D.M.R.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science, LNCS, vol. 104, pp. 167-183. Springer, Berlin (1981) · Zbl 0457.68049 |
| [45] | Peterson, JL, Petri Net Theory and the Modeling of Systems (1981), Englewood Cliffs: Prentice-Hall, Englewood Cliffs · Zbl 0461.68059 |
| [46] | Pomello, L., Rozenberg, G., Simone, C.: A survey of equivalence notions for net based systems. In: Advances in Petri Nets: The DEMON Project, LNCS, vol. 609, pp. 410-472. Springer, Berlin (1992) |
| [47] | Paige, R.; Tarjan, RE, Three partition refinement algorithms, SIAM J. Comput., 16, 6, 973-989 (1987) · Zbl 0654.68072 · doi:10.1137/0216062 |
| [48] | Rabinovich, A.; Trakhtenbrot, BA, Behavior structures and nets, Fundam. Inf., 11, 4, 357-404 (1988) · Zbl 0657.68068 |
| [49] | Reisig, W., Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies (2013), Berlin: Springer, Berlin · Zbl 1278.68222 · doi:10.1007/978-3-642-33278-4 |
| [50] | Sangiorgi, D., An Introduction to Bisimulation and Coinduction (2012), Cambridge: Cambridge University Press, Cambridge · Zbl 1252.68008 |
| [51] | van Glabbeek, R.J., Vaandrager, F.W.: Petri net models for algebraic theories of concurrency. In: Proceedings of the PARLE’87, LNCS, vol. 259, pp. 224-242. Springer, Berlin (1987) · Zbl 0633.68054 |
| [52] | van Glabbeek, R.J., Goltz, U.: Equivalence notions for concurrent systems and refinement of actions. In: Proceedings of the MFCS’89, LNCS 379, pp. 237-248. Springer, Berlin (1989) · Zbl 0755.68095 |
| [53] | 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 |
| [54] | van Glabbeek, RJ; Meyer, R.; Platzer, A.; Wehrheim, H., Structure preserving bisimilarity—supporting an operational Petri Net semantics of CCSP, Correct System Design—Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, LNCS, 99-130 (2015), Berlin: Springer, Berlin · Zbl 1444.68125 |
| [55] | Winskel, G.: Event structures, advances in Petri nets, part II. In: Proceedings of an Advanced Course, Bad Honnef, 1986, LNCS, vol. 255, pp. 325-392. Springer, Berlin (1987) · Zbl 0626.68022 |
| [56] | Winskel, G., Nielsen, M.: Models for concurrency. In: Handbook of Logic in Computer Science, vol. 4, pp. 1-148. Oxford University Press, Oxford (1995) |
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.
