×

zbMATH — the first resource for mathematics

Abstract model repair for probabilistic systems. (English) Zbl 1388.68185
Summary: Given a Discrete Time Markov Chain \(M\) and a probabilistic temporal logic formula \(\phi\), where \(M\) violates \(\phi\), the problem of Model Repair is to obtain a new model \(M^\prime\), such that \(M^\prime\) satisfies \(\phi\). Additionally, the changes made to \(M\) in order to obtain \(M^\prime\) should be minimum with respect to all such \(M^\prime\). The state explosion problem makes the repair of large probabilistic systems almost infeasible. In this paper, we use the abstraction of Discrete Time Markov Chains in order to speed-up the process of model repair for temporal logic reachability properties. We present a framework based on abstraction and refinement, which reduces the state space of the probabilistic system to repair at the price of obtaining an approximate solution. A metric space is defined over the set of DTMCs, in order to measure the differences between the initial and the repaired models. For the repair, we introduce an algorithm and we discuss its important properties, such as soundness and complexity. As a proof of concept, we provide experimental results for probabilistic systems with diverse structures of state spaces, including the well-known Craps game, the IPv4 Zeroconf protocol, a message authentication protocol and the gambler’s ruin model.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
60J20 Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clarke, E. M.; Emerson, E. A.; Sifakis, J., Model checking: algorithmic verification and debugging, Commun. ACM, 52, 11, 74-84, (2009)
[2] Bartocci, E.; Grosu, R.; Katsaros, P.; Ramakrishnan, C. R.; Smolka, S. A., Model repair for probabilistic systems, (Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software, TACAS’11/ETAPS’11, (2011), Springer-Verlag Berlin, Heidelberg), 326-340 · Zbl 1316.68070
[3] Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, ACM Trans. Program. Lang. Syst., 16, 1512-1542, (1994)
[4] Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S.; Probst, D., Property preserving abstractions for the verification of concurrent systems, Form. Methods Syst. Des., 6, 11-44, (1995) · Zbl 0829.68053
[5] Godefroid, P.; Huth, M.; Jagadeesan, R., Abstraction-based model checking using modal transition systems, (Proceedings of the 12th International Conference on Concurrency Theory, CONCUR ’01, (2001), Springer-Verlag London, UK), 426-440 · Zbl 1006.68077
[6] Chatzieleftheriou, G.; Bonakdarpour, B.; Smolka, S. A.; Katsaros, P., Abstract model repair, (Proceedings of the 4th International Conference on NASA Formal Methods, (2012), Springer-Verlag), 341-355
[7] Chatzieleftheriou, G.; Bonakdarpour, B.; Katsaros, P.; Smolka, S. A., Abstract model repair, Log. Methods Comput. Sci., 11, 3, (2015) · Zbl 1448.68292
[8] Katoen, J.-P.; Klink, D.; Leucker, M.; Wolf, V., Three-valued abstraction for probabilistic systems, J. Log. Algebraic Program., 81, 4, 356-389, (2012) · Zbl 1277.68219
[9] Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic cegar, (International Conference on Computer Aided Verification, (2008), Springer), 162-175 · Zbl 1155.68438
[10] Kattenbelt, M.; Kwiatkowska, M.; Norman, G.; Parker, D., Abstraction refinement for probabilistic software, (International Workshop on Verification, Model Checking, and Abstract Interpretation, (2009), Springer), 182-197 · Zbl 1206.68090
[11] Kattenbelt, M.; Kwiatkowska, M.; Norman, G.; Parker, D., A game-based abstraction-refinement framework for Markov decision processes, Form. Methods Syst. Des., 36, 3, 246-280, (2010) · Zbl 1233.90276
[12] D’argenio, P. R.; Jeannet, B.; Jensen, H. E.; Larsen, K. G., Reachability analysis of probabilistic systems by successive refinements, (Process Algebra and Probabilistic Methods. Performance Modelling and Verification, (2001), Springer), 39-56 · Zbl 1007.68131
[13] Komuravelli, A.; Păsăreanu, C. S.; Clarke, E. M., Assume-guarantee abstraction refinement for probabilistic systems, (International Conference on Computer Aided Verification, (2012), Springer), 310-326
[14] Chadha, R.; Viswanathan, M., A counterexample-guided abstraction-refinement framework for Markov decision processes, ACM Trans. Comput. Log., 12, 1, 1, (2010) · Zbl 1351.68154
[15] Vavasis, S. A., Quadratic programming is in np, Inf. Process. Lett., 36, 2, 73-77, (1990) · Zbl 0719.90052
[16] Boggs, P. T.; Tolle, J. W., Sequential quadratic programming, Acta Numer., 4, 1-51, (1995) · Zbl 0828.65060
[17] Lawrence, C. T.; Tits, A. L., A computationally efficient feasible sequential quadratic programming algorithm, SIAM J. Optim., 11, 4, 1092-1118, (2001) · Zbl 1035.90105
[18] Pathak, S.; Ábrahám, E.; Jansen, N.; Tacchella, A.; Katoen, J.-P., A greedy approach for the efficient repair of stochastic models, (NASA Formal Methods Symposium, (2015), Springer), 295-309
[19] Kwiatkowska, M.; Norman, G.; Parker, D., Prism 4.0: verification of probabilistic real-time systems, (Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, (2011), Springer-Verlag Berlin, Heidelberg), 585-591
[20] Dehnert, C.; Junges, S.; Katoen, J.; Volk, M., A storm is coming: a modern probabilistic model checker, (Computer Aided Verification - 29th International Conference, Proceedings, Part II, CAV 2017, Heidelberg, Germany, July 24-28, 2017, (2017)), 592-600
[21] (2017), Maple · Zbl 1372.68003
[22] Kwiatkowska, M.; Norman, G.; Parker, D., Stochastic model checking, (SFM’07, (2007), Springer), 220-270 · Zbl 1323.68379
[23] Baier, C.; Katoen, J.-P., Principles of model checking, Representation and Mind Series, (2008), The MIT Press
[24] Kwiatkowska, M.; Norman, G.; Parker, D.; Sproston, J., Performance analysis of probabilistic timed automata using digital clocks, Form. Methods Syst. Des., 29, 33-78, (2006) · Zbl 1105.68063
[25] Filieri, A.; Ghezzi, C.; Tamburrelli, G., Run-time efficient probabilistic model checking, (Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, (2011), ACM New York, NY, USA), 341-350
[26] Chen, T.; Hahn, E. M.; Han, T.; Kwiatkowska, M.; Qu, H.; Zhang, L., Model repair for Markov decision processes, (2013 International Symposium on Theoretical Aspects of Software Engineering, TASE, (2013), IEEE), 85-92
[27] Bartocci, E.; Bortolussi, L.; Nenzi, L.; Sanguinetti, G., System design of stochastic models using robustness of temporal properties, Theor. Comput. Sci., 587, 3-25, (2015) · Zbl 1327.68147
[28] Češka, M.; Pilař, P.; Paoletti, N.; Brim, L.; Kwiatkowska, M., Prism-psy: precise GPU-accelerated parameter synthesis for stochastic systems, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2016), Springer), 367-384
[29] Brim, L.; Češka, M.; Dražan, S.; Šafránek, D., Exploring parameter space of stochastic biochemical systems using quantitative model checking, (Proceedings of the 25th International Conference on Computer Aided Verification, CAV’13, (2013), Springer-Verlag Berlin, Heidelberg), 107-123
[30] Calinescu, R. C.; Ceska, M.; Gerasimou, S.; Kwiatkowska, M.; Paoletti, N., Designing robust software systems through parametric Markov chain synthesis, (IEEE International Conference on Software Architecture, ICSA 2017, (2017), IEEE)
[31] Dehnert, C.; Junges, S.; Jansen, N.; Corzilius, F.; Volk, M.; Bruintjes, H.; Katoen, J.-P.; Abraham, E., Prophesy: a probabilistic parameter synthesis tool, (International Conference on Computer Aided Verification, (2015), Springer), 214-231
[32] Arming, S.; Bartocci, E.; Sokolova, A., SEA-PARAM: exploring schedulers in parametric mdps, (Quantitative Aspects of Programming Languages and Systems, (2017))
[33] Bozzano, M.; Bruintjes, H.; Cimatti, A.; Katoen, J.-P.; Noll, T.; Tonetta, S., Formal methods for aerospace systems, (Cyber-Physical System Design from an Architecture Analysis Viewpoint, (2017), Springer), 133-159
[34] Arcuri, A., Evolutionary repair of faulty software, Appl. Soft Comput., 11, 4, 3494-3514, (2011)
[35] Buccafurri, F.; Eiter, T.; Gottlob, G.; Leone, N., Enhancing model checking in verification by AI techniques, Artif. Intell., 112, 1, 57-104, (1999) · Zbl 0996.68104
[36] Aflaki, S.; Volk, M.; Bonakdarpour, B.; Katoen, J.-P.; Storjohann, A., Automated fine tuning of probabilistic self-stabilizing algorithms, (SRDS, (2017))
[37] Derisavi, S.; Hermanns, H.; Sanders, W. H., Optimal state-space lumping in Markov chains, Inf. Process. Lett., 87, 6, 309-315, (2003) · Zbl 1189.68039
[38] Bacci, G.; Bacci, G.; Larsen, K. G.; Mardare, R., On the metric-based approximate minimization of Markov chains, (Chatzigiannakis, I.; Indyk, P.; Kuhn, F.; Muscholl, A., 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, (2017), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl, Germany), 104:1-104:14
[39] Dehnert, C.; Gebler, D.; Volpato, M.; Jansen, D. N., On abstraction of probabilistic systems, (Advanced Lectures of the International Autumn School on Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, ROCKS 2012, LNCS, vol. 8453, (2014), Springer-Verlag, Inc. New York, NY, USA), 87-116 · Zbl 1426.68167
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.