Verifying weak and strong k-step opacity in discrete-event systems
From MaRDI portal
(Redirected from Publication:6165326)
Verifying weak and strong \(k\)-step opacity in discrete-event systems
Verifying weak and strong \(k\)-step opacity in discrete-event systems
Abstract: Opacity is an important system-theoretic property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has only limited observations of its behavior. Several notions of opacity have been discussed in the literature, including current-state opacity, k-step opacity, and infinite-step opacity. We investigate weak and strong k-step opacity, the notions that generalize both current-state opacity and infinite-step opacity, and ask whether the intruder is not able to decide, at any instant, when respectively whether the system was in a secret state during the last k observable steps. We design a new algorithm verifying weak k-step opacity, the complexity of which is lower than the complexity of existing algorithms and does not depend on the parameter k, and show how to use it to verify strong k-step opacity by reducing strong k-step opacity to weak k-step opacity. The complexity of the resulting algorithm is again better than the complexity of existing algorithms and does not depend on the parameter k.
Recommendations
- Verification and enforcement of strong infinite- and k-step opacity using state recognizers
- Strong current-state and initial-state opacity of discrete-event systems
- Comparing the notions of opacity for discrete-event systems
- Infinite-step opacity and K-step opacity of stochastic discrete-event systems
- Verification of K-step and infinite-step opacity of bounded labeled Petri nets
Cites work
- A general language-based framework for specifying and verifying notions of opacity
- A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- Comments on: ``A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- Comparing the notions of opacity for discrete-event systems
- Concurrent secrets
- Enforcement and validation (at runtime) of various notions of opacity
- Introduction to algorithms.
- Introduction to Discrete Event Systems
- Modelling opacity using Petri nets
- On a structural property in the state complexity of projected regular languages
- Opacity of discrete event systems and its applications
- Supervisory control of timed discrete-event systems
- Verification and enforcement of strong infinite- and k-step opacity using state recognizers
- Verification of Infinite-Step Opacity and Complexity Considerations
Cited in
(28)- Infinite-step opacity and K-step opacity of stochastic discrete-event systems
- Opacity of networked discrete event systems
- Comparing the notions of opacity for discrete-event systems
- Verification and enforcement of strong infinite- and k-step opacity using state recognizers
- Online verification of K-step opacity by Petri nets in centralized and decentralized structures
- Verification of K-step and infinite-step opacity of bounded labeled Petri nets
- Comments on: ``A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- A general language-based framework for specifying and verifying notions of opacity
- Strong current-state and initial-state opacity of discrete-event systems
- Verification of initial-state opacity in security applications of discrete event systems
- scientific article; zbMATH DE number 7155812 (Why is no real title available?)
- Verification of k-Step and Definite Critical Observability in Discrete-Event Systems
- Secure Your Intention: On Notions of Pre-Opacity in Discrete-Event Systems
- Secret inference and attacktability analysis of discrete event systems
- State-based opacity of labeled real-time automata
- Active opacity of discrete-event systems
- Matrix approach for verification of opacity of partially observed discrete event systems
- Identification of labeled Petri nets from finite automata
- State-based opacity of real-time automata
- Infinite- and K-step opacity verification of discrete-event systems under nondeterministic observations
- Optimal control strategy for k-level opaque systems based on the optimization method of multi-selection problems at each stage
- New insights into opacity verification in timed discrete-event systems
- Always guarding you: strong initial-and-final-state opacity of discrete-event systems
- Opacity of discrete event systems and its applications
- Verification and transformation for a trajectory-based weak K-step opacity
- Verification and enforcement of strong state-based opacity for discrete-event systems
- Enforcement and validation (at runtime) of various notions of opacity
This page was built for publication: Verifying weak and strong \(k\)-step opacity in discrete-event systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6165326)
