The Complexity of Diagnosability and Opacity Verification for Petri Nets

• Autorzy: Bérard B. , Haar S. , Schmitz S. , Schwoon S.

Identyfikatory

DOI

10.3233/FI-2018-1706

• Konferencja: International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Petri Nets 2017) (31; School of Engineering and Architecture of Zaragoza University; 25.30.07.2017; Spain)
• Języki publikacji: EN

Abstrakty

EN

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 NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and 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 ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.

Słowa kluczowe

EN

diagnosability; opacity; verification; complexity; Petri nets

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 161, nr 4
• Strony: 317--349
• Opis fizyczny: Bibliogr. 35 poz., rys., tab.

Twórcy

autor

Bérard B.

• Sorbonne Universités, UPMC Univ. Paris 06, LIP6, CNRS, Paris, France

autor

Haar S.

• INRIA and LSV, ENS Paris-Saclay and CNRS, Université Paris-Saclay, France

autor

Schmitz S.

• LSV, ENS Paris-Saclay and CNRS, Université Paris-Saclay, France

autor

Schwoon S.

• LSV, ENS Paris-Saclay and CNRS, Université Paris-Saclay, and INRIA, France

Bibliografia

• [1] Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D. Diagnosability of discrete-event systems. IEEE Transactions on Automatic Control, 1995. 40(9):1555-1575. doi:10.1109/9.412626.
• [2] Jiang S, Huang Z, Chandra V, Kumar R. A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Transactions on Automatic Control, 2001. 46(8):1318-1321. doi:10.1109/9.940942.
• [3] Yoo TS, Lafortune S. Polynomial-time verification of diagnosability of partially observed discrete event systems. IEEE Transactions on Automatic Control, 2002. 47(9):1491-1495. doi:10.1109/TAC.2002.802763.
• [4] Germanos V, Haar S, Khomenko V, Schwoon S. Diagnosability under weak fairness. ACM Transactions on Embedded Computer Systems, 2015. 14(4:69). doi:10.1145/2832910.
• [5] Haar S. Qualitative diagnosability of labeled Petri nets revisited. In: Proceedings of CDC’09 and CCC’09. IEEE, 2009 pp. 1248-1253. doi:10.1109/CDC.2009.5400917.
• [6] Haar S. Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Transactions on Automatic Control, 2010. 55(10):2310-2320. doi:10.1109/TAC.2010.2063490.
• [7] Haar S. What topology tells us about diagnosability in partial order semantics. Discrete Event Dynamic Systems, 2012. 22(4):383-402. doi:10.1007/s10626-011-0121-z.
• [8] Haar S, Rodríguez C, Schwoon S. Reveal your faults: it’s only fair! In: Proceedings of ACSD’13. IEEE, 2013 pp. 120-129. doi:10.1109/ACSD.2013.15.
• [9] Vogler W. Fairness and partial order semantics. Information Processing Letters, 1995. 55(1):33-39. doi:10.1016/0020-0190(95)00049-I.
• [10] Jančar P. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science, 1990. 74(1):71-93. doi:10.1016/0304-3975(90)90006-4.
• [11] Bryans J, Koutny M, Mazaré L, Ryan PYA. Opacity generalised to transition systems. International Journal of Information Security, 2008. 7(6):421-435. doi:10.1007/s10207-008-0058-x.
• [12] Cassez F, Dubreil J, Marchand H. Dynamic observers for the synthesis of opaque systems. In: Proceedings of ATVA’09, volume 5799 of Lecture Notes in Computer Science. Springer, 2009 pp. 352-367. doi:10.1007/978-3-642-04761-9_26.
• [13] Tong Y, Li Z, Seatzu C, Giua A. Verification of initial-state opacity in Petri nets. In: Proceedings of CDC’15. IEEE, 2015 pp. 344-349. doi:10.1109/CDC.2015.7402224.
• [14] Badouel E, Bednarczyk MA, Borzyszkowski AM, Caillaud B, Darondeau P. Concurrent secrets. Discrete Event Dynamic Systems, 2007. 17(4):425-446. doi:10.1007/s10626-007-0020-5.
• [15] Lin F. Opacity of discrete event systems and its applications. Automatica, 2011. 47(3):496-503. doi:10.1016/j.automatica.2011.01.002.
• [16] Busi N, Gorrieri R. Structural non-interference in elementary and trace nets. Mathematical Structures in Computer Science, 2009. 19(6):1065-1090. doi:10.1017/S0960129509990120.
• [17] Best E, Darondeau P, Gorrieri R. On the decidability of non interference over unbounded Petri nets. In: Proceedings of SecCo’10, volume 51 of Electronic Proceedings in Theoretical Computer Science. 2010 pp. 16-33. doi:10.4204/EPTCS.51.2.
• [18] Howell RR, Rosier LE, Yen HC. A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science, 1991. 82(2):341-372. doi:10.1016/0304-3975(91)90228-T.
• [19] Esparza J. Decidability and complexity of Petri net problems—an introduction. In: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science. Springer, 1996 pp. 374-428. doi:10.1007/3-540-65306-6_20.
• [20] Mayer AJ, Stockmeyer LJ. The complexity of word problems—this time with interleaving. Information and Computation, 1994. 115(2):293-311. doi:10.1006/inco.1994.1098.
• [21] Cabasino MP, Giua A, Lafortune S, Seatzu C. A new approach for diagnosability analysis of Petri nets using verifier nets. IEEE Transactions on Automatic Control, 2012. 57(12):3104-3117. doi:10.1109/TAC.2012.2200372.
• [22] Schmitz S. Automata column: The complexity of reachability in vector addition systems. ACM SIGLOG News, 2016. 3(1):3-21. doi:10.1145/2893582.2893585.
• [23] Lipton R. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976.
• [24] Leroux J, Schmitz S. Demystifying reachability in vector addition systems. In: Proceedings of LICS’15. IEEE, 2015 pp. 56-67. doi:10.1109/LICS.2015.16.
• [25] Bérard B, Haar S, Schmitz S, Schwoon S. The complexity of diagnosability and opacity verification for Petri nets. In: Proceedings of PN 2017, volume 10258 of Lecture Notes in Computer Science. Springer, 2017 pp. 200-220. doi:10.1007/978-3-319-57861-3_13.
• [26] Madalinski A, Khomenko V. Diagnosability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Proceedings of SysTol’10. IEEE, 2010 pp. 398-403.
• [27] Even S. On information lossless automata of finite order. IEEE Transactions on Electronic Computers, 1965. EC-14(4):561-569. doi:10.1109/PGEC.1965.263996.
• [28] Vardi MY, Wolper P. An automata-theoretic approach to automatic program verification. In: Proceedings of LICS 1986. IEEE, 1986 pp. 332-344.
• [29] Jones ND, Landweber LH, Lien YE. Complexity of some problems in Petri nets. Theoretical Computer Science, 1977. 4(3):277-299. doi:10.1016/0304-3975(77)90014-7.
• [30] Tong Y, Li Z, Seatzu C, Giua A. Decidability of opacity verification problems in labeled Petri net systems. Automatica, 2017. 80:48-53. doi:10.1016/j.automatica.2017.01.013.
• [31] Jančar P. Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theoretical Computer Science, 2001. 256(1-2):23-30. doi:10.1016/S0304-3975(00)00100-6.
• [32] Pelz E. Closure properties of deterministic Petri nets. In: Proceedings of STACS’87, volume 247 of Lecture Notes in Computer Science. Springer, 1987 pp. 371-382. doi:10.1007/BFb0039620.
• [33] Habermehl P. On the complexity of the linear-time µ-calculus for Petri nets. In: Proceedings of PN’97, volume 1248 of Lecture Notes in Computer Science. Springer, 1997 pp. 102-116. doi:10.1007/3-540-63139-9_32.
• [34] Yin X, Lafortune S. On the decidability and complexity of diagnosability for labeled Petri nets. IEEE Transactions on Automatic Control, 2017. 62(11):5931-5938. doi:10.1109/TAC.2017.2699278.
• [35] Atig MF, Habermehl P. On Yen’s path logic for Petri nets. International Journal of Foundations of Computer Science, 2011. 22(4):783-799. doi:10.1142/S0129054111008428.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).