Abstract
Model checking of technical systems is a common and demanding task. The behavior of such systems can often be characterized using hybrid automata, leading to verification problems within the first-order logic over the reals. The applicability of logic-based formalisms to a wider range of systems has recently been increased by introducing quantifiers into satisfiability modulo theory (SMT) approaches to solve such problems, especially randomized quantifiers, resulting in stochastic satisfiability modulo theory (SSMT). These quantifiers combine non-determinism and stochasticity, thereby allowing to represent models such as Markov decision processes. While algorithms for exact model checking in this setting exist, their scalability is limited due to the computational complexity which increases with the number of quantified variables. Additionally, these methods become infeasible if the domain of the quantified variables, randomized variables in particular, becomes too large or even infinite. In this paper, we present an approximation algorithm based on confidence intervals obtained from sampling which allow for an explicit trade-off between accuracy and computational effort. Although the algorithm gives only approximate results in terms of confidence intervals, it is still guaranteed to converge to the exact solution. To further increase the performance of the algorithm, we adopt search strategies based on the upper bound confidence algorithm UCB, originally used to solve a similar problem, the multi-armed bandit. Preliminary results show that the proposed algorithm can improve the performance in comparison to existing SSMT solvers, especially in the presence of many randomized quantified variables.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Groote, J., van Vlijmen, S., Koorn, J.: The safety guaranteeing system at station hoorn-kersenboogerd. In: Proceedings of the Tenth Annual Conference on Systems Integrity, Software Safety and Process Security, Computer Assurance, COMPASS 1995, pp. 57–68. IEEE (1995)
Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. Electronic Notes in Theoretical Computer Science 119(2), 17–32 (2005)
Fränzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design 30(3), 179–198 (2007)
Teige, T., Eggers, A., Fränzle, M.: Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. Nonlinear Analysis: Hybrid Systems (2010)
Robbins, H.: Some aspects of the sequential design of experiments. Bulletin of the American Mathematical Society 58(5), 527–536 (1952)
Auer, P., Cesa-Bianchi, N., Fischer, P.: Finite-time analysis of the multiarmed bandit problem. Machine Learning 47(2), 235–256 (2002)
Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1(3-4), 209–236 (2007)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)
Sen, K., Viswanathan, M., Agha, G.: Statistical Model Checking of Black-Box Probabilistic Systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)
Younes, H., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204(9), 1368–1409 (2006)
Younes, H.L.S.: Ymer: A Statistical Model Checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for Statistical Model Checking of Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical Model Checking for Networks of Priced Timed Automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011)
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 243–252. ACM, Stockholm (2010)
Bubeck, S., Munos, R., Stoltz, G., Szepesvári, C.: X-armed bandits. Journal of Machine Learning Research 12, 1655–1695 (2011)
Hoeffding, W.: Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association, 13–30 (1963)
Kocsis, L., Szepesvári, C.: Bandit Based Monte-Carlo Planning. In: Fürnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp. 282–293. Springer, Heidelberg (2006)
Szepesvári, C.: In: Reinforcement Learning Algorithms for MDPs. John Wiley & Sons, Inc. (2010)
Serfling, R.J.: Probability inequalities for the sum in sampling without replacement. The Annals of Statistics 2(1), 39–48 (1974)
Srinivas, N., Krause, A., Kakade, S., Seeger, M.: Gaussian process optimization in the bandit setting: No regret and experimental design. In: Fürnkranz, J., Joachims, T. (eds.) Proceedings of the 27th International Conference on Machine Learning (ICML 2010), pp. 1015–1022. Omnipress, Haifa (2010)
Littman, M.L., Majercik, S.M., Pitassi, T.: Stochastic boolean satisfiability. Journal of Automated Reasoning 27(3), 251–296 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ellen, C., Gerwinn, S., Fränzle, M. (2012). Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33365-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-33365-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33364-4
Online ISBN: 978-3-642-33365-1
eBook Packages: Computer ScienceComputer Science (R0)