Verification of Opacity and Diagnosability for Pushdown Systems. (22nd May 2013)

• Record Type: Journal Article
• Authors: Kobayashi, Koichi; Hiraishi, Kunihiko
• Other Names: Luo Guiming Academic Editor.
• Is Part Of: Journal of applied mathematics. Volume 2013(2013)
• Publication Date: 2013-05-22
• Subjects: Mathematics -- Periodicals; 519.05
• DOI: 10.1155/2013/654059
• Languages: English
• ISSNs: 1110-757X

Abstract

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.