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.