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.