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 条
[1]   Multilevel transitive and intransitive non-interference, causally [J].
Baldan, Paolo ;
Beggiato, Alessandro .
THEORETICAL COMPUTER SCIENCE, 2018, 706 :54-82
[2]   An algebraic characterization of language-based opacity in labeled Petri nets [J].
Basile, F. ;
De Tommasi, G. .
IFAC PAPERSONLINE, 2018, 51 (07) :329-336
[3]   On K-diagnosability of Petri nets via integer linear programming [J].
Basile, F. ;
Chiacchio, P. ;
De Tommasi, G. .
AUTOMATICA, 2012, 48 (09) :2047-2058
[4]   An optimization-based approach to assess non-interference in labeled and bounded Petri net systems [J].
Basile, Francesco ;
Boccia, Maurizio ;
De Tommasi, Gianmaria ;
Motta, Carlo ;
Sterle, Claudio .
NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2022, 44
[5]   Noninterference Enforcement via Supervisory Control in Bounded Petri Nets [J].
Basile, Francesco ;
De Tommasi, Gianmaria ;
Sterle, Claudio .
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2021, 66 (08) :3653-3666
[6]  
Basile F, 2018, IEEE INT C EMERG, P441, DOI 10.1109/ETFA.2018.8502532
[7]  
Berthomieu B, 2004, INT J PROD RES, V42, P2741, DOI [10.1080/00207540412331312688, 10.1080/00207540410001705257]
[8]  
BOURJIJ A, 1997, 1997 IEEE INT C SYST, V3, P2228
[9]   A survey on non-interference with Petri nets [J].
Busi, N ;
Gorrieri, R .
LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 :328-344
[10]  
Cabasino M.P., 2013, CONTROL DISCRETEEVEN, V433, P213, DOI DOI 10.1007/978-1-4471-4276-8
1234