×

zbMATH — the first resource for mathematics

Polynomial time decision algorithms for probabilistic automata. (English) Zbl 1329.68168
Summary: Deciding in an efficient way weak probabilistic bisimulation in the context of probabilistic automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. This enables us to arrive at a polynomial time algorithm for deciding weak probabilistic bisimulation, and also branching probabilistic bisimulation. We furthermore present several extensions to interesting related problems, in particular weak and branching probabilistic simulation, setting the ground for the development of more effective and compositional analysis algorithms for probabilistic systems.

MSC:
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
PRISM; SIGREF
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Segala, R., Modeling and verification of randomized distributed real-time systems, (1995), MIT, Ph.D. thesis
[2] Cheung, L.; Stoelinga, M.; Vaandrager, F. W., A testing scenario for probabilistic processes, J. ACM, 54, 6, (2007), Article No. 29 · Zbl 1326.68138
[3] Derman, C., Finite state Markovian decision processes, (1970), Academic Press, Inc. · Zbl 0262.90001
[4] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (CAV, LNCS, vol. 6806, (2011)), 585-591
[5] Vardi, M. Y., Automatic verification of probabilistic concurrent finite-state programs, (FOCS, (1985)), 327-338
[6] Hansson, H. A., Time and probability in formal design of distributed systems, Real-Time Safety Critical Systems, vol. 1, (1994), Elsevier
[7] Philippou, A.; Lee, I.; Sokolsky, O., Weak bisimulation for probabilistic systems, (CONCUR, LNCS, vol. 1877, (2000)), 334-349 · Zbl 0999.68146
[8] Segala, R., Probability and nondeterminism in operational models of concurrency, (CONCUR, LNCS, vol. 4137, (2006)), 64-78 · Zbl 1151.68553
[9] Milner, R., Communication and concurrency, (1989), Prentice-Hall International Englewood Cliffs · Zbl 0683.68008
[10] van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600, (1996) · Zbl 0882.68085
[11] Segala, R.; Lynch, N. A., Probabilistic simulations for probabilistic processes, Nord. J. Comput., 2, 2, 250-273, (1995) · Zbl 0839.68067
[12] Baier, C.; Engelen, B.; Majster-Cederbaum, M., Deciding bisimilarity and similarity for probabilistic processes, J. Comput. Syst. Sci., 60, 1, 187-231, (2000) · Zbl 1073.68690
[13] Cattani, S.; Segala, R., Decision algorithms for probabilistic bisimulation, (CONCUR, LNCS, vol. 2421, (2002)), 371-385 · Zbl 1012.68127
[14] Deng, Y., Axiomatisations and types for probabilistic and mobile processes, (2005), École des Mines de Paris, Ph.D. thesis
[15] Andova, S.; Willemse, T. A.C., Branching bisimulation for probabilistic systems: characteristics and decidability, Theor. Comput. Sci., 356, 3, 325-355, (2006) · Zbl 1092.68062
[16] Segala, R.; Turrini, A., Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models, (QEST, (2005)), 44-53
[17] Baier, C.; Stoelinga, M., Norm functions for probabilistic bisimulations with delays, (FoSSaCS, LNCS, vol. 1784, (2000)), 1-16 · Zbl 0961.68087
[18] Stoelinga, M., Alea jacta est: verification of probabilistic, real-time and parametric systems, (2002), University of Nijmegen, Ph.D. thesis
[19] Eisentraut, C.; Hermanns, H.; Zhang, L., On probabilistic automata in continuous time, (LICS, (2010)), 342-351
[20] Eisentraut, C.; Hermanns, H.; Zhang, L., Concurrency and composition in a stochastic world, (CONCUR, LNCS, vol. 6269, (2010)), 21-39 · Zbl 1287.68132
[21] Deng, Y.; Hennessy, M., On the semantics of Markov automata, (ICALP, LNCS, vol. 6756, (2011)), 307-318 · Zbl 1333.68162
[22] Hermanns, H., Interactive Markov chains: the quest for quantified quality, LNCS, vol. 2428, (2002), Springer · Zbl 1012.68142
[23] Coste, N.; Hermanns, H.; Lantreibecq, E.; Serwe, W., Towards performance prediction of compositional models in industrial GALS designs, (CAV, LNCS, vol. 5643, (2009)), 204-218 · Zbl 1242.68005
[24] Haverkort, B. R.; Kuntz, M.; Remke, A.; Roolvink, S.; Stoelinga, M., Evaluating repair strategies for a water-treatment facility using arcade, (DSN, (2010)), 419-424
[25] Esteve, M.-A.; Katoen, J.-P.; Nguyen, V. Y.; Postma, B.; Yushtein, Y., Formal correctness, safety, dependability and performance analysis of a satellite, (ICSE, (2012)), 1022-1031
[26] Wimmer, R.; Herbstritt, M.; Hermanns, H.; Strampp, K.; Becker, B., Sigref - a symbolic bisimulation tool box, (ATVA, LNCS, vol. 4218, (2006)), 477-492 · Zbl 1161.68631
[27] Hermanns, H.; Katoen, J.-P., Automated compositional Markov chain generation for a plain-old telephone system, Sci. Comput. Program., 36, 1, 97-127, (2000) · Zbl 0941.68649
[28] Böde, E.; Herbstritt, M.; Hermanns, H.; Johr, S.; Peikenkamp, T.; Pulungan, R.; Rakow, J.; Wimmer, R.; Becker, B., Compositional dependability evaluation for STATEMATE, Interact. Technol. Smart Educ., 35, 2, 274-292, (2009)
[29] Kanellakis, P. C.; Smolka, S. A., CCS expressions, finite state processes, and three problems of equivalence, Inf. Comput., 86, 1, 43-68, (1990) · Zbl 0705.68063
[30] Paige, R.; Tarjan, R. E., Three partition refinement algorithms, SIAM J. Comput., 16, 6, 973-989, (1987) · Zbl 0654.68072
[31] van Glabbeek, R. J., The linear time - branching time spectrum II, (CONCUR, LNCS, vol. 715, (1993)), 66-81
[32] Hermanns, H.; Turrini, A., Deciding probabilistic automata weak bisimulation in polynomial time, (FSTTCS, (2012)), 435-447 · Zbl 1354.68157
[33] Hermanns, H.; Turrini, A., Cost preserving bisimulations for probabilistic automata, (CONCUR, LNCS, vol. 8052, (2013)), 349-363 · Zbl 1390.68473
[34] Jonsson, B.; Larsen, K. G., Specification and refinement of probabilistic processes, (LICS, (1991)), 266-277
[35] Parma, A.; Segala, R., Axiomatization of trace semantics for stochastic nondeterministic processes, (QEST, (2004)), 294-303
[36] Zhang, L.; Hermanns, H.; Eisenbrand, F.; Jansen, D. N., Flow faster: efficient decision algorithms for probabilistic simulations, (TACAS, LNCS, vol. 4424, (2007)), 155-169 · Zbl 1186.68326
[37] Todd, M. J., The many facets of linear programming, Math. Program., 91, 3, 417-436, (2002) · Zbl 1030.90051
[38] Groote, J. F.; Vaandrager, F. W., An efficient algorithm for branching bisimulation and stuttering equivalence, (ICALP, LNCS, vol. 443, (1990)), 626-638 · Zbl 0765.68125
[39] Bouali, A., Weak and branching bisimulation in fctool, (1992), INRIA, Tech. Rep. RR-1575
[40] Henzinger, M. R.; Henzinger, T. A.; Kopke, P. W., Computing simulations on finite and infinite graphs, (FOCS, (1995)), 453-462 · Zbl 0938.68538
[41] Baier, C.; Hermanns, H., Weak bisimulation for fully probabilistic processes, (CAV, LNCS, vol. 1254, (1997)), 119-130
[42] Derisavi, S.; Hermanns, H.; Sanders, W. H., Optimal state-space lumping in Markov chains, Inf. Process. Lett., 87, 6, 309-315, (2003) · Zbl 1189.68039
[43] Turrini, A.; Hermanns, H., Cost preserving bisimulations for probabilistic automata, Log. Methods Comput. Sci., 4, 11, 1-58, (2014) · Zbl 1448.68353
[44] Calvete, H. I., Network simplex algorithm for the general equal flow problem, Eur. J. Oper. Res., 150, 3, 585-600, (2002) · Zbl 1033.90010
[45] Morrison, D. R.; Sauppe, J. J.; Jacobson, S. H., A network simplex algorithm for the equal flow problem on a generalized network, INFORMS J. Comput., 25, 1, 2-12, (2011)
[46] Morrison, D. R.; Sauppe, J. J.; Jacobson, S. H., An algorithm to solve the proportional network flow problem, Optim. Lett., 8, 3, 801-809, (2013) · Zbl 1292.90304
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.