Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach

被引：38
|
作者：
Zhang, Kuize [1 ,2 ]
Yin, Xiang [3 ,4 ]
Zamani, Majid [5 ,6 ]
机构：
[1] KTH Royal Inst Technol, Sch Elect Engn, ACCESS Linnaeus Ctr, S-10044 Stockholm, Sweden
[2] Harbin Engn Univ, Coll Automat, Harbin 150001, Heilongjiang, Peoples R China
[3] Shanghai Jiao Tong Univ, Dept Automat, Shanghai 200240, Peoples R China
[4] Shanghai Jiao Tong Univ, Key Lab Syst Control & Informat Proc, Shanghai 200240, Peoples R China
[5] Univ Colorado, Comp Sci Dept, Boulder, CO 80309 USA
[6] Ludwig Maximilian Univ Munich, Dept Comp Sci, D-80539 Munich, Germany
来源：
IEEE TRANSACTIONS ON AUTOMATIC CONTROL | 2019年 / 64卷 / 12期
基金：
黑龙江省自然科学基金; 中国国家自然科学基金;
关键词：
(Bi)simulation relation; nondeterministic transition system; opacity; INFINITE-STEP; DISCRETE; VERIFICATION;
D O I：
10.1109/TAC.2019.2908726
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper, we propose several opacity-preserving (bi)simulation relations for nondeterministic transition systems (NTSs) in terms of initial-state opacity, current-state opacity, $K$-step opacity, and infinite-step opacity. We also show how one can leverage quotient constructions to compute such relations. As a result, although the opacity verification problem for infinite NTSs is generally undecidable, if one can find such an opacity-preserving relation from an infinite NTS to a finite one, the (lack of) opacity of the infinite NTS can be easily verified over the finite one, which is decidable.
引用
收藏
页码：5116 / 5123
页数：8
相关论文
共 50 条
  • [1] Infinite-step opacity of nondeterministic finite transition systems: A bisimulation relation approach
    Zhang, Kuize
    Zamani, Majid
    [J]. 2017 IEEE 56TH ANNUAL CONFERENCE ON DECISION AND CONTROL (CDC), 2017,
  • [2] Opacity of discrete-event systems under nondeterministic observation mechanism
    Zhang, Jiahui
    Chu, Qian
    Han, Xiaoguang
    Li, ZhiWu
    Chen, Zengqiang
    [J]. ASIAN JOURNAL OF CONTROL, 2023, 25 (02) : 1577 - 1590
  • [3] Detectability of Nondeterministic Finite Transition Systems
    Zhang, Kuize
    Zamani, Majid
    [J]. IFAC PAPERSONLINE, 2017, 50 (01): : 9272 - 9277
  • [4] Opacity generalised to transition systems
    Bryans, JW
    Koutny, M
    Mazaré, L
    Ryan, PYA
    [J]. FORMAL ASPECTS IN SECURITY AND TRUST, 2006, 3866 : 81 - 95
  • [5] Opacity generalised to transition systems
    Jeremy W. Bryans
    Maciej Koutny
    Laurent Mazaré
    Peter Y. A. Ryan
    [J]. International Journal of Information Security, 2008, 7 : 421 - 435
  • [6] Opacity generalised to transition systems
    Bryans, Jeremy W.
    Koutny, Maciej
    Mazare, Laurent
    Ryan, Peter Y. A.
    [J]. INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2008, 7 (06) : 421 - 435
  • [7] Fuzzy Bisimulations for Nondeterministic Fuzzy Transition Systems
    Qiao, Sha
    Zhu, Ping
    Feng, Jun-e
    [J]. IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2023, 31 (07) : 2450 - 2463
  • [8] SIMULATION OF ATOMIC TRANSITION ARRAYS FOR OPACITY CALCULATIONS
    BAUCHE, J
    BAUCHEARNOULT, C
    WYART, JF
    DUFFY, P
    KLAPISCH, M
    [J]. PHYSICAL REVIEW A, 1991, 44 (09): : 5707 - 5714
  • [9] A Metamodeling Approach for Uncertainty Analysis of Nondeterministic Systems
    Choi, Hae-Jin
    Allen, Janet K.
    [J]. JOURNAL OF MECHANICAL DESIGN, 2009, 131 (04) : 0410081 - 04100810
  • [10] Control of nondeterministic discrete event systems for simulation equivalence
    Zhou, Changyan
    Kumar, Ratnesh
    [J]. IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2007, 4 (03) : 340 - 349
12345