PIPushdown

Ch. Morvan, S. Pinchinat. Diagnosis of Pushdown Systems. Research Report IRISA, No 1904, October 2008.

Download [help]

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

Diagnosis problems of discrete-event systems consist in detecting unobservable defects during system execution. For finite-state systems, the theory is well understood and a number of effective solutions have been developed. For infinite-state systems, however, there are only few results, mostly identifying classes where the problem is undecidable. We consider higher-order pushdown systems and investigate two basic variants of diagnosis problems: the diagnosability, which consists in deciding whether defects can be detected within a finite delay, and the bounded-latency problem, which consists in determining a bound for the delay of detecting defects. We establish that the diagnosability problem is decidable for arbitrary sub-classes of higher-order visibly pushdown systems provided unobservable events leave the stacks unchanged. For this case, we present an effective algorithm. Otherwise, we show that diagnosability becomes undecidable already for first-order visibly pushdown automata. Furthermore, we establish that the bounded-latency problem for higher-order pushdown systems is as hard as deciding finiteness of a higher-order pushdown language. This is in contrast with the case of finite-state systems where the problem reduces to diagnosability

Contact

Christophe Morvan http://www-igm.univ-mlv.fr/~cmorvan/

BibTex Reference

@TechReport{PIPushdown,
   Author = {Morvan, Ch. and Pinchinat, S.},
   Title = {Diagnosis of Pushdown Systems},
   Number = {1904},
   Institution = {IRISA},
   Month = {October},
   Year = {2008}
}

EndNote Reference [help]

Get EndNote Reference (.ref)