Diagnosis in Infinite-State Probabilistic Systems

Nathalie Bertrand 1, * Serge Haddad 2, 3 Engel Lefaucheux 3, 1
* Auteur correspondant
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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δ 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.
Type de document :
Communication dans un congrès
27th International Conference on Concurrency Theory (Concur 2016), Aug 2016, Québec city, Canada. 27th International Conference on Concurrency Theory (Concur 2016). 〈10.4230/LIPIcs.CONCUR.2016.37〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01373354
Contributeur : Engel Lefaucheux <>
Soumis le : mercredi 28 septembre 2016 - 15:36:34
Dernière modification le : mercredi 16 mai 2018 - 11:24:07

Fichier

p37-bertrand.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Nathalie Bertrand, Serge Haddad, Engel Lefaucheux. Diagnosis in Infinite-State Probabilistic Systems . 27th International Conference on Concurrency Theory (Concur 2016), Aug 2016, Québec city, Canada. 27th International Conference on Concurrency Theory (Concur 2016). 〈10.4230/LIPIcs.CONCUR.2016.37〉. 〈hal-01373354〉

Partager

Métriques

Consultations de la notice

425

Téléchargements de fichiers

42