Verification of Infinite-Step Opacity and Complexity Considerations

DOI10.1109/TAC.2011.2173774zbMath1369.93110MaRDI QIDQ5352820

Anooshiravan Saboori, Christoforos N. Hadjicostis

Publication date: 8 September 2017

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

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Observability (93B07) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (28)

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 ⋮ \(k\)-memory-embedded insertion mechanism for opacity enforcement ⋮ Verification of opacity and diagnosability for pushdown systems ⋮ Current-state opacity and initial-state opacity of modular discrete event systems ⋮ A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers ⋮ Compositional synthesis of opacity-preserving finite abstractions for interconnected systems ⋮ Verification of detectability in probabilistic finite automata ⋮ Verification complexity of a class of observational properties for modular discrete events systems ⋮ A novel approach for supervisor synthesis to enforce opacity of discrete event systems ⋮ Verification and enforcement of current-state opacity based on a state space approach ⋮ Enforcement and validation (at runtime) of various notions of opacity ⋮ Strong current-state and initial-state opacity of discrete-event systems ⋮ Detectability in stochastic discrete event systems ⋮ State-based opacity of labeled real-time automata ⋮ Active opacity of discrete-event systems ⋮ Matrix approach for verification of opacity of partially observed discrete event systems ⋮ Verifying weak and strong \(k\)-step opacity in discrete-event systems ⋮ Infinite-step opacity and \(K\)-step opacity of stochastic discrete-event systems ⋮ Probabilistic opacity for Markov decision processes ⋮ Enforcement of opacity by public and private insertion functions ⋮ Relative predictability of failure event occurrences and its opacity-based test algorithm ⋮ Opacity of networked discrete event systems ⋮ Verification of approximate opacity for switched systems: a compositional approach ⋮ Comparing the notions of opacity for discrete-event systems ⋮ Online verification of \(K\)-step opacity by Petri nets in centralized and decentralized structures ⋮ Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems

This page was built for publication: Verification of Infinite-Step Opacity and Complexity Considerations