Abstract
Petri nets have been proposed as a fundamental model for discrete-event systems in a wide variety of applications and have been an asset to reduce the computational complexity involved in solving a series of problems, such as control, state estimation, fault diagnosis, etc. Many of those problems require an analysis of the reachability graph of the Petri net. The basis reachability graph is a condensed version of the reachability graph that was introduced to efficiently solve problems linked to partial observation. It was in particular used for diagnosis which consists in deciding whether some fault events occurred or not in the system, given partial observations on the run of the system. However this method is, with very specific exceptions, limited to bounded Petri nets. In this paper, we introduce the notion of basis coverability graph to remove this requirement. We then establish the relationship between the coverability graph and the basis coverability graph. Finally, we focus on the diagnosability problem: we show how the basis coverability graph can be used to get an efficient algorithm.
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
References
Bérard, B., Haar, S., Schmitz, S., Schwoon, S.: The complexity of diagnosability and opacity verification for Petri nets. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 200–220. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57861-3_13
Boucheneb, H., Barkaoui, K.: Reducing interleaving semantics redundancy in reachability analysis of time Petri nets. ACM Trans. Embed. Comput. Syst. 12(1), 7:1–7:24 (2013)
Cabasino, M.P., Giua, A., Lafortune, S., Seatzu, C.: A new approach for diagnosability analysis of Petri nets using verifier nets. IEEE Trans. Autom. Control 57(12), 3104–3117 (2012)
Cabasino, M.P., Giua, A., Seatzu, C.: Fault detection for discrete event systems using Petri nets with unobservable transitions. Automatica 46(9), 1531–1539 (2010)
Cabasino, M.P., Giua, A., Seatzu, C.: Introduction to Petri nets. In: Seatzu, C., Silva, M., van Schuppen, J. (eds.) Control of Discrete-Event Systems. LNCIS, vol. 433, pp. 191–211. Springer, London (2013). https://doi.org/10.1007/978-1-4471-4276-8_10
Cabasino, M.P., Giua, A., Pocci, M., Seatzu, C.: Discrete event diagnosis using labeled Petri nets. An application to manufacturing systems. Control Eng. Pract. 19(9), 989–1001 (2011)
Giua, A., Seatzu, C., Corona, D.: Marking estimation of Petri nets with silent transitions. IEEE Trans. Autom. Control 52(9), 1695–1699 (2007)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, vol. 1032. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60761-7
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Ma, Z.Y., Tong, Y., Li, Z.W., Giua, A.: Basis marking representation of Petri net reachability spaces and its application to the reachability problem. IEEE Trans. Autom. Control 62(3), 1078–1093 (2017)
Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, STOC 1981, pp. 238–246. ACM (1981)
Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)
Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part I. Theor. Comput. Sci. 13(1), 85–108 (1981). Special Issue Semantics of Concurrent Computation
Reynier, P.-A., Servais, F.: Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. Fundam. Informaticae 122(1–2), 1–30 (2013)
Lipton, R.: The reachability problem requires exponential space. Technical report, Yale University (1976)
Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40(9), 1555–1575 (1995)
Tong, Y., Li, Z., Seatzu, C., Giua, A.: Verification of state-based opacity using Petri nets. IEEE Trans. Autom. Control 62(6), 2823–2837 (2017)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Lefaucheux, E., Giua, A., Seatzu, C. (2018). Basis Coverability Graph for Partially Observable Petri Nets with Application to Diagnosability Analysis. In: Khomenko, V., Roux, O. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2018. Lecture Notes in Computer Science(), vol 10877. Springer, Cham. https://doi.org/10.1007/978-3-319-91268-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-91268-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91267-7
Online ISBN: 978-3-319-91268-4
eBook Packages: Computer ScienceComputer Science (R0)