Department of Information Technology

Lossy Channel Systems

Lossy Channel Systems consist of finite-state processes communicating over unbounded, but lossy, FIFO channels. Lossy channel systems can model many interesting systems, e.g. link protocols such as the Alternating Bit Protocol and HDLC. These protocols and others are designed to operate correctly even in the case that the FIFO channels are faulty and may lose messages. The state space of a lossy channel system is infinite due to the unboundedness of the channels.

Contributions

safety.jpg
  • Algorithm for Checking Saftey Properties [AJ93, AJ96a, AKP97]

An early significant result was our demonstration that safety properties of lossy channel systems could be automatically verified. This was one of the first examples in the literature of decidability of safety properties for a class of systems which is not essentially finite-state (in contrast e.g. to real-time automata). This result should be contrasted with the well-known fact that all non-trivial verification problems are undecidable for systems with unbounded perfect FIFO channels.

  • Undecidability of PTL, CTL, etc. [AJ94, AJ96b]

undecidable.gifAlthough safety properties are decidable, the general model checking problem is undecidable for propositional temporal logics such as PTL and CTL (when interpreted over lossy channel systems). We also show the undecidability of eventuality properties under different types of fairness conditions on the channels. The undecidabiltiy results are achieved through a reduction from a variant of Post's Correspondence Problem.

  • Simulation and Bisimulation [AK95]

simulation.jpgWe have shown (un)decidability results for different simulation and bisimulation relations between lossy channel systems and finite transition systems. More precisely, we show the decidability of (1) trace inclusion and equivalence between lossy channel systems and finite transition systems, (2) whether a state in a finite transition system simulates a state in a lossy channel system, and conversely, (3) whether a state in a finite transition system is bisimilar to a state in a lossy channel system, (4) whether a state in a finite transition system weakly simulates a state in a lossy channel, and (5) whether a state in a finite transition system is weakly bisimilar to a state in a lossy channel system system. Furthermore, we show the undecidability of the problem of whether a state in a lossy channel system weakly simulates a state in a finite transition system.

  • On-the-fly Verification [ABJ98, AAB99, AABJ00]

onthefly.jpgWe have shown how to perform on-the-fly verification of lossy channel systems, using forward reachability analysis. We propose a novel representation formalism, called simple regular expressions (SREs) , for representing sets of states of lossy channel systems. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of lossy channel systems. We have also implemented a prototype and used it to verify the Bounded Retransmission Protocol (BRP) of Philips.

  • Probabilistic Lossy Channel Systems. [ABIJ00]

probability.bmpWe show that the problem of checking whether a progress property holds with probability 1 is undecidable. More surprisingly, we show that checking whether safety properties hold with probability 1 is undecidable too. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.

  • Model Cecking Probabilistic Lossy Channel Systems. [ABM05, ABMSq06, ABMSa06]

We show that probabilistic lossy channel systems induce Markov chains which have finite attractors. An Attractor is a set of states which is reached with probability one from all other states. For this class of Markov chains, we show that many qualitative problems, sush as wether a set of states is reached/repeatdly reached with probability one/zero, are decidable.
We also prove that for lossy channel systems exact quantitative analysis is a "hard" problem in the sens that we cannot express the measure of runs, satisfying a given simple LTL property, in Tarski Algebra. Observe that this is possible for finite state Markov chains in general, and for few classes of infinite state Markov chains such as those induced by pushdown autoamata. Nevertheless, we propose some algorithms to approximate these probabilities up to an arbitrarily small error.
In recent works, we propose techniques for solving quantitative expectation problems. Typical examples of such problems are: the expected length of a path starting in an initial state and reaching a target set (expected execution time of a program) and the steady state distribution (the probability of being in a certain state in the long run).

Publications

You can find here a list of our published work.

Updated  2007-04-23 23:42:08 by Noomene Ben Henda.