Abstract
Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the specific complexity class of the weak probabilistic bisimulation problem, and it considers several practical algorithms and linear programming problem transformations that enable an efficient solution. We then discuss two different implementations of a probabilistic automata weak probabilistic bisimulation minimizer, one of them employing SAT modulo linear arithmetic as the solver technology. Empirical results demonstrate the effectiveness of the minimization approach on standard benchmarks, also highlighting the benefits of compositional minimization.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Arora S, Hazan E, Kale S (2012) The multiplicative weights update method: a meta-algorithm and applications. Theory Comput 8: 121–164
Ahuja RK, Magnanti TJ, Orlin JB (1993) Network flows: theory, algorithms, and applications. Prentice Hall, New York
Anstreicher KM (1999) Linear programming in \({\mathcal{O}(\frac{n^3}{{\rm \ln} n} L)}\) operations. SIAM J. Optim. 9(4): 803–812
Beling PA (2001) Exact algorithms for linear programming over algebraic extensions. Algorithmica 31(4): 459–478
Bahçeci U, Feyziog̃lu O (2012) A network simplex based algorithm for the minimum cost proportional flow problem with disconnected subnetworks. Optim Lett 6: 1173–1184
Böde E, Herbstritt M, Hermanns H, Johr S, Peikenkamp T, Pulungan R, Rakow J, Wimmer R, Becker B (2009) Compositional dependability evaluation for STATEMATE. ITSE 35(2): 274–292
Blum L, Shub M, Smale M (1989) On a theory of computation and complexity over the real numbers; \({NP}\)-completeness, recursive functions and universal machines. Bull Am Math Soc 21(1): 1–46
Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. In SMT
Bertsimas D, Tsitsiklis JN (1997) Introduction to linear optimization. Athena Scientific, Belmont
Calvete HI (2002) Network simplex algorithm for the general equal flow problem. Eur J Oper Res 150(3): 585–600
Chehaibar G, Garavel H, Mounier L, Tawbi N, Zulian F (1996) Specification and verification of the \({{\rm PowerScale^{registered}}}\) bus arbitration protocol: an industrial experiment with LOTOS. In: FORTE, pp 435–450
Crouzen P, Hermanns H (2010) Aggregation ordering for massively compositional models. In: ACSD, pp 171–180,
Coste N, Hermanns H, Lantreibecq E, Serwe W (2009) Towards performance prediction of compositional models in industrial GALS designs. In: CAV. LNCS, vol 5643, pp 204–218
Christiano P, Kelner JA, M¸dry A, Spielman D (2011) Electrical flows, laplacian systems, and faster approximation of maximum flow in undirected graphs. In: STOC, pp 273–282
Crouzen P, Lang F (2011) Smart reduction. In FASE. LNCS, vol 6603, pp 111–126
Cattani S, Segala R (2002) Decision algorithms for probabilistic bisimulation. In: CONCUR of LNCS, vol 2421, pp 371–385
Deng Y (2005) Axiomatisations and types for probabilistic and mobile processes. PhD thesis, École des Mines de Paris
Derman C (1970) Finite state markovian decision processes. Academic Press, Inc, New York
Mendonça de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS. LNCS, vol 4963, pp 337–340
Eisentraut C, Hermanns H, Schuster J, Turrini A, Zhang L (2013) The quest for minimal quotients for probabilistic automata. In: TACAS. LNCS, vol 7795, pp 16–31
Eisentraut C, Hermanns H, Zhang L (2010) Concurrency and composition in a stochastic world. In: CONCUR. LNCS, vol 6269, pp 21–39
Eisentraut C, Hermanns H, Zhang L (2010) On probabilistic automata in continuous time. In: LICS, pp 342–351
Gebler D, Hashemi V, Turrini A (2014) Computing behavioral relations for probabilistic concurrent systems. In: Stochastic model checking. Rigorous dependability analysis using model checking techniques for stochastic systems. LNCS, vol 8453. Springer Berlin Heidelberg, pp 117–155
GNU linear programming kit. http://www.gnu.org/software/glpk/.
Graf S, Steffen B, Lüttgen G (1996) Compositional minimisation of finite state systems using interface specifications. Formal Asp Comput 8(5): 607–616
Hansson HA (1991) Time and probability in formal design of distributed systems. PhD thesis, Uppsala University
Hashemi V, Hermanns H, Turrini A (2012) On the efficiency of deciding probabilistic automata weak bisimulation. ECEASST, vol 66: 66
Helgason RV, Kennington JL (1995) Primal simplex algorithms for minimum cost network flows. In: Network models. Handbooks in operations research and management science, vol 7, chapter 2. Elsevier, Amsterdam, pp 85–113
Hermanns H, Katoen J-P (2000) Automated compositional Markov chain generation for a plain-old telephone system. Sci Comput Program 36(1): 97–127
Hochbaum DS, Naor JS (1994) Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J Comput 23(6): 1179–1192
Jonsson B, Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS, pp 266–277
Jones WB, Thron WB (1980) Continued fractions: analytic theory and applications. In: Encyclopedia of mathematics and its applications. Addison-Wesley, New York
Karmarkar N (1984) A new polynomial-time algorithm for linear programming. Combinatorica 4(4): 373–395
Khachyan LG (1979) A polynomial algorithm in linear programming. Sov Math Doklady 20(1): 191–194
Katoen J-P, Kemna T, Zapreev IS, Jansen DN (2007) Bisimulation minimisation mostly speeds up probabilistic model checking. In: TACAS. LNCS, vol 4424, pp 76–92
Klee V, Minty GJ (1972) How good is the simplex algorithm? In: Inequalities, vol III, pp 159–175. Defense Technical Information Center, USA
Krimm J-P, Mounier L (2000) Compositional state space generation with partial order reductions for asynchronous communicating systems. In: TACAS. LNCS, vol 1785, pp 266–282
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV. LNCS, vol 6806, pp 585–591
Kanellakis PC, Smolka SA (1990) CCS expressions, finite state processes, and three problems of equivalence. I&C. 86(1):43–68
LpSolve mixed integer linear programming solver. http://lpsolve.sourceforge.net.
Milner R (1989) Communication and concurrency. Prentice-Hall International, Englewood Cliffs
Morrison DR, Sauppe JJ, Jacobson SH (2011) A network simplex algorithm for the equal flow problem on a generalized network. INFORMS J Comput 25(1): 2–12
Morrison DR, Sauppe JJ, Jacobson SH (2013) An algorithm to solve the proportional network flow problem. Optim Lett 8(3): 801–809
Philippou A, Lee I, Sokolsky O (2000) Weak bisimulation for probabilistic systems. In: CONCUR. LNCS, vol 1877, pp 334–349
PRISM model checker. http://www.prismmodelchecker.org/
Parma A, Segala R (2004) Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST, pp 294–303
Paige R, Tarjan RE (1987) Three partition refinement algorithms. SIAM J Comput 16(6): 973–989
Pulat PS (1989) A decomposition algorithm to determine the maximum flow in a generalized network. Comput Oper Res 16: 161–172
Schrijver A (2003) Combinatorial optimization: polyhedra and efficiency. In: Algorithms and combinatorics, vol 24. Springer, Berlin
Segala R (1995) Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT
Segala R (2006) Probability and nondeterminism in operational models of concurrency. In: CONCUR. LNCS, vol 4137, pp 64–78
Shamir R (1987) The efficiency of the simplex method: a survey. Manag Sci 33(3): 301–334
Segala R, Lynch NA (1995) Probabilistic simulations for probabilistic processes. Nordic J Comput 2(2): 250–273
Turrini A, Hermanns H (2015) Polynomial time decision algorithms for probabilistic automata. I&C 244:134–171
Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp 327–338
Vazirani VV (2004) Approximation algorithms. Springer, Berlin
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by Joachim Parrow
Rights and permissions
About this article
Cite this article
Ferrer Fioriti, L.M., Hashemi, V., Hermanns, H. et al. Deciding probabilistic automata weak bisimulation: theory and practice. Form Asp Comp 28, 109–143 (2016). https://doi.org/10.1007/s00165-016-0356-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0356-4