Verification and enforcement of strong infinite- and \(k\)-step opacity using state recognizers
From MaRDI portal
Publication:2065174
DOI10.1016/j.automatica.2021.109838zbMath1480.93270OpenAlexW3194981700MaRDI QIDQ2065174
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
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
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