Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ICALP

2003

Springer

2003

Springer

Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behaviour of such protocols, lossy channel systems (LCS) have been proposed. In an LCS the communication channels are modelled as FIFO buffers which are unbounded, but also unreliable in the sense that they can nondeterministically lose messages. Recently, several attempts have been made to study probabilistic lossy channel systems (PLCS) in which the probability of losing messages is taken into account and the following qualitative model checking problem is investigated: to verify whether a given property holds with probability one. Here we consider a more challenging problem, namely to calculate the probability by which a certain property is satisﬁed. Our main result is an algorithm for the following Quantitative model checking problem: Instance: A PLCS, its state s, a ﬁnite state ω-automaton A, and a rational Â>0. Task:Find a rational r such...

Related Content

Added |
06 Jul 2010 |

Updated |
06 Jul 2010 |

Type |
Conference |

Year |
2003 |

Where |
ICALP |

Authors |
Alexander Moshe Rabinovich |

Comments (0)