Diagnosis in Infinite-State Probabilistic Systems

Authors Nathalie Bertrand, Serge Haddad, Engel Lefaucheux

Thumbnail PDF


  • Filesize: 0.58 MB
  • 15 pages

Document Identifiers

Author Details

Nathalie Bertrand
Serge Haddad
Engel Lefaucheux

Cite AsGet BibTex

Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. Diagnosis in Infinite-State Probabilistic Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


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.
  • probabilistic systems
  • infinite-state systems
  • pushdown automata
  • diagnosis
  • partial observation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. R. Alur and P. Madhusudan. Visibly pushdown languages. In Proc. STOC'04, pages 202-211. ACM, 2004. Google Scholar
  2. N. Bertrand, É. Fabre, S. Haar, S. Haddad, and L. Hélouët. Active diagnosis for probabilistic systems. In Proc. FoSSaCS'14, volume 8412 of LNCS, pages 29-42. Springer, 2014. Google Scholar
  3. N. Bertrand, S. Haddad, and E. Lefaucheux. Foundation of diagnosis and predictability in probabilistic systems. In Proc. FSTTCS'14, volume 29 of LIPIcs, pages 417-429. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  4. N. Bertrand, S. Haddad, and E. Lefaucheux. Accurate approximate diagnosability of stochastic systems. In Proc. LATA'16, volume 9618 of LNCS, pages 549-561. Springer, 2016. Google Scholar
  5. N. Bertrand, S. Haddad, and E. Lefaucheux. Diagnosis in infinite-state probabilistic systems (long version). Technical report, HAL Inria, 2016. URL: https://hal.inria.fr/hal-01334218.
  6. M. P. Cabasino, A. Giua, and C. Seatzu. Diagnosability of discrete-event systems using labeled Petri nets. IEEE Trans. Automation Science and Engineering, 11(1):144-153, 2014. Google Scholar
  7. K. Etessami and M. Yannakakis. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACM, 56(1), 2009. Google Scholar
  8. K. Etessami and M. Yannakakis. Model checking of recursive probabilistic systems. ACM Trans. Computational Logic, 13(2):12, 2012. Google Scholar
  9. S. Haar, S. Haddad, T. Melliti, and S. Schwoon. Optimal constructions for active diagnosis. In Proc. FSTTCS'13, volume 24 of LIPIcs, pages 527-539. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  10. S. Jiang, Z. Huang, V. Chandra, and R. Kumar. A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans. Automatic Control, 46(8):1318-1321, 2001. Google Scholar
  11. A. Kučera, J. Esparza, and R. Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2(1), 2006. Google Scholar
  12. C. Morvan and S. Pinchinat. Diagnosability of pushdown systems. In Proc. HVC'09, volume 6405 of LNCS, pages 21-33. Springer, 2009. Google Scholar
  13. Y. N. Moschovakis. Descriptive Set Theory. Mathematical Surveys and Monographs. AMS, 2009. Google Scholar
  14. M. Sampath, S. Lafortune, and D. Teneketzis. Active diagnosis of discrete-event systems. IEEE Trans. Automatic Control, 43(7):908-929, 1998. Google Scholar
  15. M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Diagnosability of discrete-event systems. IEEE Trans. Automatic Control, 40(9):1555-1575, 1995. Google Scholar
  16. D. Thorsley and D. Teneketzis. Diagnosability of stochastic discrete-event systems. IEEE Trans. Automatic Control, 50(4):476-492, 2005. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail