Journal of Applied Mathematics
Volume 2013 (2013), Article ID 654059, 10 pages
Research Article

Verification of Opacity and Diagnosability for Pushdown Systems

School of Information Science, Japan Advanced Institute of Science and Technology, Ishikawa 923-1292, Japan

Received 26 February 2013; Revised 28 April 2013; Accepted 30 April 2013

Academic Editor: Guiming Luo

Copyright © 2013 Koichi Kobayashi and Kunihiko Hiraishi. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.


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.