Verification of Opacity and Diagnosability for Pushdown Systems

Koichi Kobayashi and Kunihiko Hiraishi

Journal of Applied Mathematics, 2013, vol. 2013, issue 1

Abstract: 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.

Date: 2013
References: Add references at CitEc
Citations:

Downloads: (external link)
https://doi.org/10.1155/2013/654059

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:wly:jnljam:v:2013:y:2013:i:1:n:654059

Access Statistics for this article

More articles in Journal of Applied Mathematics from John Wiley & Sons
Bibliographic data for series maintained by Wiley Content Delivery ().