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


Baier, Christel ; Engelen, Bettina ; Roggenbach, Markus


[img]
Vorschau
PDF
1999_03.pdf - Veröffentlichte Version

Download (1MB)

URL: http://ub-madoc.bib.uni-mannheim.de/1939
URN: urn:nbn:de:bsz:180-madoc-19392
Dokumenttyp: Arbeitspapier
Erscheinungsjahr: 1999
Titel einer Zeitschrift oder einer Reihe: None
Sprache der Veröffentlichung: Englisch
Einrichtung: Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Sonstige - Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik
MADOC-Schriftenreihe: Veröffentlichungen der Fakultät für Mathematik und Informatik > Institut für Informatik > Technical Reports
Fachgebiet: 004 Informatik
Fachklassifikation: MSC: 68Q85 ,
Normierte Schlagwörter (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].
Zusätzliche Informationen:




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




Metadaten-Export


Zitation


+ Suche Autoren in

+ Download-Statistik

Downloads im letzten Jahr

Detaillierte Angaben



Sie haben einen Fehler gefunden? Teilen Sie uns Ihren Korrekturwunsch bitte hier mit: E-Mail


Actions (login required)

Eintrag anzeigen Eintrag anzeigen