Verifying nondeterministic probabilistic channel systems against $ømega$-regular linear-time properties

Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Philippe SchnoebelenPhilippe Schnoebelen

DOI Link

Christel Baier, Nathalie Bertrand, Philippe Schnoebelen
Verifying nondeterministic probabilistic channel systems against $ømega$-regular linear-time properties
ACM Transactions on Computational Logic, 9, 2007

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BBS2007,
  author  = {Christel Baier and Nathalie Bertrand and Philippe Schnoebelen},
  title   = {Verifying nondeterministic probabilistic channel systems against
             ${\o}mega$-regular linear-time properties},
  journal = {ACM Transactions on Computational Logic},
  volume  = {9},
  year    = {2007},
  doi     = {10.1145/1297658.1297663}
}