Verifying nondeterministic probabilistic channel systems against omega-regular linear-time properties.

Abstract : Lossy channel systems (LCS's) are systems of finite state processes that communicate via unreliable unbounded fifo channels. We introduce NPLCS's, a variant of LCS's where message losses have a probabilistic behavior while the component processes behave nondeterministically, and study the decidability of qualitative verification problems for omega-regular linear-time properties. We show that – in contrast to finite-state Markov decision processes – the satisfaction relation for lineartime formulas depends on the type of schedulers that resolve the nondeterminism. While the qualitative model checking problems for the full class of history-dependent schedulers is undecidable, the same questions for finitememory schedulers can be solved algorithmically. Additionally, some special kinds of reachability, or recurrent reachability, qualitative properties yield decidable verification problems for the full class of schedulers, which – for this restricted class of problems – are as powerful as finite-memory schedulers, or even a subclass of them.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2007, 9 (1), 〈10.1145/1297658.1297663〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00424516
Contributeur : Nathalie Bertrand <>
Soumis le : vendredi 16 octobre 2009 - 10:55:16
Dernière modification le : mardi 13 mars 2018 - 14:24:05

Lien texte intégral

Identifiants

Collections

Citation

Christel Baier, Nathalie Bertrand, Philippe Schnoebelen. Verifying nondeterministic probabilistic channel systems against omega-regular linear-time properties.. ACM Transactions on Computational Logic, Association for Computing Machinery, 2007, 9 (1), 〈10.1145/1297658.1297663〉. 〈inria-00424516〉

Partager

Métriques

Consultations de la notice

67