Skip to main content
SpringerLink
Log in

The Complexity of Diagnosability and Opacity Verification for Petri Nets

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10258))

Abstract

Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues.

We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions.

Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is \(\mathsf {NL}\)-complete for finite state systems, \(\mathsf {PSPACE}\)-complete for safe Petri nets (even with fairness), and \(\mathsf {EXPSPACE}\)-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is \(\mathsf {ESPACE}\)-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In Jančar’s definition, (WF.2) uses the simpler condition \({\varvec{m}}_{i-1}(p)<w(p,t)\). We could easily adapt our treatment of weak fairness to work with that definition, but we preferred to remain compatible with [7, 11].

References

  1. Badouel, E., Bednarczyk, M.A., Borzyszkowski, A.M., Caillaud, B., Darondeau, P.: Concurrent secrets. Discrete Event Dyn. Syst. 17(4), 425–446 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bryans, J., Koutny, M., Mazaré, L., Ryan, P.Y.A.: Opacity generalised to transition systems. Int. J. Inf. Secur. 7(6), 421–435 (2008)

    Article  Google Scholar 

  3. 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)

    Article  MathSciNet  Google Scholar 

  4. Cassez, F., Dubreil, J., Marchand, H.: Dynamic observers for the synthesis of opaque systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 352–367. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_26

    Chapter  Google Scholar 

  5. Esparza, J.: Decidability and complexity of Petri net problems — an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998). doi:10.1007/3-540-65306-6_20

    Chapter  Google Scholar 

  6. Even, S.: On information lossless automata of finite order. IEEE Trans. Elec. Comput. EC-14(4), 561–569 (1965)

    Google Scholar 

  7. Germanos, V., Haar, S., Khomenko, V., Schwoon, S.: Diagnosability under weak fairness. ACM Trans. Embed. Comput. Syst. 14(4:69), 132–141 (2015)

    Google Scholar 

  8. Haar, S.: Qualitative diagnosability of labeled Petri nets revisited. In: Proceedings of CDC 2009 and CCC 2009, pp. 1248–1253. IEEE (2009)

    Google Scholar 

  9. Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Trans. Autom. Control 55(10), 2310–2320 (2010)

    Article  MathSciNet  Google Scholar 

  10. Haar, S.: What topology tells us about diagnosability in partial order semantics. Discrete Event Dyn. Syst. 22(4), 383–402 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  11. Haar, S., Rodríguez, C., Schwoon, S.: Reveal your faults: it’s only fair! In: Proceedings of ACSD 2013, pp. 120–129. IEEE (2013)

    Google Scholar 

  12. Habermehl, P.: On the complexity of the linear-time \(\mu \)-calculus for Petri Nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997). doi:10.1007/3-540-63139-9_32

    Chapter  Google Scholar 

  13. Howell, R.R., Rosier, L.E., Yen, H.C.: A taxonomy of fairness and temporal logic problems for Petri nets. Theor. Comput. Sci. 82(2), 341–372 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  14. Jančar, P.: Decidability of a temporal logic problem for Petri nets. Theor. Comput. Sci. 74(1), 71–93 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  15. Jančar, P.: Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theor. Comput. Sci. 256(1–2), 23–30 (2001)

    MathSciNet  MATH  Google Scholar 

  16. Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Trans. Autom. Control 46(8), 1318–1321 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  17. Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in Petri nets. Theor. Comput. Sci. 4(3), 277–299 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  18. Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Proceedings of LICS 2015, pp. 56–67. IEEE (2015)

    Google Scholar 

  19. Lin, F.: Opacity of discrete event systems and its applications. Automatica 47(3), 496–503 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  20. Lipton, R.: The reachability problem requires exponential space. Technical report 62. Yale University (1976)

    Google Scholar 

  21. Madalinski, A., Khomenko, V.: Diagnosability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Proceedings of SysTol 2010, pp. 398–403. IEEE (2010)

    Google Scholar 

  22. Mayer, A.J., Stockmeyer, L.J.: The complexity of word problems–this time with interleaving. Inf. Comput. 115(2), 293–311 (1994)

    Article  MathSciNet  Google Scholar 

  23. Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40(9), 1555–1575 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  24. Schmitz, S.: Automata column: the complexity of reachability in vector addition systems. ACM SIGLOG News 3(1), 3–21 (2016)

    Google Scholar 

  25. Tong, Y., Li, Z., Seatzu, C., Giua, A.: Verification of initial-state opacity in Petri nets. In: Proceedings of CDC 2015, pp. 344–349. IEEE (2015)

    Google Scholar 

  26. Vogler, W.: Fairness and partial order semantics. Inf. Process. Lett. 55(1), 33–39 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  27. Yoo, T.S., Lafortune, S.: Polynomial-time verification of diagnosability of partially observed discrete event systems. IEEE Trans. Autom. Control 47(9), 1491–1495 (2002)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Sorbonne Universités, UPMC University Paris 06, LIP6, Paris, France

    Béatrice Bérard

  2. INRIA and LSV, CNRS and ENS Cachan, Université Paris-Saclay, Cachan, France

    Béatrice Bérard, Stefan Haar, Sylvain Schmitz & Stefan Schwoon

Authors
  1. Béatrice Bérard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Haar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sylvain Schmitz
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Stefan Schwoon
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvain Schmitz .

Editor information

Editors and Affiliations

  1. Department of Mathematics and Computer Science (MF 7.103), Eindhoven University of Technology, Eindhoven, Noord-Brabant, The Netherlands

    Wil van der Aalst

  2. Carl von Ossietzky Universität Oldenburg, Oldenburg, Germany

    Eike Best

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bérard, B., Haar, S., Schmitz, S., Schwoon, S. (2017). The Complexity of Diagnosability and Opacity Verification for Petri Nets. In: van der Aalst, W., Best, E. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2017. Lecture Notes in Computer Science(), vol 10258. Springer, Cham. https://doi.org/10.1007/978-3-319-57861-3_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57861-3_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57860-6

  • Online ISBN: 978-3-319-57861-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation