Current-state opacity modelling and verification in partially observed Petri nets

DOI10.1016/j.automatica.2020.108907zbMath1440.93024OpenAlexW3011778292MaRDI QIDQ1987252

Zhiwu Li, Ikram Saadaoui, NaiQi Wu

Publication date: 14 April 2020

Published in: Automatica (Search for Journal in Brave)

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

zbMATH Keywords

integer linear programmingPetri netopacityobservable behavioursecret behaviour

Mathematics Subject Classification ID

Integer programming (90C10) Discrete event control/observation systems (93C65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Attainable sets, reachability (93B03) Mathematical modeling or simulation for problems pertaining to systems and control theory (93-10)

Related Items (6)

A framework for current-state opacity under dynamic information release mechanism ⋮ Current-state opacity and initial-state opacity of modular discrete event systems ⋮ Least-cost transition sequence estimation in labelled time Petri net systems with unobservable transitions ⋮ Active opacity of discrete-event systems ⋮ Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques ⋮ Opacity of networked discrete event systems

Uses Software

• AIMMS
• Choco

Cites Work

• Unnamed Item
• Unnamed Item
• Comparative analysis of related notions of opacity in centralized and coordinated architectures
• Verification of initial-state opacity in security applications of discrete event systems
• Fault detection for discrete event systems using Petri nets with unobservable transitions
• Fault diagnosis in discrete event systems modeled by partially observed Petri nets
• Multilevel transitive and intransitive non-interference, causally
• Probabilistic system opacity in discrete event systems
• On-line verification of current-state opacity by Petri nets and integer linear programming
• Decidability of opacity verification problems in labeled Petri net systems
• Current-State Opacity Formulations in Probabilistic Finite Automata
• Verification of State-Based Opacity Using Petri Nets

This page was built for publication: Current-state opacity modelling and verification in partially observed Petri nets