License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2016.37
URN: urn:nbn:de:0030-drops-61597
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6159/
Go to the corresponding LIPIcs Volume Portal

Bertrand, Nathalie ; Haddad, Serge ; Lefaucheux, Engel

Diagnosis in Infinite-State Probabilistic Systems

pdf-format:
LIPIcs-CONCUR-2016-37.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{bertrand_et_al:LIPIcs:2016:6159,
  author =	{Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
  title =	{{Diagnosis in Infinite-State Probabilistic Systems}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{37:1--37:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Jos{\'e}e Desharnais and Radha Jagadeesan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6159},
  URN =		{urn:nbn:de:0030-drops-61597},
  doi =		{10.4230/LIPIcs.CONCUR.2016.37},
  annote =	{Keywords: probabilistic systems, infinite-state systems, pushdown automata, diagnosis, partial observation}
}

Keywords: probabilistic systems, infinite-state systems, pushdown automata, diagnosis, partial observation
Collection: 27th International Conference on Concurrency Theory (CONCUR 2016)
Issue Date: 2016
Date of publication: 24.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI