Abstract
In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finite-state) Petri nets, which can be used for verification purposes. Contextual nets are a generalisation of Petri nets suited to model systems with read-only access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan’s construction to a suitable encoding of the contextual net into an ordinary net. However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. A construction for generating such a contextual complete prefix has been proposed for a special class of nets, called read-persistent. In this paper, we propose an algorithm that works for arbitrary semi-weighted, bounded contextual nets. The construction explicitly takes into account the fact that, unlike in ordinary or read-persistent nets, an event can have several different histories in general contextual net computations.
Research partially supported by EU IST-2004-16004 SEnSOria, MIUR Project ART, DFG project SANDS and CRUI/DAAD Vigoni “Models based on Graph Transformation Systems: Analysis and Verification”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
The Mole unfolder, http://www.fmi.uni-stuttgart.de/szs/tools/mole
Baldan, P., Corradini, A., König, B.: Verifying finite-state graph grammars: an unfolding-based approach. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 83–98. Springer, Heidelberg (2004)
Baldan, P., Corradini, A., Montanari, U.: An event structure semantics for P/T contextual nets: asymmetric event structures. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 63–80. Springer, Heidelberg (1998)
Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures and processes. Information and Computation 171(1), 1–49 (2001)
Christensen, S., Hansen, N.D.: Coloured Petri nets extended with place capacities, test arcs and inhibitor arcs. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 186–205. Springer, Heidelberg (1993)
Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28, 575–591 (1991)
Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20, 285–310 (2002)
Janicki, R., Koutny, M.: Invariant semantics of nets with inhibitor arcs. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527. Springer, Heidelberg (1991)
Janicki, R., Koutny, M.: Semantics of inhibitor nets. Information and Computation 123, 1–16 (1995)
Langerak, R.: Transformation and Semantics for LOTOS. PhD thesis, Department of Computer Science, University of Twente (1992)
McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–174. Springer, Heidelberg (1993)
McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)
Montanari, U., Rossi, F.: Contextual occurrence nets and concurrent constraint programming. In: Ehrig, H., Schneider, H.-J. (eds.) Dagstuhl Seminar 1993. LNCS, vol. 776. Springer, Heidelberg (1994)
Montanari, U., Rossi, F.: Contextual nets. Acta Informatica 32(6), 545–596 (1995)
Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, event structures and domains, Part 1. Theoretical Computer Science 13, 85–108 (1981)
Pinna, G.M., Poigné, A.: On the nature of events: another perspective in concurrency. Theoretical Computer Science 138(2), 425–454 (1995)
Ristori, G.: Modelling Systems with Shared Resources via Petri Nets. PhD thesis, Department of Computer Science, University of Pisa (1994)
Vogler, W.: Efficiency of asynchronous systems and read arcs in Petri nets. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 538–548. Springer, Heidelberg (1997)
Vogler, W., Semenov, A., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 501–516. Springer, Heidelberg (1998)
Winkowski, J.: Reachability in contextual nets. Fundamenta Informaticae 51(1), 235–250 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Baldan, P., Corradini, A., König, B., Schwoon, S. (2008). McMillan’s Complete Prefix for Contextual Nets. In: Jensen, K., van der Aalst, W.M.P., Billington, J. (eds) Transactions on Petri Nets and Other Models of Concurrency I. Lecture Notes in Computer Science, vol 5100. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89287-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-89287-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89286-1
Online ISBN: 978-3-540-89287-8
eBook Packages: Computer ScienceComputer Science (R0)