×

zbMATH — the first resource for mathematics

Smoothed model checking for uncertain continuous-time Markov chains. (English) Zbl 1336.68162
Summary: We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters under mild conditions. This enables us to devise a novel Bayesian statistical algorithm which performs model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on non-trivial case studies show that the approach is accurate and considerably faster than naive parameter exploration with standard statistical model checking methods.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
60G15 Gaussian processes
60J28 Applications of continuous-time Markov processes on discrete state spaces
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (Proc. of Computer Aided Verification, Lect. Notes Comput. Sci., vol. 6806, (2011), Springer), 585-591
[2] Katoen, J.-P.; Khattri, M.; Zapreevt, I. S., A Markov reward model checker, (Proc. of Quantitative Evaluation of Systems, (2005), IEEE Computer Society), 243-244
[3] Gillespie, D. T., Exact stochastic simulation of coupled chemical reactions, J. Phys. Chem., 81, 25, 2340-2361, (1977)
[4] Younes, H. L.; Simmons, R. G., Statistical probabilistic model checking with a focus on time-bounded properties, Inf. Comput., 204, 9, 1368-1409, (2006) · Zbl 1110.68077
[5] Zuliani, P.; Platzer, A.; Clarke, E. M., Bayesian statistical model checking with application to simulink/stateflow verification, (Proc. of Hybrid Systems: Computation and Control, (2010), ACM), 243-252 · Zbl 1361.68154
[6] Opper, M.; Sanguinetti, G., Variational inference for Markov jump processes, (Proc. of Advances in Neural Information Processing Systems, (2007)), 1105-1112
[7] Bartocci, E.; Grosu, R.; Katsaros, P.; Ramakrishnan, C. R.; Smolka, S. A., Model repair for probabilistic systems, (Proc. of Tools and Algorithms for the Construction and Analysis of Systems, Lect. Notes Comput. Sci., vol. 6605, (2011), Springer), 326-340 · Zbl 1316.68070
[8] Andreychenko, A.; Mikeev, L.; Spieler, D.; Wolf, V., Approximate maximum likelihood estimation for stochastic chemical kinetics, EURASIP J. Bioinform. Syst. Biol., 2012, 1, 1-14, (2012)
[9] Bortolussi, L.; Sanguinetti, G., Learning and designing stochastic processes from logical constraints, (Proc. of Quantitative Evaluation of Systems, Lect. Notes Comput. Sci., vol. 8054, (2013), Springer), 89-105
[10] 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
[11] Katoen, J.-P.; Klink, D.; Leucker, M.; Wolf, V., Three-valued abstraction for continuous-time Markov chains, (Proc. of Computer Aided Verification, Lect. Notes Comput. Sci., vol. 4590, (2007)), 311-324 · Zbl 1135.68476
[12] Caillaud, B.; Delahaye, B.; Larsen, K. G.; Legay, A.; Pedersen, M. L.; Wasowski, A., Constraint Markov chains, Theor. Comput. Sci., 412, 34, 4373-4404, (2011) · Zbl 1223.68070
[13] Baier, C.; Hermanns, H.; Katoen, J.-P.; Haverkort, B. R., Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes, Theor. Comput. Sci., 345, 1, 2-26, (2005) · Zbl 1081.90066
[14] Benedikt, M.; Lenhardt, R.; Worrell, J., LTL model checking of interval Markov chains, (Proc. of Tools and Algorithms for the Construction and Analysis of Systems, Lect. Notes Comput. Sci., vol. 7795, (2013)), 32-46 · Zbl 1381.68147
[15] Brim, L.; Češka, M.; Dražan, S.; Šafránek, D., Exploring parameter space of stochastic biochemical systems using quantitative model checking, (Proc. of Computer Aided Verification, Lect. Notes Comput. Sci., vol. 8044, (2013)), 107-123
[16] Češka, M.; Dannenberg, F.; Kwiatkowska, M.; Paoletti, N., Precise parameter synthesis for stochastic biochemical systems, (Proc. of Computational Methods in Systems Biology, Lect. Notes Comput. Sci., vol. 8859, (2014), Springer), 86-98
[17] Spielman, D. A.; Teng, S.-H., Smoothed analysis: an attempt to explain the behavior of algorithms in practice, Commun. ACM, 52, 10, 76-84, (2009)
[18] Durrett, R., Essentials of stochastic processes, (2012), Springer · Zbl 1244.60001
[19] Norris, J. R., Markov chains, Camb. Ser. Stat. Probab. Math., (1997), Cambridge University Press · Zbl 0873.60043
[20] Bortolussi, L.; Hillston, J.; Latella, D.; Massink, M., Continuous approximation of collective systems behaviour: a tutorial, Perform. Eval., 70, 5, 317-349, (2013)
[21] Billingsley, P., Probability and measure, (2012), Wiley Hoboken, N.J. · Zbl 1236.60001
[22] Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, (Proc. of Formal Modelling and Analysis of Timed Systems, Lect. Notes Comput. Sci., vol. 3253, (2004), Springer), 152-166 · Zbl 1109.68518
[23] Chen, T.; Diciolla, M.; Kwiatkowska, M.; Mereacre, A., Time-bounded verification of CTMCs against real-time specifications, (Proc. of Formal Modelling and Analysis of Timed Systems, Lect. Notes Comput. Sci., vol. 6919, (2011), Springer), 26-42 · Zbl 1348.68126
[24] Rasmussen, C. E.; Williams, C. K.I., Gaussian processes for machine learning, (2006), MIT Press · Zbl 1177.68165
[25] Steinwart, I., On the influence of the kernel on the consistency of support vector machines, J. Mach. Learn. Res., 2, 67-93, (2002) · Zbl 1009.68143
[26] Opper, M.; Winther, O., Gaussian processes for classification: mean-field algorithms, Neural Comput., 12, 11, 2655-2684, (2000)
[27] Minka, T. P., Expectation propagation for approximate Bayesian inference, (Proc. of Uncertainty in Artificial Intelligence, (2001), Morgan Kaufmann Publishers Inc.), 362-369
[28] Heskes, T.; Opper, M.; Wiegerinck, W.; Winther, O.; Zoeter, O., Approximate inference techniques with expectation constraints, J. Stat. Mech. Theory Exp., (2005)
[29] Kuss, M.; Rasmussen, C. E., Assessing approximate inference for binary Gaussian process classification, J. Mach. Learn. Res., 6, 1679-1704, (2005) · Zbl 1190.62119
[30] Bortolussi, L.; Milios, D.; Sanguinetti, G., U-check: model checking and parameter synthesis under uncertainty, (Proc. of Quantitative Evaluation of Systems, Lect. Notes Comput. Sci., vol. 9259, (2015)), 89-104
[31] Ciocchetta, F.; Hillston, J., Bio-PEPA: a framework for the modelling and analysis of biological systems, Theor. Comput. Sci., 410, 33-34, 3065-3084, (2009) · Zbl 1173.68041
[32] Bortolussi, L.; Galpin, V.; Hillston, J., Hybrid performance modelling of opportunistic networks, (Proc. of Quantitative Aspects of Programming Languages, (2012)), 106-121
[33] Andersson, H.; Britton, T., Stochastic epidemic models and their statistical analysis, (2000), Springer · Zbl 0951.92021
[34] Haseltine, E. L.; Rawlings, J. B., Approximate simulation of coupled fast and slow reactions for stochastic chemical kinetics, J. Chem. Phys., 117, 15, 6959, (2002)
[35] Elowitz, M.; Levine, A.; Siggia, E.; Swain, P., Stochastic gene expression in a single cell, Science, 297, 5584, 1183-1186, (2002)
[36] Fisher, J.; Henzinger, T., Executable cell biology, Nat. Biotechnol., 25, 11, 1239-1249, (2007)
[37] Kierzek, A. M., STOCKS: stochastic kinetic simulations of biochemical systems with Gillespie algorithm, Bioinformatics, 18, 3, 470-481, (2002)
[38] Daws, C., Symbolic and parametric model checking of discrete-time Markov chains, (Proc. of Theoretical Aspects of Computing, Lect. Notes Comput. Sci., vol. 3407, (2005), Springer), 280-294 · Zbl 1108.68497
[39] Hahn, E. M.; Hermanns, H.; Wachter, B.; Zhang, L., PARAM: a model checker for parametric Markov models, (Proc. of Computer Aided Verification, Lect. Notes Comput. Sci., vol. 6174, (2010), Springer), 660-664
[40] Dehnert, C.; Junges, S.; Jansen, N.; Corzilius, F.; Volk, M.; Bruintjes, H.; Katoen, J.-P.; Ábrahám, E., Prophesy: a probabilistic parameter synthesis tool, (Proc. of Computer Aided Verification, Lect. Notes Comput. Sci., vol. 9206, (2015), Springer), 214-231
[41] Jegourel, C.; Legay, A.; Sedwards, S., Cross-entropy optimisation of importance sampling parameters for statistical model checking, (Proc. of Computer Aided Verification, Lect. Notes Comput. Sci., vol. 7358, (2012)), 327-342
[42] Bartocci, E.; Bortolussi, L.; Sanguinetti, G., Data-driven statistical learning of temporal logic properties, (Proc. of Formal Modelling and Analysis of Timed Systems, Lect. Notes Comput. Sci., vol. 8711, (2014), Springer), 23-37 · Zbl 1448.68371
[43] Legay, A.; Sedwards, S., Statistical abstraction boosts design and test efficiency of evolving critical systems, (Proc. of Leveraging Applications of Formal Methods, Verification and Validation, Technologies for Mastering Change, ISoLA, Lect. Notes Comput. Sci., vol. 8802, (2014)), 4-25
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.