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...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/654059 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850231812113039360 |
|---|---|
| author | Koichi Kobayashi Kunihiko Hiraishi |
| author_facet | Koichi Kobayashi Kunihiko Hiraishi |
| author_sort | Koichi Kobayashi |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-02c9c3c8e0224e7781c7ddc1da8ffa94 |
| institution | OA Journals |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-02c9c3c8e0224e7781c7ddc1da8ffa942025-08-20T02:03:25ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/654059654059Verification of Opacity and Diagnosability for Pushdown SystemsKoichi Kobayashi0Kunihiko Hiraishi1School of Information Science, Japan Advanced Institute of Science and Technology, Ishikawa 923-1292, JapanSchool of Information Science, Japan Advanced Institute of Science and Technology, Ishikawa 923-1292, JapanIn 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.http://dx.doi.org/10.1155/2013/654059 |
| spellingShingle | Koichi Kobayashi Kunihiko Hiraishi Verification of Opacity and Diagnosability for Pushdown Systems Journal of Applied Mathematics |
| title | Verification of Opacity and Diagnosability for Pushdown Systems |
| title_full | Verification of Opacity and Diagnosability for Pushdown Systems |
| title_fullStr | Verification of Opacity and Diagnosability for Pushdown Systems |
| title_full_unstemmed | Verification of Opacity and Diagnosability for Pushdown Systems |
| title_short | Verification of Opacity and Diagnosability for Pushdown Systems |
| title_sort | verification of opacity and diagnosability for pushdown systems |
| url | http://dx.doi.org/10.1155/2013/654059 |
| work_keys_str_mv | AT koichikobayashi verificationofopacityanddiagnosabilityforpushdownsystems AT kunihikohiraishi verificationofopacityanddiagnosabilityforpushdownsystems |