|
Deciding bisimilarity and bimilarity for probabilistic processes
Baier, Christel
;
Engelen, Bettina
;
Majster-Cederbaum, Mila
|
DOI:
|
https://doi.org/10.1006/jcss.1999.1683
|
|
URL:
|
https://www.sciencedirect.com/science/article/pii/...
|
|
Dokumenttyp:
|
Zeitschriftenartikel
|
|
Erscheinungsjahr:
|
2000
|
|
Titel einer Zeitschrift oder einer Reihe:
|
Journal of Computer and System Sciences
|
|
Band/Volume:
|
60
|
|
Heft/Issue:
|
1
|
|
Seitenbereich:
|
187-231
|
|
Ort der Veröffentlichung:
|
San Diego, Calif.
|
|
Verlag:
|
Elsevier
|
|
ISSN:
|
0022-0000 , 1090-2724
|
|
Sprache der Veröffentlichung:
|
Englisch
|
|
Einrichtung:
|
Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Praktische Informatik II (Majster-Cederbaum -2005, Em)
|
|
Fachgebiet:
|
004 Informatik
|
|
Abstract:
|
This paper deals with probabilistic and nondeterministic processes represented by a variant of labeled transition systems where any outgoing transition of a state s is augmented with probabilities for the possible successor states. Our main contributions are algorithms for computing this bisimulation equivalence classes as introduced by Larsen and Skou (1996, Inform. and Comput.99, 1–28), and the simulation preorder à la Segala and Lynch (1995, Nordic J. Comput.2, 250–273). The algorithm for deciding bisimilarity is based on a variant of the traditional partitioning technique and runs in time (mn(log m+log n)) where m is the number of transitions and n the number of states. The main idea for computing the simulation preorder is the reduction to maximum flow problems in suitable networks. Using the method of Cheriyan, Hagerup, and Mehlhorn, (1990, Lecture Notes in Computer Science, Vol. 443, pp. 235–248, Springer-Verlag, Berlin) for computing the maximum flow, the algorithm runs in time ((mn6+m2n3)/log n). Moreover, we show that the network-based technique is also applicable to compute the simulation-like relation of Jonsson and Larsen (1991, “Proc. LICS'91” pp. 266–277) in fully probabilistic systems (a variant of ordinary labeled transition systems where the nondeterminism is totally resolved by probabilistic choices).
|
 | Dieser Eintrag ist Teil der Universitätsbibliographie. |
 Suche Autoren in
Sie haben einen Fehler gefunden? Teilen Sie uns Ihren Korrekturwunsch bitte hier mit: E-Mail
Actions (login required)
 |
Eintrag anzeigen |
|
|
