Efficient unfolding of contextual Petri nets. (English) Zbl 1263.68117
A contextual net is a Petri net extended with read arcs, which allows transitions to check for tokens without consuming them. This way, concurrent read access can be modelled directly. It is known that unfoldings of a contextual net can be exponentially more compact than those of a corresponding Petri net. This paper contributes two methods for computing contextual unfoldings and studies their efficiency. Experiments on a number of benchmark examples show that contextual unfoldings are not only smaller than unfoldings of corresponding Petri nets but can also be computed with the same or better efficiency.
Reviewer: Jörg Desel (Hagen)
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | Esparza, J.; Heljanko, K., (Unfoldings — A Partial-Order Approach to Model Checking. Unfoldings — A Partial-Order Approach to Model Checking, EATCS Monographs in Theoretical Computer Science (2008), Springer) · Zbl 1153.68035 |
| [2] | K. Heljanko, Combining symbolic and partial-order methods for model-checking 1-safe Petri nets, Ph.D. Thesis, Helsinki University of Technology, 2002.; K. Heljanko, Combining symbolic and partial-order methods for model-checking 1-safe Petri nets, Ph.D. Thesis, Helsinki University of Technology, 2002. |
| [3] | W. Vogler, A.L. Semenov, A. Yakovlev, Unfolding and finite prefix for nets with read arcs, in: Proc. of CONCUR’98, in: LNCS, vol. 1466, 1998, pp. 501-516.; W. Vogler, A.L. Semenov, A. Yakovlev, Unfolding and finite prefix for nets with read arcs, in: Proc. of CONCUR’98, in: LNCS, vol. 1466, 1998, pp. 501-516. · Zbl 0940.68096 |
| [4] | G. Ristori, Modelling systems with shared resources via Petri nets, Ph.D. Thesis, Department of Computer Science, University of Pisa, 1994.; G. Ristori, Modelling systems with shared resources via Petri nets, Ph.D. Thesis, Department of Computer Science, University of Pisa, 1994. |
| [5] | Montanari, U.; Rossi, F., Contextual occurrence nets and concurrent constraint programming, (Dagstuhl Seminar 9301. Dagstuhl Seminar 9301, LNCS, vol. 776 (1994)), 280-295 · Zbl 1494.68183 |
| [6] | R. Janicki, M. Koutny, Invariant semantics of nets with inhibitor arcs, in: Proc. Concur, in: LNCS, vol. 527, 1991, pp. 317-331.; R. Janicki, M. Koutny, Invariant semantics of nets with inhibitor arcs, in: Proc. Concur, in: LNCS, vol. 527, 1991, pp. 317-331. |
| [7] | P. Baldan, A. Corradini, U. Montanari, An event structure semantics for P/T contextual nets: Asymmetric event structures, in: Proc. FoSSaCS, in: LNCS, vol. 1378, 1998, pp. 63-80.; P. Baldan, A. Corradini, U. Montanari, An event structure semantics for P/T contextual nets: Asymmetric event structures, in: Proc. FoSSaCS, in: LNCS, vol. 1378, 1998, pp. 63-80. · Zbl 0902.68140 |
| [8] | Winkowski, J., Reachability in contextual nets, Fundamenta Informaticae, 51, 1-2, 235-250 (2002) · Zbl 1003.68106 |
| [9] | Baldan, P.; Corradini, A.; König, B.; Schwoon, S., McMillan’s complete prefix for contextual nets, (ToPNoC 1. ToPNoC 1, LNCS, vol. 5100 (2008)), 199-220 · Zbl 1171.68560 |
| [10] | Esparza, J.; Römer, S.; Vogler, W., An improvement of McMillan’s unfolding algorithm, Formal Methods in System Design, 20, 285-310 (2002) · Zbl 1017.68085 |
| [11] | C. Rodríguez, Cunf, http://www.lsv.ens-cachan.fr/ rodriguez/tools/cunf/; C. Rodríguez, Cunf, http://www.lsv.ens-cachan.fr/ rodriguez/tools/cunf/ |
| [12] | S. Schwoon, Mole, http://www.lsv.ens-cachan.fr/ schwoon/tools/mole/; S. Schwoon, Mole, http://www.lsv.ens-cachan.fr/ schwoon/tools/mole/ |
| [13] | P. Baldan, A. Bruni, A. Corradini, B. König, S. Schwoon, On the computation of McMillan’s prefix for contextual nets and graph grammars, in: Proc. ICGT’10, in: LNCS, vol. 6372, 2010, pp. 91-106.; P. Baldan, A. Bruni, A. Corradini, B. König, S. Schwoon, On the computation of McMillan’s prefix for contextual nets and graph grammars, in: Proc. ICGT’10, in: LNCS, vol. 6372, 2010, pp. 91-106. · Zbl 1306.68120 |
| [14] | C. Rodríguez, S. Schwoon, P. Baldan, Efficient contextual unfolding, in: Proc. Concur, in: LNCS, vol. 6901, 2011, pp. 342-357.; C. Rodríguez, S. Schwoon, P. Baldan, Efficient contextual unfolding, in: Proc. Concur, in: LNCS, vol. 6901, 2011, pp. 342-357. · Zbl 1343.68176 |
| [15] | C. Rodríguez, S. Schwoon, P. Baldan, Efficient contextual unfolding, Tech. Rep. LSV-11-14, LSV, ENS de Cachan, 2011.; C. Rodríguez, S. Schwoon, P. Baldan, Efficient contextual unfolding, Tech. Rep. LSV-11-14, LSV, ENS de Cachan, 2011. · Zbl 1343.68176 |
| [16] | Janicki, R.; Koutny, M., Semantics of inhibitor nets, Information and Computation, 123, 1-16 (1995) · Zbl 1096.68678 |
| [17] | K.L. McMillan, Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, in: Proc. CAV, in: LNCS, vol. 663, 1992, pp. 164-177.; K.L. McMillan, Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, in: Proc. CAV, in: LNCS, vol. 663, 1992, pp. 164-177. |
| [18] | V. Khomenko, Model checking based on prefixes of Petri net unfoldings, Ph.D. Thesis, School of Computing Science, Newcastle University, 2003.; V. Khomenko, Model checking based on prefixes of Petri net unfoldings, Ph.D. Thesis, School of Computing Science, Newcastle University, 2003. · Zbl 1072.68072 |
| [19] | V. Khomenko, Punf, http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/punf/; V. Khomenko, Punf, http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/punf/ |
| [20] | K. Heljanko, Deadlock and reachability checking with finite complete prefixes, Licentiate’s Thesis, Helsinki University of Technology, 1999.; K. Heljanko, Deadlock and reachability checking with finite complete prefixes, Licentiate’s Thesis, Helsinki University of Technology, 1999. |
| [21] | C. Rodríguez, Implementation of a complete prefix unfolder for contextual nets, Rapport de master, Master Parisien de Recherche en Informatique, Paris, France, Sep. 2010.; C. Rodríguez, Implementation of a complete prefix unfolder for contextual nets, Rapport de master, Master Parisien de Recherche en Informatique, Paris, France, Sep. 2010. |
| [22] | Heljanko, K., Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets, Fundamenta Informaticae, 37, 3, 247-268 (1999) · Zbl 0930.68096 |
| [23] | C. Schröter, Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen, Ph.D. Thesis, Universität Stuttgart, 2006.; C. Schröter, Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen, Ph.D. Thesis, Universität Stuttgart, 2006. |
| [24] | Codish, M.; Genaim, S.; Stuckey, P. J., A declarative encoding of telecommunications feature subscription in SAT, (PPDP (2009)), 255-266 |
| [25] | J. Esparza, K. Heljanko, Implementing LTL model checking with net unfoldings, in: Proc. SPIN, in: LNCS, vol. 2057, 2001, pp. 37-56.; J. Esparza, K. Heljanko, Implementing LTL model checking with net unfoldings, in: Proc. SPIN, in: LNCS, vol. 2057, 2001, pp. 37-56. · Zbl 0985.68520 |
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.
