Sequential convex programming for the efficient verification of parametric MDPs. (English) Zbl 1452.68117
Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part II. Berlin: Springer. Lect. Notes Comput. Sci. 10206, 133-150 (2017).
Summary: Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a geometric programming problem. These geometric programs are obtained by convexifying the nonconvex constraints of the original problem. Direct applications of the encodings as nonlinear programs are model repair and parameter synthesis. We demonstrate the scalability and quality of our approach by well-known benchmarks.
For the entire collection see [Zbl 1360.68016].
For the entire collection see [Zbl 1360.68016].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 90C25 | Convex programming |
References:
| [1] | Satia, J.K., Lave Jr., R.E.: Markovian decision processes with uncertain transition probabilities. Oper. Res. 21(3), 728-740 (1973) · Zbl 0286.60038 · doi:10.1287/opre.21.3.728 |
| [2] | Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, p. 375. Academic Press, Cambridge (1976) · Zbl 0395.65004 |
| [3] | Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 15(1), 441-460 (1990) · Zbl 0705.68016 · doi:10.1016/0196-6774(90)90021-6 |
| [4] | Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127-165. Springer, Heidelberg (1994). doi:10.1007/3-540-58085-9_75 · doi:10.1007/3-540-58085-9_75 |
| [5] | Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796-817 (2001) · Zbl 1010.90061 · doi:10.1137/S1052623400366802 |
| [6] | Han, J., Jonker, P.: A system architecture solution for unreliable nanoelectronic devices. IEEE Trans. Nanotechnol. 1, 201-208 (2002) · doi:10.1109/TNANO.2002.807393 |
| [7] | Boyd, S., Kim, S.-J., Vandenberghe, L., Hassibi, A.: A tutorial on geometric programming. Optim. Eng. 8(1), 67 (2007) · Zbl 1178.90270 · doi:10.1007/s11081-007-9001-7 |
| [8] | Boyd, S.: Sequential convex programming. Lecture Notes (2008) |
| [9] | Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS 4(4), 50-65 (2008) · Zbl 1186.68286 |
| [10] | Biegler, L.T., Zavala, V.M.: Large-scale nonlinear programming using IPOPT: an integrating framework for enterprise-wide dynamic optimization. Comput. Chem. Eng. 33(3), 575-582 (2009) · doi:10.1016/j.compchemeng.2008.08.006 |
| [11] | Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660-664. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_56 · doi:10.1007/978-3-642-14295-6_56 |
| [12] | Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3-19 (2010) · doi:10.1007/s10009-010-0146-x |
| [13] | Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326-340. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_30 · Zbl 1316.68070 · doi:10.1007/978-3-642-19835-9_30 |
| [14] | Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112-127. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_11 · Zbl 1315.68177 · doi:10.1007/978-3-642-19835-9_11 |
| [15] | 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). doi:10.1007/978-3-642-22110-1_47 · doi:10.1007/978-3-642-22110-1_47 |
| [16] | Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 317-332. Springer, Heidelberg (2012) · Zbl 1374.68285 · doi:10.1007/978-3-642-33386-6_25 |
| [17] | Jovanović, D., Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339-354. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_27 · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27 |
| [18] | Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203-204. IEEE CS (2012) |
| [19] | Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE, pp. 85-92. IEEE CS (2013) |
| [20] | 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). doi:10.1007/978-3-642-39799-8_35 · Zbl 1435.68202 · doi:10.1007/978-3-642-39799-8_35 |
| [21] | Češka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86-98. Springer, Heidelberg (2014). doi:10.1007/978-3-319-12982-2_7 · Zbl 1373.92038 · doi:10.1007/978-3-319-12982-2_7 |
| [22] | Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312-317. Springer, Heidelberg (2014). doi:10.1007/978-3-319-06410-9_22 · doi:10.1007/978-3-319-06410-9_22 |
| [23] | Jansen, N., Corzilius, F., Volk, M., Wimmer, R., Ábrahám, E., Katoen, J.-P., Becker, B.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 404-420. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10696-0_31 · doi:10.1007/978-3-319-10696-0_31 |
| [24] | Su, G., Rosenblum, D.S.: Nested reachability approximation for discrete-time Markov chains with univariate parameters. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 364-379. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11936-6_26 · Zbl 1448.68320 · doi:10.1007/978-3-319-11936-6_26 |
| [25] | Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., Ábrahám, E.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214-231. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_13 · doi:10.1007/978-3-319-21690-4_13 |
| [26] | PARAM Website (2015). http://depend.cs.uni-sb.de/tools/param/ |
| [27] | Pathak, S., Ábrahám, E., Jansen, N., Tacchella, A., Katoen, J.-P.: A greedy approach for the efficient repair of stochastic models. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 295-309. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17524-9_21 · doi:10.1007/978-3-319-17524-9_21 |
| [28] | Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time Markov chains. Inf. Comput. 247, 235-253 (2016) · Zbl 1336.68162 · doi:10.1016/j.ic.2016.01.004 |
| [29] | Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: The probabilistic model checker storm (extended abstract). CoRR, abs/1610.08713 (2016) |
| [30] | Delgado, K.V., de Barros, L.N., Dias, D.B., Sanner, S.: Real-time dynamic programming for Markov decision processes with imprecise probabilities. Artif. Intell. 230, 192-223 (2016) · Zbl 1344.68246 · doi:10.1016/j.artint.2015.09.005 |
| [31] | Katoen, J.-P.: The probabilistic model checking landscape. In: IEEE Symposium on Logic In Computer Science (LICS). ACM (2016) · Zbl 1401.68201 |
| [32] | Long, F., Rinard, M.: Automatic patch generation by learning correct code. In: POPL, pp. 298-312. ACM (2016) |
| [33] | Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50-67. Springer, Heidelberg (2016). doi:10.1007/978-3-319-46520-3_4 · Zbl 1398.68346 · doi:10.1007/978-3-319-46520-3_4 |
| [34] | Su, G., Rosenblum, D.S., Tamburrelli, G.: Reliability of run-time QOS evaluation using parametric model checking. In: ICSE. ACM (2016, to appear) |
| [35] | MOSEK ApS: The MOSEK optimization toolbox for PYTHON. Version 7.1 (Revision 60) (2015) |
| [36] | Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076 |
| [37] | Bertsekas, D.P.: Nonlinear Programming. Athena Scientific, Belmont (1999) · Zbl 1015.90077 |
| [38] | Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004) · Zbl 1058.90049 · doi:10.1017/CBO9780511804441 |
| [39] | Thrun, S. |
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.
