Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques

被引：12

作者：

Basile, Francesco ^{[1
]}

De Tommasi, Gianmaria ^{[2
]}

Motta, Carlo ^{[2
]}

机构：

[1] Univ Salerno, DIEM, I-84084 Fisciano, Italy

[2] Univ Napoli Federico II, DIETI, I-80125 Naples, Italy

来源：

AUTOMATICA | 2023年 / 152卷

关键词：

Opacity; Labeled Petri nets; DES; Integer linear programming; NONINTERFERENCE; DIAGNOSABILITY; VERIFICATION;

D O I：

10.1016/j.automatica.2023.110911

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Opacity is a property of discrete event systems (DES) that is related to the possibility of hiding a secret to external observers, the so called intruders. If the secret is the system initial state, then the related opacity problem is referred to as Initial State Opacity (ISO). This paper gives a necessary and sufficient condition to check ISO in DES modeled as bounded and live labeled Petri nets (PNs). The proposed approach relies on both the algebraic representation of labeled PNs dynamic, and on their structural representation in terms of minimal support T-invariants. The proposed necessary and sufficient condition enables ISO assessment by means of the solution of Integer Linear Programming problems, which can be efficiently solved nowadays by means of off-the-shelf optimization tools.(c) 2023 Elsevier Ltd. All rights reserved.

引用

页数：9

共 34 条

[21] Overview of discrete event systems opacity: Models, validation, and quantification [J].

Jacob, Romain ;

Lesage, Jean-Jacques ;

Faure, Jean-Marc .

ANNUAL REVIEWS IN CONTROL, 2016, 41 :135-146

[22] On the history of diagnosability and opacity in discrete event systems [J].

Lafortune, Stephane ;

Lin, Feng ;

Hadjicostis, Christoforos N. .

ANNUAL REVIEWS IN CONTROL, 2018, 45 :257-266

[23] Verification of Infinite-step Opacity Using Labeled Petri Nets [J].

Lan, Hao ;

Tong, Yin ;

Seatzu, Carla .

IFAC PAPERSONLINE, 2020, 53 (02) :1729-1734

[24]

Lofberg J., 2004, 2004 IEEE INT C ROBO, P284, DOI [DOI 10.1109/CACSD.2004.1393890, 10.1109/CACSD.2004.1393890]

[25] Verification and enforcement of strong infinite- and k-step opacity using state recognizers [J].

Ma, Ziyue ;

Yin, Xiang ;

Li, Zhiwu .

AUTOMATICA, 2021, 133

[26] PETRI NETS - PROPERTIES, ANALYSIS AND APPLICATIONS [J].

MURATA, T .

PROCEEDINGS OF THE IEEE, 1989, 77 (04) :541-580

[27] Current-state opacity modelling and verification in partially observed Petri nets [J].

Saadaoui, Ikram ;

Li, Zhiwu ;

Wu, Naiqi .

AUTOMATICA, 2020, 116

[28]

Saboori A., 2009, IFAC Proc., V42, P46, DOI 10.3182/20090610-3-IT-4004.00013

[29]

Silva M., 1998, Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, P309

[30]

Teruel E., 1993, Applications and Theory of Petri Nets 1993. 14th International Conference Proceedings, P415

← 1 2 3 4 →