A novel approach for supervisor synthesis to enforce opacity of discrete event systems

DOI10.1007/978-3-030-88052-1_13zbMath1496.68195OpenAlexW3201626205MaRDI QIDQ2672457

Kais Klai, Nour Elhouda Souid

Publication date: 8 June 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-88052-1_13

zbMATH Keywords

formal verificationdiscrete event systemsopacitysupervisory control theoryinformation flow securitysymbolic observation graph

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) Computer security (68M25)

Uses Software

• UMDES

Cites Work

• Enforcement and validation (at runtime) of various notions of opacity
• Concurrent secrets
• MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs
• Verification of Infinite-Step Opacity and Complexity Considerations
• Automated Technology for Verification and Analysis
• Quantifying opacity
• Unnamed Item
• Unnamed Item

This page was built for publication: A novel approach for supervisor synthesis to enforce opacity of discrete event systems