Abstract
We define a safety slice as a subnet of a marked Petri net Σ that approximates Σ’s temporal behavior with respect to a set of interesting places Crit. This safety slice can be used to verify and falsify stutter-invariant linear-time safety properties when Crit is the set of places referred to by the safety property. By construction it is guaranteed that the safety slice’s state space is at most as big as that of the original net. Results on a benchmark set demonstrate effective reductions on several net instances. Therefore safety slicing as a net preprocessing step may achieve an acceleration for model checking stutter-invariant linear-time safety properties.
This work is partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems”.
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
Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008); 12, 112–120, 422–425
Berthelot, G.: Checking Properties of Nets Using Transformation. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222, pp. 19–40. Springer, Heidelberg (1986)
Brückner, I.: Slicing Integrated Formal Specifications for Verification. PhD thesis. University of Paderborn (March 2008)
Chang, C.K., Wang, H.: A slicing algorithm of concurrency modeling based on Petri nets. In: Hwang, K., Jacobs, S.M., Swartzlander, E.E. (eds.) Proc. of the 1986 Int. Conf. on Parallel Processing, pp. 789–792. IEEE Computer Society Press, Washington (1987)
Corbett, J.C.: Evaluating Deadlock Detection Methods for Concurrent Software. IEEE Transactions on Software Engineering 22(3), 161–180 (1996)
Lamport, L.: What Good is Temporal Logic? In: Information Processing 1983: Proceedings of the IFIO 9th World Computer Congress, pp. 657–668 (1983)
Llorens, M., Oliver, J., Silva, J., Tamarit, S., Vidal, G.: Dynamic Slicing Techniques for Petri Nets. In: Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008), Liverpool, UK. Electronic Notes in Theoretical Computer Science, vol. 223, pp. 153–165 (December 2008)
Peled, D., Wilke, T.: Stutter-Invariant Temporal Properties are Expressible Without the Next-time Operator. Information Processing Letters 63(5), 243–246 (1997)
Poitrenaud, D., Pradat-Peyre, J.-F.: Pre- and Post-agglomerations for LTL Model Checking. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 387–408. Springer, Heidelberg (2000)
PROD. Pr/T-net reachability analysis tool. Helsinki Univerity of Technology, http://www.tcs.hut.fi/Software/prod/
Rakow, A.: Slicing Petri nets with an Application to Workflow Verification. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds.) SOFSEM 2008. LNCS, vol. 4910, pp. 436–447. Springer, Heidelberg (2008)
Rakow, A.: Slicing Petri Nets. Technical Report, Carl von Ossietzky Universität Oldenburg, 20 pages (2007), http://parsys.informatik.uni-oldenburg.de/pubs/SlPN_tr.pdf
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Vasudevan, S., Emerson, E.A., Abraham, J.A.: Efficient model checking of hardware using conditioned slicing. In: Proc. of the 4th International Workshop on Automated Verification of Critical Systems, AVOCS 2004. Electronic Notes in Theoretical Computer Science, vol. 128(6), pp. 279–294. Elsevier Science Publishers (2004)
Vasudevan, S., Emerson, E.A., Abraham, J.A.: Improved Verification of Hardware Designs Through Antecedant Conditioned Slicing. International Journal of Software Tools and Technology Transfer (STTT) 9(1), 89–101 (2007)
Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Press, Piscataway (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rakow, A. (2012). Safety Slicing Petri Nets. In: Haddad, S., Pomello, L. (eds) Application and Theory of Petri Nets. PETRI NETS 2012. Lecture Notes in Computer Science, vol 7347. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31131-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-31131-4_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31130-7
Online ISBN: 978-3-642-31131-4
eBook Packages: Computer ScienceComputer Science (R0)