Verifying nondeterministic probabilistic channel systems against $\omega$-regular linear-time properties

Christel Baier, Nathalie Bertrand, Philippe Schnoebelen

Lossy channel systems (LCSs) are systems of finite state automata that communicate via unreliable unbounded fifo channels. In order to circumvent the undecidability of model checki…