Strong state-based opacity verification using HyperLTL model checking technique

DOI10.1080/00207179.2025.2608824MaRDI QIDQ7295431zbMATH OpenFDO

Authors Jia-Hui Zhang, Xiaoguang Han, Miao Zhang

Publication date 13 July 2026

Published in International Journal of Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/00207179.2025.2608824

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65)

Cites work

• \(k\)-memory-embedded insertion mechanism for opacity enforcement
• A unified framework for verification of observational properties for partially-observed discrete-event systems
• A Uniform Approach for Synthesizing Property-Enforcing Supervisors for Partially-Observed Discrete-Event Systems
• AutoHyper: explicit-state model checking for HyperLTL
• Comparative analysis of related notions of opacity in centralized and coordinated architectures
• Comparing the notions of opacity for discrete-event systems
• Concurrent secrets
• Current-state opacity and initial-state opacity of modular discrete event systems
• Enforcement and validation (at runtime) of various notions of opacity
• Estimation and inference in discrete event systems. A model-based approach with finite automata
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Information control in networked discrete event systems and its application to battery management systems
• Introduction to Discrete Event Systems
• Least-cost transition sequence estimation in labelled time Petri net systems with unobservable transitions
• Modelling opacity using Petri nets
• Notions of Centralized and Decentralized Opacity in Linear Systems
• On Approximate Opacity of Cyber-Physical Systems
• Opacity Enforcement for Confidential Robust Control in Linear Cyber-Physical Systems
• Opacity Enforcement Using Nondeterministic Publicly Known Edit Functions
• Opacity of discrete event systems and its applications
• Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach
• Robustly distributed diagnosis of discrete-event systems and its application to alipay transaction systems
• Strong current-state and initial-state opacity of discrete-event systems
• Synthesis of opaque systems with static and dynamic masks
• Verification and enforcement of strong infinite- and k-step opacity using state recognizers
• Verification of Infinite-Step Opacity and Complexity Considerations
• Verification of initial-state opacity in security applications of discrete event systems
• Verifying weak and strong \(k\)-step opacity in discrete-event systems

This page was built for publication: Strong state-based opacity verification using HyperLTL model checking technique

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7295431)