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

DOI10.1109/TAC.2019.2908726MaRDI QIDQ5211280zbMATH OpenOpenAlexWikidataFDO

Authors Kuize Zhang, Xiang Yin, Majid Zamani

Publication date 28 January 2020

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1802.03321

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: In this paper, we propose several opacity-preserving (bi)simulation relations for general nondeterministic transition systems (NTS) in terms of initial-state opacity, current-state opacity, K-step opacity, and infinite-step opacity. We also show how one can leverage quotient construction to compute such relations. In addition, we use a two-way observer method to verify opacity of nondeterministic finite transition systems (NFTSs). As a result, although the verification of opacity for infinite NTSs is generally undecidable, if one can find such an opacity-preserving relation from an infinite NTS to an NFTS, the (lack of) opacity of the NTS can be easily verified over the NFTS which is decidable.

Cited in

(12)

• Enforcing opacity by insertion functions under multiple energy constraints
• Matrix approach for verification of opacity of partially observed discrete event systems
• Security and privacy with opacity-based state observation for finite state machine
• Enforcement for infinite-step opacity and K-step opacity via insertion mechanism
• Opacity of discrete-event systems under nondeterministic observation mechanism
• Strong current-state and initial-state opacity of discrete-event systems
• Authors' reply to ``Comments on: ``A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers'
• Non-interference assessment in colored net systems via integer linear programming
• Verification of approximate opacity for switched systems: a compositional approach
• Initial-state detectability and initial-state opacity of unambiguous weighted automata
• Enforcing current-state opacity through shuffle and deletions of event observations
• Compositional synthesis of opacity-preserving finite abstractions for interconnected systems

This page was built for publication: Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5211280)