Verification of Opacity and Diagnosability for Pushdown Systems

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 pus...

Full description

Saved in:
Bibliographic Details
Published in:Journal of Applied Mathematics 2013-01, Vol.2013 (2013), p.527-536-561
Main Authors: Kobayashi, Koichi, Hiraishi, Kunihiko
Format: Article
Language:English
Subjects:
Cybersecurity
Extensible Markup Language
Language
Studies
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1110-757X
1687-0042
DOI:10.1155/2013/654059