Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

bertrand:hal-01373354

N. Bertrand, S. Haddad, E. Lefaucheux. Diagnosis in Infinite-State Probabilistic Systems . In 27th International Conference on Concurrency Theory (Concur 2016), 27th International Conference on Concurrency Theory (Concur 2016), Québec city, Canada, August 2016.

Download [help]

Download paper: Doi page

Download Hal paper: Hal : Hyper Archive en ligne

Download paper: Adobe portable document (pdf) 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

In a recent work, we introduced four variants of diagnosability (FA, IA, FF, IF) in (finite) probabilistic systems (pLTS) depending whether one considers (1) finite or infinite runs and (2) faulty or all runs. We studied their relationship and established that the corresponding decision problems are PSPACE-complete. A key ingredient of the decision procedures was a characterisation of diagnosability by the fact that a random run almost surely lies in an open set whose specification only depends on the qualitative behaviour of the pLTS. Here we investigate similar issues for infinite pLTS. We first show that this characterisation still holds for FF-diagnosability but with a G-delta set instead of an open set and also for IF-and IA-diagnosability when pLTS are finitely branching. We also prove that surprisingly FA-diagnosability cannot be characterised in this way even in the finitely branching case. Then we apply our characterisations for a partially observable probabilistic extension of visibly pushdown automata (POpVPA), yielding EXPSPACE procedures for solving diagnosability problems. In addition, we establish some computational lower bounds and show that slight extensions of POpVPA lead to undecidability

Contact

Nathalie Bertrand http://www.irisa.fr/prive/nbertran/

BibTex Reference

@InProceedings{bertrand:hal-01373354,
   Author = {Bertrand, N. and Haddad, S. and Lefaucheux, E.},
   Title = {{Diagnosis in Infinite-State Probabilistic Systems }},
   BookTitle = {{27th International Conference on Concurrency Theory (Concur 2016)}},
   Series = {27th International Conference on Concurrency Theory (Concur 2016)},
   Address = {Qu{é}bec city, Canada},
   Month = {August},
   Year = {2016}
}

EndNote Reference [help]

Get EndNote Reference (.ref)