The Verification of Probabilistic Lossy Channel Systems

Philippe Schnoebelen
LSV, ENS Cachan
Friday, 21 March, 2003 (All day)

Lossy Channel Systems (LCS's) are systems of finite-state automata that communicate via unbounded fifo channels along which messages can be lost without any notification (hence the "Lossy"). They are a natural model for asynchronous protocols that are supposed to tolerate unreliable communication, of the kind one meets in embedded systems, in mobile systems, or on the WWW. Recently, several papers have proposed versions of LCS's where the losses of messages follow probabilistic rules. Sometimes the motivation is to obtain a finer view of the behaviour, where quantitative properties can be stated. Sometimes the goal is to circumvent undecidability by randomization. In this talk we will survey these different proposals and assess their interest. Special emphasis will be put on explaining the underlying algorithmic ideas in general terms that can be understood by computer scientists with no background in probabilistic systems.

Photographs of the seminar:

Picture of P. Schnoebelen Picture of P. Schnoebelen Picture of B. De Wachter