Verification and enforcement of strong infinite- and \(k\)-step opacity using state recognizers

DOI10.1016/j.automatica.2021.109838zbMath1480.93270OpenAlexW3194981700MaRDI QIDQ2065174

Xiang Yin, Ziyue Ma, Zhiwu Li

Publication date: 7 January 2022

Published in: Automatica (Search for Journal in Brave)

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

zbMATH Keywords

discrete event systeminfinite-step opacity\(k\)-step opacitystate recognizer

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Discrete event control/observation systems (93C65)

Related Items (4)

Enforcement for infinite-step opacity and K-step opacity via insertion mechanism ⋮ Strong current-state and initial-state opacity of discrete-event systems ⋮ Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques ⋮ Verifying weak and strong \(k\)-step opacity in discrete-event systems

Uses Software

• UMDES

Cites Work

• Comparative analysis of related notions of opacity in centralized and coordinated architectures
• Synthesis of insertion functions for enforcement of opacity security properties
• Opacity of discrete event systems and its applications
• Enforcement and validation (at runtime) of various notions of opacity
• Current-state opacity enforcement in discrete event systems under incomparable observations
• Enforcement of opacity by public and private insertion functions
• A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
• Centralized and distributed algorithms for on-line synthesis of maximal control policies under partial observation
• A Uniform Approach for Synthesizing Property-Enforcing Supervisors for Partially-Observed Discrete-Event Systems
• Introduction to Discrete Event Systems
• Decentralized Prognosis of Failures in Discrete Event Systems
• Synthesis of Maximally Permissive Supervisors for Nondeterministic Discrete Event Systems With Nondeterministic Specifications
• Synthesis of Dynamic Masks for Infinite-Step Opacity
• Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement
• Opacity Enforcement Using Nondeterministic Publicly Known Edit Functions
• Basis Marking Representation of Petri Net Reachability Spaces and Its Application to the Reachability Problem
• Verification of State-Based Opacity Using Petri Nets
• Opacity-Enforcing Supervisory Strategies via State Estimator Constructions
• Design of Supervisors for Active Diagnosis in Discrete Event Systems

This page was built for publication: Verification and enforcement of strong infinite- and \(k\)-step opacity using state recognizers