# 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.