Abstract
We integrate two compact data structures for representing state spaces of Petri nets: merged processes and contextual prefixes. The resulting data structure, called contextual merged processes (CMP), combines the advantages of the original ones and copes with several important sources of state space explosion: concurrency, sequences of choices, and concurrent read accesses to shared resources. In particular, we demonstrate on a number of benchmarks that CMPs are more compact than either of the original data structures. Moreover, we sketch a polynomial (in the CMP size) encoding into SAT of the model-checking problem for reachability properties.
This research was supported by the Epsrc grant EP/K001698/1 (Uncover).
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.
Similar content being viewed by others
References
Baldan, P., Bruni, A., Corradini, A., König, B., Rodríguez, C., Schwoon, S.: Efficient unfolding of contextual Petri nets. Theo. Comp. Sci. 449, 2–22 (2012)
Baldan, P., Corradini, A., König, B., Schwoon, S.: McMillan’s complete prefix for contextual nets. In: Jensen, K., van der Aalst, W.M.P., Billington, J. (eds.) ToPNoC I, LNCS, vol. 5100, pp. 199–220. Springer, Heidelberg (2008)
Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001)
Corbett, J.C.: Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering 22, 161–180 (1996)
Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)
Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20, 285–310 (2002)
Heljanko, K.: Deadlock and reachability checking with finite complete prefixes. Licentiate’s thesis, Helsinki University of Technology (1999)
Heljanko, K.: Minimizing finite complete prefixes. In: Proc. CS&P, pp. 83–95 (1999)
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, pp. 317–331. Springer, Heidelberg (1991)
Kahlon, V.: Boundedness vs. unboundedness of lock chains: Characterizing decidability of CFL-reachability for threads communicating via locks. In: Proc. LICS, pp. 27–36 (2009)
Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings. Ph.D. thesis, School of Computing Science, Newcastle University (2003)
Khomenko, V., Mokhov, A.: An algorithm for direct construction of complete merged processes. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol. 6709, pp. 89–108. Springer, Heidelberg (2011)
Khomenko, V.: Punf, http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/punf/
Khomenko, V., Kondratyev, A., Koutny, M., Vogler, W.: Merged processes – a new condensed representation of Petri net behaviour. Act. Inf. 43(5), 307–330 (2006)
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–177. Springer, Heidelberg (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, pp. 280–295. Springer, Heidelberg (1994)
Ranjan, D.P., Tang, D., Malik, S.: A comparative study of 2QBF algorithms. In: Proc. SAT (2004)
Ristori, G.: Modelling Systems with Shared Resources via Petri Nets. Ph.D. thesis, Department of Computer Science, University of Pisa (1994)
Rodríguez, C.: Cunf, http://www.lsv.ens-cachan.fr/~rodriguez/tools/cunf/
Rodríguez, C., Schwoon, S.: Verification of Petri Nets with Read Arcs. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 471–485. Springer, Heidelberg (2012)
Rodríguez, C., Schwoon, S., Baldan, P.: Efficient contextual unfolding. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 342–357. Springer, Heidelberg (2011)
Rodríguez, C., Schwoon, S., Khomenko, V.: Contextual merged processes. Tech. Rep. LSV-13-06, LSV, ENS de Cachan (2013)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rodríguez, C., Schwoon, S., Khomenko, V. (2013). Contextual Merged Processes. In: Colom, JM., Desel, J. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2013. Lecture Notes in Computer Science, vol 7927. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38697-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-38697-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38696-1
Online ISBN: 978-3-642-38697-8
eBook Packages: Computer ScienceComputer Science (R0)