Establishing qualitative properties for probabilistic lossy channel systems : an algorithmic approach

Baier, Christel ; Engelen, Bettina ; Roggenbach, Markus

1999_03.pdf - Published

Download (1MB)

URN: urn:nbn:de:bsz:180-madoc-19392
Document Type: Working paper
Year of publication: 1999
The title of a journal, publication series: None
Publication language: English
Institution: School of Business Informatics and Mathematics > Sonstige - Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik
MADOC publication series: Veröffentlichungen der Fakultät für Mathematik und Informatik > Institut für Informatik > Technical Reports
Subject: 004 Computer science, internet
Classification: MSC: 68Q85 ,
Subject headings (SWD): Kommunikationssystem , Softwarespezifikation
Abstract: Lossy channel systems (LCSs for short) are models for communicating systems where the subprocesses are linked via unbounded FIFO channels which might lose messages. Link protocols, such as the Alternating Bit Protocol and HDLC can be modelled with these systems. The decidability of several verification problems of LCSs has been investigated by Abdulla & Jonsson [AJ93,AJ94], e.g. they have shown that the reachability problem for LCSs is decidable while LT L model checking is not. In this paper, we consider probabilistic LCSs (which are LCSs where the transitions are augmented with appropriate probabilities) as introduced by [IN97] and show that the question of whether or not a linear time property holds with probability 1 is deddable. More precisely, we show how LT L\x model checking for (certain types of) probabilistic LCSs can be reduced to a reachability problem in a (non-probabilistic) LCS where the latter can be solved with the methods of [AJ93].
Additional information:

Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.

Metadata export


+ Search Authors in

+ Download Statistics

Downloads per month over past year

View more statistics

You have found an error? Please let us know about your desired correction here: E-Mail

Actions (login required)

Show item Show item