Abstract
This paper deals with the partial order techniques of Petri nets, based on persistent sets and step graphs. To take advantage of the strengths of each method, it proposes the persistent step sets as a parametric combination of the both methods. The persistent step sets method allows to fix, for each marking, the set of transitions to be covered by the selected steps and then to control their maximal length and number. Moreover, this persistent step selective search preserves, at least, deadlocks of Petri nets.
This paper also provides two practical computation procedures of the persistent step sets based on the strong-persistent sets [5, 10] and the persistent sets, respectively.
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
Notes
- 1.
Two firing sequences are equivalent w.r.t. some property, if they cannot be distinguished by the property.
- 2.
References
Barkaoui, K., Couvreur, J.-M., Klai, K.: On the equivalence between liveness and deadlock-freeness in Petri nets. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 90–107. Springer, Heidelberg (2005). https://doi.org/10.1007/11494744_7
Barkaoui, K., Pradat-Peyre, J.-F.: On liveness and controlled siphons in Petri nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 57–72. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61363-3_4
Chen, Y.F., Li, Z.W., Barkaoui, K.: New Petri net structure and its application to optimal supervisory control: Interval inhibitor arcs. IEEE Trans. Syst. Man Cybern. 44(10), 1384–1400 (2014)
Desel, J., Juhás, G.: “What is a Petri net?” Informal answers for the informed reader. In: Ehrig, H., Padberg, J., Juhás, G., Rozenberg, G. (eds.) Unifying Petri Nets. LNCS, vol. 2128, pp. 1–25. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45541-8_1
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60761-7
Junttila, T.: On the symmetry reduction method for Petri nets and similar formalisms. Ph.D. dissertation, Helsinki University of Technology, Espoo, Finland (2005)
Li, Z.W., Zhao, M.: On controllability of dependent siphons for deadlock prevention in generalized Petri nets. IEEE Trans. Syst. Man Cybern. 38(2), 369–384 (2008)
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_34
Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett. 63(5), 243–246 (1997)
Ribet, P.-O., çois, F., Berthomieu, B.: On combining the persistent sets method with the covering steps graph method. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 344–359. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36135-9_22
Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1(4), 297–322 (1992)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-65306-6_21
Valmari, A., Hansen, H.: Can stubborn sets be optimal? Fundam. Inform. 113(3–4), 377–397 (2011)
Vernadat, F., Azéma, P., Michel, F.: Covering step graph. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 516–535. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61363-3_28
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Barkaoui, K., Boucheneb, H., Li, Z. (2018). Exploiting Local Persistency for Reduced State Space Generation. In: Atig, M., Bensalem, S., Bliudze, S., Monsuez, B. (eds) Verification and Evaluation of Computer and Communication Systems. VECoS 2018. Lecture Notes in Computer Science(), vol 11181. Springer, Cham. https://doi.org/10.1007/978-3-030-00359-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-00359-3_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00358-6
Online ISBN: 978-3-030-00359-3
eBook Packages: Computer ScienceComputer Science (R0)