Verification of State-Based Opacity Using Petri Nets

DOI10.1109/TAC.2016.2620429zbMath1369.68265OpenAlexW2538443008MaRDI QIDQ5352631

Alessandro Giua, Carla Seatzu, Zhiwu Li, Yin Tong

Publication date: 8 September 2017

Published in: IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/tac.2016.2620429

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (33)

An optimization-based approach to assess non-interference in labeled and bounded Petri net systems ⋮ Enforcement for infinite-step opacity and K-step opacity via insertion mechanism ⋮ Verification of \(K\)-step and infinite-step opacity of bounded labeled Petri nets ⋮ A framework for current-state opacity under dynamic information release mechanism ⋮ A Framework for the Analysis of Supervised Discrete Event Systems Under Attack ⋮ Current-state opacity and initial-state opacity of modular discrete event systems ⋮ Decidability of opacity verification problems in labeled Petri net systems ⋮ Performance safety enforcement in stochastic event graphs against boost and slow attacks ⋮ Marking diagnosability verification in labeled Petri nets ⋮ A general language-based framework for specifying and verifying notions of opacity ⋮ Least-cost transition sequence estimation in labelled time Petri net systems with unobservable transitions ⋮ Supervisory control of discrete-event systems under external attacks ⋮ Strong current-state and initial-state opacity of discrete-event systems ⋮ Resource failure and buffer space allocation control for automated manufacturing systems ⋮ Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques ⋮ Information control in networked discrete event systems and its application to battery management systems ⋮ Privacy and safety analysis of timed stochastic discrete event systems using Markovian trajectory-observers ⋮ State estimation in labeled time Petri net systems using observed modified state class graph ⋮ Symbolic state estimation in bounded timed labeled Petri nets ⋮ Deadlock analysis and control using Petri net decomposition techniques ⋮ Current-state opacity modelling and verification in partially observed Petri nets ⋮ Verification of C-detectability using Petri nets ⋮ Current-state opacity enforcement in discrete event systems under incomparable observations ⋮ Enforcement of opacity by public and private insertion functions ⋮ On-line verification of current-state opacity by Petri nets and integer linear programming ⋮ Opacity of networked discrete event systems ⋮ Analysis of strong and strong periodic detectability of bounded labeled Petri nets ⋮ Enhancement of opacity for distributed state estimation in cyber-physical systems ⋮ Verification and enforcement of strong infinite- and \(k\)-step opacity using state recognizers ⋮ Usability aware secret protection with minimum cost ⋮ Deadlock and liveness characterization for a class of generalized Petri nets ⋮ Online verification of \(K\)-step opacity by Petri nets in centralized and decentralized structures ⋮ Diagnosis on a sliding window for partially observable Petri nets

This page was built for publication: Verification of State-Based Opacity Using Petri Nets