Verification of State-Based Opacity Using Petri Nets

No abstract is available for this paper.

• Publication year

  2017

• Venue

  IEEE Transactions on Automatic Control

• Publication date

  2017-06-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1109/TAC.2016.2620429
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Concurrency

  2021cited by this paper
• Basis Marking Representation of Petri Net Reachability Spaces and Its Application to the Reachability Problem

  2017cited by this paper
• On the Equivalence of Observation Structures for Petri Net Generators

  2016cited by this paper
• Verification of language-based opacity in Petri nets using verifier

  2016cited by this paper
• Overview of discrete event systems opacity: Models, validation, and quantification

  2016cited by this paper
• Decentralized Supervision of Petri Nets With a Coordinator

  2015cited by this paper
• Design of Optimal Petri Net Controllers for Disjunctive Generalized Mutual Exclusion Constraints

  2015cited by this paper
• Verification of current-state opacity using Petri nets

  2015cited by this paper
• Verification of initial-state opacity in Petri nets

  2015cited by this paper
• Diagnosability of Discrete-Event Systems Using Labeled Petri Nets

  2014cited by this paper
• Enforcement and validation (at runtime) of various notions of opacity

  2014cited by this paper
• Verification of initial-state opacity in security applications of discrete event systems

  2013influential reference
• Synthesis of opaque systems with static and dynamic masks

  2012cited by this paper
• Fault Diagnosis of Discrete-Event Systems Using Continuous Petri Nets

  2012cited by this paper
• Comparative analysis of related notions of opacity in centralized and coordinated architectures

  2012influential reference
• Discrete event diagnosis using labeled Petri nets. An application to manufacturing systems

  2011influential reference
• Dynamic Observers for the Synthesis of Opaque Systems

  2009cited by this paper
• The Dark Side of Timed Opacity

  2009cited by this paper
• Notions of security and opacity in discrete event systems

  2007cited by this paper
• Petri Net Supervisors for Disjunctive Constraints

  2007cited by this paper
• Marking Estimation of Petri Nets With Silent Transitions

  2007cited by this paper
• Modelling Opacity Using Petri Nets

  2005influential reference
• Fault detection for discrete event systems using Petri nets with unobservable transitions

  2005influential reference
• Opacity generalised to transition systems

  2005cited by this paper
• Using Unification For Opacity Properties

  2004cited by this paper
• Petri net supervisors for DES with uncontrollable and unobservable transitions

  2000cited by this paper
• Introduction to Discrete Event Systems

  1999cited by this paper
• Generalized mutual exclusion contraints on nets with uncontrollable transitions

  1992cited by this paper
• Petri nets: Properties, analysis and applications

  1989cited by this paper
• Theory of linear and integer programming

  1986cited by this paper

• Recent Advances in Fault Diagnosis and Opacity Analysis in Discrete Event Systems.

  2026cites this paper
• On clock interval automata for a class of time PNs

  2026cites this paper
• Opacity in Discrete Event Systems: A Perspective and Overview

  2026cites this paper
• New insights into opacity verification in timed discrete-event systems

  2026cites this paper
• Verification of current-state opacity and opaque time for labeled time Petri net systems

  2025cites this paper
• Decentralized Fault Diagnosis Using ILP and Labeled Petri Nets in Manufacturing Systems

  2025cites this paper
• New Insights into the Decidability of Opacity in Timed Automata

  2025cites this paper
• Opacity Verification for a Class of Modular Discrete Event Systems

  2025cites this paper
• Strong Current-State Opacity Verification of Discrete-Event Systems Modeled with Time Labeled Petri Nets

  2025cites this paper
• Language-based opacity in modular discrete event systems: Compositional secret-based verification using labeled petri nets

  2025cites this paper
• Decentralized State Estimation and Opacity Verification Based on Partially Ordered Observation Sequences

  2025cites this paper
• Obfuscation mechanism for simultaneous public event information release and private event information hiding in discrete event systems

  2025cites this paper
• Sequence-based Vs Observer-based Approaches to Verify Current-State Opacity: A Benchmark Case

  2025influential citation
• On Epistemic Properties in Discrete-Event Systems: A Uniform Framework and Its Applications

  2024cites this paper
• Supervisor synthesis for opacity enforcement in partially observed discrete event systems

  2024cites this paper
• Improved Local Partitioning Minimal-Siphon Enumeration Method

  2024cites this paper
• State estimation for constant-time labeled automata under dense time

  2024cites this paper
• Verification of Current-State Opacity in Time Labeled Petri Nets With Its Application to Smart Houses

  2024cites this paper
• Symbolic state estimation in bounded timed labeled Petri nets

  2024cites this paper
• On clock interval automata for a class of distributed timed DESs with time intervals

  2024cites this paper
• On Deadlock Analysis and Characterization of Labeled Petri Nets with Undistinguishable and Unobservable Transitions

  2024cites this paper
• Timed Opacity Verification for Switching Output Automata

  2024cites this paper
• State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets

  2024cites this paper
• An Optimization Approach to Current State Opacity Assessment

  2024cites this paper
• Observer Decomposition for Finite State Machines and its Application to Opacity

  2024cites this paper
• Verification of Archive System Opacity With Bounded Labeled Petri Nets

  2024cites this paper
• Security-by-Design of Smart Water Supply Systems: a Switching Output Automaton-based Approach

  2024cites this paper
• Liveness and deadlock-freeness verification and enforcement in bounded Petri nets using basis reachability graphs

  2024cites this paper
• Verification of Current-State Opacity in Discrete Event Systems by Using Basis Coverability Graphs

  2023influential citation
• Optimal Multi-Robot Path Planning for Cyclic Tasks using Petri Nets

  2023cites this paper
• Verification of Joint Current-State Opacity Using Petri Nets

  2023cites this paper
• Verification and Enforcement of (ϵ, ξ)-Differential Privacy over Finite Steps in Discrete Event Systems

  2023cites this paper
• A classification of cybersecurity strategies in the context of Discrete Event Systems

  2023cites this paper
• Security Quantification for Discrete Event Systems Based on the Worth of States

  2023cites this paper
• Adjacent initial states-based differential privacy for probabilistic labeled Petri nets

  2023cites this paper
• Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques

  2023cites this paper
• On tick automata for distributed timed DESs with synchronisations and minimal time constraints

  2023cites this paper
• State-Based Differential Privacy Verification and Enforcement for Probabilistic Automata

  2023cites this paper
• Detectability in Discrete Event Systems Using Unbounded Petri Nets

  2023cites this paper
• Optimal Secret Protection in Discrete Event Systems with Dynamic Clearance Levels

  2023cites this paper
• Verification of $k$-Step and Definite Critical Observability in Discrete-Event Systems

  2023cites this paper
• Opacity of Parametric Discrete Event Systems

  2023cites this paper
• Robust Diagnosability Analysis Using Basis Reachability Graph

  2023cites this paper
• Revisiting State Estimation and Weak Detectability of Discrete-Event Systems

  2023cites this paper
• Medical Cyber–Physical Systems: A Solution to Smart Health and the State of the Art

  2022cites this paper
• PNBA: A Software for Marking Estimation and Reconfiguration in Petri Nets Using Basis Marking Analysis

  2022cites this paper
• Diagnosis on a sliding window for partially observable Petri nets

  2022cites this paper
• Secure-by-Construction Synthesis of Cyber-Physical Systems

  2022cites this paper
• Enhancement of opacity for distributed state estimation in cyber-physical systems

  2022cites this paper
• An optimization-based approach to assess non-interference in labeled and bounded Petri net systems

  2022cites this paper
• Verifiers for the detection of timed patterns in discrete event systems

  2022cites this paper
• Opacity of discrete‐event systems under nondeterministic observation mechanism

  2022cites this paper
• Transformations between opacity for discrete-event systems

  2022cites this paper
• Reduced Complexity Verification of Almost-Infinite-Step Opacity in Stochastic Discrete-Event Systems*

  2022cites this paper
• Modular Verification of Opacity for Interconnected Control Systems via Barrier Certificates

  2022cites this paper
• Current-state opacity verification in discrete event systems using an observer net

  2022influential citation
• Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates

  2022cites this paper
• Fault diagnosis of PLC-based discrete event systems using Petri nets

  2022cites this paper
• Verification of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" id="d1e290" altimg="si6.svg"><mml:mi>K</mml:mi></mml:math>-step and infinite-step opacity of bounded labeled Petri nets

  2022cites this paper
• You Don't Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems

  2022cites this paper
• Online verification of K-step opacity by Petri nets in centralized and decentralized structures

  2022cites this paper
• Symbolic Verification of Current-State Opacity of Discrete Event Systems Using Petri Nets

  2022influential citation
• The Unfolding: Origins, Techniques, and Applications within Discrete Event Systems

  2022cites this paper
• Verification of Current-state Opacity for Discrete Event Systems Modeled With Unbounded Petri Nets

  2022influential citation
• Least-cost transition sequence estimation in labelled time Petri net systems with unobservable transitions

  2022cites this paper
• Optimistic Fault Diagnosis in Discrete Event Systems by Labeled Petri Nets and Basis Markings

  2022cites this paper
• Language-based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets

  2022cites this paper
• Verification of Strong K-Step Opacity for Discrete-Event Systems

  2022cites this paper
• Enforcement for infinite-step opacity and K-step opacity via insertion mechanism

  2022cites this paper
• Marking Predictability and Prediction in Labeled Petri Nets

  2021influential citation
• Current-state opacity and initial-state opacity of modular discrete event systems

  2021cites this paper
• Robust Diagnosability Analysis of Discrete Event Systems Using Labeled Petri Nets

  2021cites this paper
• Optimal Secret Protections in Discrete-Event Systems

  2021cites this paper
• Verification and enforcement of strong infinite- and k-step opacity using state recognizers

  2021cites this paper
• Strong current-state and initial-state opacity of discrete-event systems

  2021cites this paper
• Verification of Detectability for Unambiguous Weighted Automata

  2021cites this paper
• Analysis of strong and strong periodic detectability of bounded labeled Petri nets

  2021cites this paper
• Marking Estimation in Petri Nets Using Hierarchical Basis Reachability Graphs

  2021cites this paper
• Supervisory control of discrete-event systems under external attacks

  2021cites this paper
• Performance safety enforcement in stochastic event graphs against boost and slow attacks

  2021cites this paper
• Critical Observability of Discrete-Event Systems in a Petri Net Framework

  2021influential citation
• Non-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs

  2021cites this paper
• Usability Aware Secret Protection with Minimum Cost

  2021cites this paper
• Diagnosability Analysis of Discrete Event Systems Using a Compact State Space Representation

  2021cites this paper
• A general language-based framework for specifying and verifying notions of opacity

  2021cites this paper
• Privacy-Preserving Supervisory Control of Discrete-Event Systems via Co-Synthesis of Edit Function and Supervisor for Opacity Enforcement and Requirement Satisfaction

  2021cites this paper
• Privacy-Preserving Co-synthesis Against Sensor-Actuator Eavesdropping Intruder

  2021cites this paper
• Marking diagnosability verification in labeled Petri nets

  2021influential citation
• Optimal Synthesis of Opacity-Enforcing Supervisors for Qualitative and Quantitative Specifications

  2021cites this paper
• Verification of Approximate Opacity via Barrier Certificates

  2021cites this paper
• Opacity of Networked Supervisory Control Systems Over Insecure Communication Channels

  2021cites this paper
• Matrix Approach to Verify Initial-State Opacity of Discrete-Event Systems

  2020cites this paper
• Extended Insertion Functions for Opacity Enforcement in Discrete-Event Systems

  2020cites this paper
• Opacity Enforcing Supervisory Control Using Nondeterministic Supervisors

  2020cites this paper
• Opacity of Discrete Event Systems

  2020cites this paper
• Initial-State Estimation of Multi-Channel Networked Discrete Event Systems

  2020cites this paper
• On Multi-Step Look-Ahead Deadlock Prediction for Automated Manufacturing Systems Based on Petri Nets

  2020cites this paper
• Note that each information-Supervisory Control of Discrete-Event Systems for Infinite-Step Opacity

  2020cites this paper
• Optimal Secret Protections in Cyber-Physical Systems Modeled by Automata

  2020cites this paper
• Stealthy Sensor Attacks for Plants Modeled by Labeled Petri Nets

  2020cites this paper