Verification of Opacity and Diagnosability for Pushdown Systems

Abstract EN

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.