Skip to main content
Department of Information Technology

The Good, the Bad, and the Random

Stochastic Games With Lossy Channels

Lossy channel systems (LCS) are models of processes communicating through unbounded fifo-buffers where messages may be lost. We consider game probabilistic LCS (GPLCS). In GPLCS, messages are lost probabilistically. Moreover, the control graph is a turn-based game rather than a simple transition system. GPLCS can be used to model, e.g., the situation where a malicious cracker tries to break a network protocol.

For GPLCS, we study the problem of almost sure repeated reachability: given a set F of "target states", can player 0 force the game to visit F infinitely many times with probability 1, no matter what player 1 does?

We give an algorithm to solve this problem, and prove correctness and termination.

This is joint work with Parosh Abdulla, Noomene Ben Henda, and Richard Mayr. A technical report is available here. It is also the last paper in my thesis.

Slides: sxi (654 kB), ps.bz2 (1.6 MB), pdf (1.4 MB)

Updated  2007-03-26 16:14:56 by Sven Sandberg.