-
Selection by year
-
Selection by authors
-
Complete lists
BBS-arxiv07
C. Baier, N. Bertrand, Ph. Schnoebelen. Verifying nondeterministic probabilistic channel systems against omega-regular linear-time properties. ACM Transactions on Computational Logic, 9(1), 2007.
Download [help]
Download paper: Adobe portable document (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
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
Contact
Nathalie Bertrand http://www.irisa.fr/prive/nbertran/
BibTex Reference
@article{BBS-arxiv07,
Author = {Baier, C. and Bertrand, N. and Schnoebelen, Ph.},
Title = {Verifying nondeterministic probabilistic channel systems against omega-regular linear-time properties},
Journal = {ACM Transactions on Computational Logic},
Volume = { 9},
Number = {1},
Publisher = {ACM Press},
Year = {2007}
}
EndNote Reference [help]
Get EndNote Reference (.ref)