Verification of opacity and diagnosability for pushdown systems

DOI10.1155/2013/654059MaRDI QIDQ2375627zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Koichi Kobayashi, Kunihiko Hiraishi

Publication date 14 June 2013

Published in Journal of Applied Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1155/2013/654059

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65)

Review text

Summary: In control theory of discrete event systems (DESs), one of the challenging topics is the extension of theory of finite-state DESs to that of infinite-state DESs. In this paper, we discuss verification of opacity and diagnosability for infinite-state DESs modeled by pushdown automata (called here pushdown systems). First, we discuss opacity of pushdown systems and prove that opacity of pushdown systems is in general undecidable. In addition, a decidable class is clarified. Next, in diagnosability, we prove that under a certain assumption, which is different from the assumption in the existing result, diagnosability of pushdown systems is decidable. Furthermore, a necessary condition and a sufficient condition using finite-state approximations are derived. Finally, as one of the applications, we consider data integration using XML (Extensible Markup Language). The obtained result is useful for developing control theory of infinite-state DESs.

Recommendations

• Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems
• The complexity of diagnosability and opacity verification for Petri nets
• The complexity of diagnosability and opacity verification for Petri nets
• Diagnosis in infinite-state probabilistic systems
• Verification and enforcement of strong infinite- and k-step opacity using state recognizers

Cites work

• A New Approach for Diagnosability Analysis of Petri Nets Using Verifier Nets
• A Note on the Properties of the Supremal Controllable Sublanguage in Pushdown Systems
• Automata, Languages and Programming
• Concurrent secrets
• Diagnosability of discrete-event systems
• Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 2087217 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• Introduction to Discrete Event Systems
• NP-completeness of sensor selection problems arising in partially observed discrete-event systems
• Optimal sensor selection for discrete-event systems with partial observation
• Regular approximation of context-free grammars through transformation
• Rewriting of visibly pushdown languages for XML data integration
• Superdeterministic PDAs
• Synthesis of opaque systems with static and dynamic masks
• Verification of Infinite-Step Opacity and Complexity Considerations
• Verifying complex continuous real-time systems with coinductive CLP(R)

Cited in

(3)

• Opacity of networked discrete event systems
• Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems
• A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers

Describes a project that uses

Uses Software

• UMDES

This page was built for publication: Verification of opacity and diagnosability for pushdown systems

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