On opacity and diagnosability in discrete event systems modeled by pushdown automata

In control theory of discrete event systems (DESs), it is one of the significant topics to develop control theory of infinite-state DESs. In this paper, we discuss opacity and diagnosability of infinite-state DESs modeled by pushdown automata (called here pushdown systems). First, we discuss opacity of pushdown systems, and it is proven that opacity of pushdown systems is in general undecidable. In addition, a decidable class is clarified. Next, in diagnosability, it is proven that under some assumption, which is different to an assumption in an existing result, diagnosability of pushdown systems is decidable. Furthermore, a necessary condition and a sufficient condition using finite-state approximations are derived, respectively. Finally, we discuss the relation between opacity and diagnosability. The obtained result is useful for developing control theory of infinite-state DESs.