Verification of \(K\)-step and infinite-step opacity of bounded labeled Petri nets

DOI10.1016/j.automatica.2022.110221zbMath1485.93361MaRDI QIDQ2125506

Yin Tong, Carla Seatzu, Hao Lan

Publication date: 14 April 2022

Published in: Automatica (Search for Journal in Brave)

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

zbMATH Keywords

Petri nets; discrete event systems; \(K\)-step opacity; infinite-step opacity

Mathematics Subject Classification ID

93C65: Discrete event control/observation systems

93B03: Attainable sets, reachability

Related Items

Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques

Uses Software

• UMDES

Cites Work

• Comparative analysis of related notions of opacity in centralized and coordinated architectures
• On-line verification of current-state opacity by Petri nets and integer linear programming
• 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 distributed approach for fault detection and diagnosis based on time Petri nets
• Introduction to Discrete Event Systems
• Basis Marking Representation of Petri Net Reachability Spaces and Its Application to the Reachability Problem
• Verification of State-Based Opacity Using Petri Nets
• Verification of Infinite-Step Opacity and Complexity Considerations