×

An efficient algorithm to determine probabilistic bisimulation. (English) Zbl 1461.68133

Summary: We provide an algorithm to efficiently compute bisimulation for probabilistic labeled transition systems, featuring non-deterministic choice as well as discrete probabilistic choice. The algorithm is linear in the number of transitions and logarithmic in the number of states, distinguishing both action states and probabilistic states, and the transitions between them. The algorithm improves upon the proposed complexity bounds of the best algorithm addressing the same purpose so far by C. Baier et al. [J. Comput. Syst. Sci. 60, No. 1, 187–231 (2000; Zbl 1073.68690)]. In addition, experimentally, on various benchmarks, our algorithm performs rather well; even on relatively small transition systems, a performance gain of a factor 10,000 can be achieved.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68W40 Analysis of algorithms

Citations:

Zbl 1073.68690

Software:

mCRL2
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Larsen, K.G.; Skou, A.; Bisimulation through probabilistic testing; Inf. Comput.: 1991; Volume 94 ,1-28. · Zbl 0756.68035
[2] Segala, R.; Modeling and Verification of Randomized Distributed Real-Time Systems; Ph.D. Thesis: Cambridge, MA, USA 1995; .
[3] Segala, R.; Lynch, N.; Probabilistic Simulations for Probabilistic Processes; CONCUR ’94: Concurrency Theory: Berlin, Germany 2005; Volume Volume 836 ,481-496.
[4] Baier, C.; Engelen, B.; Majster-Cederbaum, M.E.; Deciding bisimilarity and similarity for probabilistic processes; J. Comput. Syst. Sci.: 2000; Volume 60 ,187-231. · Zbl 1073.68690
[5] Paige, R.; Tarjan, R.E.; Three partition refinement algorithms; SIAM J. Comput.: 1987; Volume 16 ,973-989. · Zbl 0654.68072
[6] Valmari, A.; Franceschinis, G.; Simple O(mlogn) time Markov chain lumping; Proceedings of the 16th international conference on Tools and Algorithms for the Construction and Analysis of Systems: ; ,38-52. · Zbl 1284.68437
[7] Dersavi, S.; Hermanns, H.; Sanders, H.; Optimal state-space lumping in Markov chains; Inf. Process. Lett.: 2003; Volume 87 ,309-315. · Zbl 1189.68039
[8] Kwiatkowska, M.; Norman, G.; Parker, D.; Stochastic model checking; Proceedings of the 7th international conference on Formal methods for performance evaluation: ; ,220-270. · Zbl 1323.68379
[9] Groote, J.F.; Mousavi, M.R.; ; Modeling and Analysis of Communication Systems: Cambridge, MA, USA 2014; . · Zbl 1353.68006
[10] Cranen, S.; Groote, J.F.; Keiren, J.J.A.; Stapper, F.P.M.; de Vink, E.P.; Wesselink, J.W.; Willemse, T.A.C.; An Overview of the mCRL2 Toolset and Its Recent Advances; Tools and Algorithms for the Construction and Analysis of Systems: Berlin, Germany 2013; Volume Volume 7795 ,199-213. · Zbl 1381.68198
[11] Hansson, H.A.; Jonsson, B.; A logic for reasoning about time and reliability; Formal Aspects Comput.: 1994; Volume 6 ,512-535. · Zbl 0820.68113
[12] Katoen, J.-P.; Kemna, T.; Zapreev, I.; Jansen, D.N.; Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking; Tools and Algorithms for the Construction and Analysis of Systems: Berlin, Germany 2007; Volume Volume 4424 ,87-101. · Zbl 1186.68296
[13] Dehnert, C.; Katoen, J.-P.; Parker, D.; SMT-based bisimulation Minimisation of Markov Models; Verification, Model Checking, and Abstract Interpretation: Berlin, Germany 2013; Volume Volume 7737 ,28-47. · Zbl 1426.68168
[14] Song, L.; Zhang, L.; Hermanns, H.; Godskesen, J.C.; Incremental bisimulation abstraction refinement; ACM Trans. Embedded Comput. Syst.: 2014; Volume 13 ,1-23.
[15] Hillston, J.; Marin, A.; Rossi, S.; Piazza, C.; Contextual lumpability; Proceedings of the 7th International Conference on Performance Evaluation Methodologies and Tools: ; ,194-203.
[16] Crafa, S.; Ranzato, F.; Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation; Formal Methods Syst. Des.: 2012; Volume 40 ,356-376. · Zbl 1290.68093
[17] Dorsch, U.; Milius, S.; Schröder, L.; Wissmann, T.; Efficient coalgebraic partition refinement; arXiv: 2017; .
[18] Zhang, L.; Hermanns, H.; Eisenbrand, F.; Jansen, D.N.; Flow faster: efficient decision algorithms for probabilistic simulations; Logical Methods Comput. Sci.: 2008; Volume 4 ,1-43. · Zbl 1161.68473
[19] Zhang, L.; Jansen, D.N.; A space-efficient simulation algorithm on probabilistic automata; Inf. Comput.: 2016; Volume 249 ,138-159. · Zbl 1345.68219
[20] Cattani, S.; Segala, R.; Decision Algorithms for Probabilistic Bisimulation; CONCUR 2002 — Concurrency Theory: Berlin, Germany 2002; Volume Volume 2421 ,371-386. · Zbl 1012.68127
[21] Turrini, A.; Hermanns, H.; Polynomial time decision algorithms for probabilistic automata; Inf. Comput.: 2015; Volume 244 ,134-171. · Zbl 1329.68168
[22] Hennessy, M.; Exploring probabilistic bisimulations, part I; Formal Aspects Comput.: 2012; Volume 24 ,749-768. · Zbl 1259.68153
[23] Kannelakis, P.; Smolka, S.; CCS expressions, finite state processes and three problems of equivalence; Inf. Comput.: 1990; Volume 86 ,43-68. · Zbl 0705.68063
[24] Groote, J.F.; Jansen, D.N.; Keiren, J.J.A.; Wijs, A.J.; An O(mlogn) algorithm for computing stuttering equivalence and branching bisimulation; ACM Trans. Comput. Logic: 2017; Volume 18 ,1-34. · Zbl 1367.68211
[25] Valmari, A.; Simple bisimilarity minimization in O(mlogn) time; Fundam. Inf.: 2010; Volume 105 ,319-339. · Zbl 1209.68344
[26] Baier, C.; ; Personal communication: 2018; .
[27] Antonick, G.; Ant on a grid; ; .
[28] Groote, J.F.; de Vink, E.P.; Problem Solving Using Process Algebra Considered Insightful; ModelEd, TestEd, TrustEd. Lecture Notes in Computer Science: Cham, Switzerland 2017; Volume Volume 10500 ,48-63. · Zbl 1498.68186
[29] Bandini, E.; Segala, R.; Axiomatizations for probabilistic bisimulation; Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP) 2001: ; ,370-381. · Zbl 0986.68073
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.