Decidability of opacity verification problems in labeled Petri net systems

被引：50

作者：

Tong, Yin ^{[1
,3
]}

Li, Zhiwu ^{[1
,2
]}

Seatzu, Carla ^{[3
]}

Giua, Alessandro ^{[3
,4
]}

机构：

[1] Xidian Univ, Sch Electromech Engn, Xian 710071, Peoples R China

[2] Macau Univ Sci & Technol, Inst Syst Engn, Taipa, Macau, Peoples R China

[3] Univ Cagliari, Dept Elect & Elect Engn, I-09123 Cagliari, Italy

[4] Univ Toulon & Var, Aix Marseille Univ, CNRS, ENSAM,LSIS, Marseille, France

来源：

AUTOMATICA | 2017年 / 80卷

基金：

中国国家自然科学基金;

关键词：

Discrete event systems; Petri nets; Opacity; Decidability problems; DISCRETE-EVENT SYSTEMS; ENFORCEMENT; VALIDATION; NOTIONS;

D O I：

10.1016/j.automatica.2017.01.013

中图分类号：

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

学科分类号：

0812 ;

摘要：

A system is said to be opaque if an intruder that observes its evolution through a mask cannot infer that the system's evolution belongs to a given secret behavior. Opacity verification is the problem of determining whether the system is opaque with respect to a given secret or not. In this paper we address the decidability of the opacity verification problem. Using reduction approaches, we show that verification of initial-state, current-state, and language opacity is undecidable in labeled Petri nets. (C) 2017 Elsevier Ltd. All rights reserved.

引用

页码：48 / 53

页数：6

共 25 条

[1]

[Anonymous], 1981, Petri net theory and the modeling of systems

[2] Concurrent secrets [J].

Badouel, E. ;

Bednarczyk, M. ;

Borzyszkowski, A. ;

Caillaud, B. ;

Darondeau, P. .

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2007, 17 (04) :425-446

[3] Opacity generalised to transition systems [J].

Bryans, Jeremy W. ;

Koutny, Maciej ;

Mazare, Laurent ;

Ryan, Peter Y. A. .

INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2008, 7 (06) :421-435

[4] Modelling Opacity Using Petri Nets [J].

Bryans, Jeremy W. ;

Koutny, Maciej ;

Ryan, Peter Y. A. .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 121 :101-115

[5] Synthesis of opaque systems with static and dynamic masks [J].

Cassez, Franck ;

Dubreil, Jeremy ;

Marchand, Herve .

FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (01) :88-115

[6]

Cassez F, 2009, LECT NOTES COMPUT SC, V5576, P21, DOI 10.1007/978-3-642-02617-1_3

[7] Supervisory Control for Opacity [J].

Dubreil, Jeremy ;

Darondeau, Philippe ;

Marchand, Herve .

IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2010, 55 (05) :1089-1100

[8] Enforcement and validation (at runtime) of various notions of opacity [J].

Falcone, Ylies ;

Marchand, Herve .

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2015, 25 (04) :531-570

[9] 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

[10] Opacity of discrete event systems and its applications [J].

Lin, Feng .

AUTOMATICA, 2011, 47 (03) :496-503

← 1 2 3 →