A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers

DOI10.1016/j.automatica.2017.02.037zbMath1370.93174MaRDI QIDQ2407182

Xiang Yin, Stéphane Lafortune

Publication date: 28 September 2017

Published in: Automatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.automatica.2017.02.037

zbMATH Keywords

discrete event systems; \(K\)-step opacity; infinite-step opacity; two-way observer

Mathematics Subject Classification ID

93C65: Discrete event control/observation systems

94A62: Authentication, digital signatures and secret sharing

Related Items

Relative predictability of failure event occurrences and its opacity-based test algorithm, \(k\)-memory-embedded insertion mechanism for opacity enforcement, Infinite-step opacity and \(K\)-step opacity of stochastic discrete-event systems, Enforcement of opacity by public and private insertion functions, Opacity of networked discrete event systems, Verification of approximate opacity for switched systems: a compositional approach, Comparing the notions of opacity for discrete-event systems, Verification and enforcement of strong infinite- and \(k\)-step opacity using state recognizers, Enforcement for infinite-step opacity and K-step opacity via insertion mechanism, Verification of \(K\)-step and infinite-step opacity of bounded labeled Petri nets, A framework for current-state opacity under dynamic information release mechanism, Comments on: ``A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers, Authors' reply to ``Comments on: ``A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers'', An improved approach for verifying delayed detectability of discrete-event systems, Initial-state detectability and initial-state opacity of unambiguous weighted automata

Uses Software

• UMDES

Cites Work

• Comparative analysis of related notions of opacity in centralized and coordinated architectures
• Synthesis of opaque systems with static and dynamic masks
• Probabilistic opacity for Markov decision processes
• Synthesis of insertion functions for enforcement of opacity security properties
• Verification of initial-state opacity in security applications of discrete event systems
• Opacity of discrete event systems and its applications
• Enforcing opacity of regular predicates on modal transition systems
• Verification of opacity and diagnosability for pushdown systems
• Concurrent secrets
• A Uniform Approach for Synthesizing Property-Enforcing Supervisors for Partially-Observed Discrete-Event Systems
• Current-State Opacity Formulations in Probabilistic Finite Automata
• Introduction to Discrete Event Systems
• Supervisory Control for Opacity
• Opacity-Enforcing Supervisory Strategies via State Estimator Constructions
• Verification of Infinite-Step Opacity and Complexity Considerations
• Unnamed Item
• Unnamed Item