Name
Title | ||
|---|---|---|
Verifying nondeterministic probabilistic channel systems against ω-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 ω-regular linear-time properties. We show that—in contrast to finite-state Markov decision processes—the satisfaction relation for linear-time formulas depends on the type of schedulers that resolve the nondeterminism. While the qualitative model checking problem for the full class of history-dependent schedulers is undecidable, the same question for finite-memory 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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1297658.1297663 | ACM Transactions on Computational Logic (TOCL) |
Keywords | Field | DocType |
qualitative model checking problem,history-dependent schedulers,nondeterministic probabilistic channel system,full class,regular linear-time property,linear-time formula,qualitative verification problem,qualitative property,finite-memory schedulers,recurrent reachability,restricted class,decidable verification problem,linear time,probabilistic model,communication protocol,markov decision process,markov decision processes,communication protocols | Discrete mathematics,Model checking,Nondeterministic algorithm,Algorithm,Markov decision process,Reachability,Decidability,Theoretical computer science,Probabilistic logic,Time complexity,Mathematics,Undecidable problem | Journal |
Volume | Issue | ISSN |
9 | 1 | ACM Trans. Computational Logic 9(1), 2007 |
Citations | PageRank | References |
13 | 0.63 | 25 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christel Baier | 1 | 3053 | 185.85 |
| Nathalie Bertrand | 2 | 250 | 17.84 |
| Philippe Schnoebelen | 3 | 387 | 23.46 |