×

Deciding probabilistic automata weak bisimulation: theory and practice. (English) Zbl 1335.68117


MSC:

68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

z3; lp_solve; GLPK; PRISM; SMT-LIB
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arora S, Hazan E, Kale S (2012) The multiplicative weights update method: a meta-algorithm and applications. Theory Comput 8: 121-164 · Zbl 1283.68414 · doi:10.4086/toc.2012.v008a006
[2] Ahuja RK, Magnanti TJ, Orlin JB (1993) Network flows: theory, algorithms, and applications. Prentice Hall, New York · Zbl 1201.90001
[3] Anstreicher KM (1999) Linear programming in \[{\mathcal{O}(\frac{n^3}{{\rm \ln} n} L)}O\](n3lnnL) operations. SIAM J. Optim. 9(4): 803-812 · Zbl 0955.90085 · doi:10.1137/S1052623497323194
[4] Beling PA (2001) Exact algorithms for linear programming over algebraic extensions. Algorithmica 31(4): 459-478 · Zbl 1093.90024 · doi:10.1007/s00453-001-0049-z
[5] 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 · Zbl 1254.90269 · doi:10.1007/s11590-011-0356-5
[6] 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 · doi:10.1109/TSE.2008.102
[7] Blum L, Shub M, Smale M (1989) On a theory of computation and complexity over the real numbers; \[{NP}\] NP-completeness, recursive functions and universal machines. Bull Am Math Soc 21(1): 1-46 · Zbl 0681.03020 · doi:10.1090/S0273-0979-1989-15750-9
[8] Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. In SMT
[9] Bertsimas D, Tsitsiklis JN (1997) Introduction to linear optimization. Athena Scientific, Belmont
[10] Calvete HI (2002) Network simplex algorithm for the general equal flow problem. Eur J Oper Res 150(3): 585-600 · Zbl 1033.90010 · doi:10.1016/S0377-2217(02)00505-2
[11] Chehaibar G, Garavel H, Mounier L, Tawbi N, Zulian F (1996) Specification and verification of the \[{{\rm PowerScale^{registered}}}\] PowerScaleregistered bus arbitration protocol: an industrial experiment with LOTOS. In: FORTE, pp 435-450
[12] Crouzen P, Hermanns H (2010) Aggregation ordering for massively compositional models. In: ACSD, pp 171-180,
[13] 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 · Zbl 1242.68005
[14] 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 · Zbl 1288.94127
[15] Crouzen P, Lang F (2011) Smart reduction. In FASE. LNCS, vol 6603, pp 111-126 · Zbl 0839.68067
[16] Cattani S, Segala R (2002) Decision algorithms for probabilistic bisimulation. In: CONCUR of LNCS, vol 2421, pp 371-385 · Zbl 1012.68127
[17] Deng Y (2005) Axiomatisations and types for probabilistic and mobile processes. PhD thesis, École des Mines de Paris
[18] Derman C (1970) Finite state markovian decision processes. Academic Press, Inc, New York · Zbl 0262.90001
[19] Mendonça de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS. LNCS, vol 4963, pp 337-340
[20] 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 · Zbl 1381.68115
[21] Eisentraut C, Hermanns H, Zhang L (2010) Concurrency and composition in a stochastic world. In: CONCUR. LNCS, vol 6269, pp 21-39 · Zbl 1287.68132
[22] Eisentraut C, Hermanns H, Zhang L (2010) On probabilistic automata in continuous time. In: LICS, pp 342-351 · Zbl 0654.68072
[23] 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 · Zbl 1426.68183
[24] GNU linear programming kit. http://www.gnu.org/software/glpk/.
[25] Graf S, Steffen B, Lüttgen G (1996) Compositional minimisation of finite state systems using interface specifications. Formal Asp Comput 8(5): 607-616 · Zbl 0860.68067 · doi:10.1007/BF01211911
[26] Hansson HA (1991) Time and probability in formal design of distributed systems. PhD thesis, Uppsala University · Zbl 0674.90023
[27] Hashemi V, Hermanns H, Turrini A (2012) On the efficiency of deciding probabilistic automata weak bisimulation. ECEASST, vol 66: 66
[28] 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 · Zbl 0839.90045
[29] Hermanns H, Katoen J-P (2000) Automated compositional Markov chain generation for a plain-old telephone system. Sci Comput Program 36(1): 97-127 · Zbl 0941.68649 · doi:10.1016/S0167-6423(99)00019-2
[30] 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 · Zbl 0831.90089 · doi:10.1137/S0097539793251876
[31] Jonsson B, Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS, pp 266-277
[32] Jones, WB; Thron, WB, Continued fractions: analytic theory and applications (1980), New York · Zbl 0445.30003
[33] Karmarkar N (1984) A new polynomial-time algorithm for linear programming. Combinatorica 4(4): 373-395 · Zbl 0557.90065 · doi:10.1007/BF02579150
[34] Khachyan LG (1979) A polynomial algorithm in linear programming. Sov Math Doklady 20(1): 191-194 · Zbl 0409.90079
[35] 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 · Zbl 1186.68296
[36] Klee V, Minty GJ (1972) How good is the simplex algorithm? In: Inequalities, vol III, pp 159-175. Defense Technical Information Center, USA · Zbl 0297.90047
[37] 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 · Zbl 0960.68119
[38] Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV. LNCS, vol 6806, pp 585-591
[39] Kanellakis PC, Smolka SA (1990) CCS expressions, finite state processes, and three problems of equivalence. I&C. 86(1):43-68 · Zbl 0705.68063
[40] LpSolve mixed integer linear programming solver. http://lpsolve.sourceforge.net.
[41] Milner R (1989) Communication and concurrency. Prentice-Hall International, Englewood Cliffs · Zbl 0683.68008
[42] 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 · doi:10.1287/ijoc.1110.0485
[43] Morrison DR, Sauppe JJ, Jacobson SH (2013) An algorithm to solve the proportional network flow problem. Optim Lett 8(3): 801-809 · Zbl 1292.90304 · doi:10.1007/s11590-013-0634-5
[44] Philippou A, Lee I, Sokolsky O (2000) Weak bisimulation for probabilistic systems. In: CONCUR. LNCS, vol 1877, pp 334-349 · Zbl 0999.68146
[45] PRISM model checker. http://www.prismmodelchecker.org/ · Zbl 1047.68533
[46] Parma A, Segala R (2004) Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST, pp 294-303
[47] Paige R, Tarjan RE (1987) Three partition refinement algorithms. SIAM J Comput 16(6): 973-989 · Zbl 0654.68072 · doi:10.1137/0216062
[48] Pulat PS (1989) A decomposition algorithm to determine the maximum flow in a generalized network. Comput Oper Res 16: 161-172 · Zbl 0674.90023 · doi:10.1016/0305-0548(89)90017-8
[49] Schrijver, A., Combinatorial optimization: polyhedra and efficiency (2003), Berlin · Zbl 1041.90001
[50] Segala R (1995) Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT
[51] Segala R (2006) Probability and nondeterminism in operational models of concurrency. In: CONCUR. LNCS, vol 4137, pp 64-78 · Zbl 1151.68553
[52] Shamir R (1987) The efficiency of the simplex method: a survey. Manag Sci 33(3): 301-334 · Zbl 0612.90081 · doi:10.1287/mnsc.33.3.301
[53] Segala R, Lynch NA (1995) Probabilistic simulations for probabilistic processes. Nordic J Comput 2(2): 250-273 · Zbl 0839.68067
[54] Turrini A, Hermanns H (2015) Polynomial time decision algorithms for probabilistic automata. I&C 244:134-171 · Zbl 1329.68168
[55] Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp 327-338
[56] Vazirani VV (2004) Approximation algorithms. Springer, Berlin
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.