Deciding probabilistic automata weak bisimulation: theory and practice

10.4086/toc.2012.v008a006

Ahuja RK, 1993, Network flows: theory, algorithms, and applications

10.1137/S1052623497323194

Beling PA, 2001, Exact algorithms for linear programming over algebraic extensions, Algorithmica, 31, 459, 10.1007/s00453-001-0049-z

Bahçeci U, 2012, A network simplex based algorithm for the minimum cost proportional flow problem with disconnected subnetworks, Optim Lett, 6, 1173, 10.1007/s11590-011-0356-5

10.1109/TSE.2008.102

10.1090/S0273-0979-1989-15750-9

Barrett C Stump A Tinelli C (2010) The SMT-LIB standard: version 2.0. In SMT

10.5555/548834

Calvete HI, 2002, Network simplex algorithm for the general equal flow problem, Eur J Oper Res, 150, 585, 10.1016/S0377-2217(02)00505-2

Chehaibar G Garavel H Mounier L Tawbi N Zulian F (1996) Specification and verification of the PowerScaleregistered 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/.

10.1007/BF01211911

Hansson HA (1991) Time and probability in formal design of distributed systems. PhD thesis Uppsala University

Hashemi V, 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

10.1016/S0167-6423(99)00019-2

10.1137/S0097539793251876

Jonsson B Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS pp 266–277

Jones WB, 1980, In: Encyclopedia of mathematics and its applications.

10.1007/BF02579150

Khachyan LG, 1979, A polynomial algorithm in linear programming, Sov Math Doklady, 20, 191

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

Morrison DR, 2011, A network simplex algorithm for the equal flow problem on a generalized network, INFORMS J Comput, 25, 2, 10.1287/ijoc.1110.0485

Morrison DR, 2013, An algorithm to solve the proportional network flow problem, Optim Lett, 8, 801, 10.1007/s11590-013-0634-5

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

10.1137/0216062

10.1016/0305-0548(89)90017-8

Schrijver A, 2003, In: Algorithms and combinatorics, vol 24.

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, 301, 10.1287/mnsc.33.3.301

Segala R, 1995, Probabilistic simulations for probabilistic processes, Nordic J Comput, 2, 250

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