Compositional Bisimulation Minimization for Interval Markov Decision Processes

详细信息    查看全文

• 关键词：Markov decision process ; Interval MDP ; Compositionality ; Bisimulation ; Complexity
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9618
• 期：1
• 页码：114-126
• 全文大小：249 KB
• 参考文献：1.Balas, E.: Disjunctive programming: properties of the convex hull of feasible points. Discrete Appl. Math. 89(1), 3–44 (1998)CrossRef MathSciNet MATH
  2.Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013)CrossRef
  3.Billingsley, P.: Probability and Measure. John Wiley and Sons, New York (1979)MATH
  4.Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)CrossRef
  5.Cattani, S., Segala, R., Kwiatkowska, M., Norman, G.: Stochastic transition systems for continuous state spaces and non-determinism. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 125–139. Springer, Heidelberg (2005)CrossRef
  6.Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking \(\omega \) -regular properties of interval Markov chains. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008)CrossRef
  7.Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the PowerScale\({}^{\textregistered }\) busarbitration protocol: an industrial experiment with LOTOS. In: FORTE, pp. 435–450 (1996)
  8.Chen, T., Han, T., Kwiatkowska, M.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210–216 (2013)CrossRef MathSciNet MATH
  9.Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 204–218. Springer, Heidelberg (2009)CrossRef
  10.Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011)CrossRef
  11.Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Decision problems for interval Markov chains. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 274–285. Springer, Heidelberg (2011)CrossRef
  12.Eirinakis, P., Ruggieri, S., Subramani, K., Wojciechowski, P.: On quantified linear implications. AMAI 71(4), 301–325 (2014)MathSciNet MATH
  13.Garey, M.R., Johnson, D.S.: Computers and Intractability; A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1990)
  14.Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146–161. Springer, Heidelberg (2011)CrossRef
  15.Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)CrossRef MATH
  16.Hashemi, V., Hatefi, H., Krčál, J.: Probabilistic bisimulations for PCTL model checking of interval MDPs. SynCoP EPTCS 145, 19–33 (2014)CrossRef
  17.Hashemi, V., Hermanns, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. ECEASST, 66 (2013)
  18.Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comp. Progr. 36(1), 97–127 (2000)CrossRef MATH
  19.Iancu, D.A., Sharma, M., Sviridenko, M.: Supermodularity and affine policies in dynamic robust optimization. Oper. Res. 61(4), 941–956 (2013)CrossRef MathSciNet MATH
  20.Iyengar, G.N.: Robust dynamic programming. Math. Oper. Res. 30(2), 257–280 (2005)CrossRef MathSciNet MATH
  21.Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277 (1991)
  22.Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990)CrossRef MathSciNet MATH
  23.Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)CrossRef
  24.Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009)CrossRef
  25.Kozine, I., Utkin, L.V.: Interval-valued finite Markov chains. Reliable Comput. 8(2), 97–113 (2002)CrossRef MathSciNet MATH
  26.Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008)
  27.Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRef
  28.Nilim, A., Ghaoui, L.E.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780–798 (2005)CrossRef MathSciNet MATH
  29.Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)CrossRef MathSciNet MATH
  30.Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527–542. Springer, Heidelberg (2013)CrossRef
  31.Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Amsterdam (1998)MATH
  32.Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT (1995)
  33.Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006)CrossRef
  34.Subramani, K.: On the complexities of selected satisfiability and equivalence queries over boolean formulas and inclusion queries over hulls. JAMDS, 2009 (2009)
  35.Turrini, A., Hermanns, H.: Polynomial time decision algorithms for probabilistic automata. Inf. Comput. 244, 134–171 (2015)CrossRef MathSciNet
  36.Vaidya, P.M.: An algorithm for linear programming which requires \({O}(((m+n)n^2) + (m+n)^{1.5})n){L})\) arithmetic operations. Math. Program. 47, 175–201 (1990)CrossRef MathSciNet MATH
  37.Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: CDC, pp. 3372–3379 (2012)
  38.Wu, D., Koutsoukos, X.D.: Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. AI 172(8–9), 945–954 (2008)MathSciNet MATH
  39.Yi, W.: Algebraic reasoning for real-time probabilistic processes with uncertain information. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 680–693. Springer, Heidelberg (1994)CrossRef
  
• 作者单位：Vahid Hashemi (17) (18)
  Holger Hermanns (18)
  Lei Song (19) (20)
  K. Subramani (21)
  Andrea Turrini (20)
  Piotr Wojciechowski (21)
  
  17. Max Planck Institute for Informatics, Saarbrücken, Germany
  18. Department of Computer Science, Saarland University, Saarbrücken, Germany
  19. University of Technology Sydney, Sydney, Australia
  20. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China
  21. LDCSEE, West Virginia University, Morgantown, WV, USA
  
• 丛书名：Language and Automata Theory and Applications
• ISBN：978-3-319-30000-9
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Formal verification of PCTL properties of MDPs with convex uncertainties has been recently investigated by Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDP while preserving PCTL properties it satisfies. We give a compositional reasoning over interval models to understand better the ways how large models with interval uncertainties can be composed. Afterwards, we discuss computational complexity of the bisimulation minimization and show that the problem is coNP-complete. Finally, we show that, under a mild condition, bisimulation can be computed in polynomial time.