Verification of Opacity and Diagnosability for Pushdown Systems

Koichi Kobayashi and Kunihiko Hiraishi

Journal of Applied Mathematics, 2013, vol. 2013, 1-10

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)
http://downloads.hindawi.com/journals/JAM/2013/654059.pdf (application/pdf)
http://downloads.hindawi.com/journals/JAM/2013/654059.xml (text/xml)

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:hin:jnljam:654059

DOI: 10.1155/2013/654059

Access Statistics for this article

More articles in Journal of Applied Mathematics from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().