Abstract
This work investigates the approximate verification of probabilistic specifications expressed as any non-nested PCTL formula over Markov processes on general state spaces. The contribution puts forward new algorithms, based on higher-order function approximation, for the efficient computation of approximate solutions with explicit bounds on the error. Approximation error related to higher-order approximations can be substantially lower than those for piece-wise constant (zeroth-order) approximations known in the literature and, unlike the latter, can display convergence in time to a finite value. Furthermore, higher-order approximation procedures, which depend on the partitioning of the state space, can lead to lower partition cardinality than the related piece-wise constant ones. The work is first presented for Markov processes over Euclidean spaces and thereafter extended to hybrid spaces characterizing models known as Stochastic Hybrid Systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abate, A., Katoen, J.-P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. European Journal of Control (6), 624–641 (2010)
Abate, A., Katoen, J.-P., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: ACM Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, Chicago, IL, pp. 83–92 (April 2011)
Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
Bertsekas, D.P., Shreve, S.E.: Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific (1996)
Blom, H.A.P., Lygeros, J. (eds.): Stochastic Hybrid Systems: Theory and Safety Critical Applications. LNCIS, vol. 337. Springer, Heidelberg (2006)
Cassandras, C.G., Lygeros, J. (eds.): Stochastic Hybrid Systems. Control Engineering, vol. 24. CRC Press, Boca Raton (2006)
Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive gridding for abstraction and verification of stochastic hybrid systems. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems, Aachen, DE, pp. 59–69 (September 2011)
Esmaeil Zadeh Soudjani, S., Abate, A.: Probabilistic invariance of mixed deterministic-stochastic dynamical systems. In: ACM Proceedings of the 15th International Conference on Hybrid Systems: Computation and Control, Beijing, PRC, pp. 207–216 (April 2012)
Hernández-Lerma, O., Lasserre, J.B.: Discrete-time Markov control processes. Applications of Mathematics, vol. 30. Springer, New York (1996)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: IEEE Proceedings of the International Conference on Quantitative Evaluation of Systems, Los Alamos, CA, USA, pp. 243–244 (2005)
Mastroianni, G., Milovanovic, G.V.: Interpolation Processes: Basic Theory and Applications. Springer (2008)
Meyn, S.P., Tweedie, R.L.: Markov chains and stochastic stability. Springer (1993)
Ramponi, F., Chatterjee, D., Summers, S., Lygeros, J.: On the connections between PCTL and dynamic programming. In: ACM Proceedings of the 13th International Conference on Hybrid Systems: Computation and Control, pp. 253–262 (April 2010)
Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica 46(12), 1951–1961 (2010)
Tkachev, I., Abate, A.: Regularization of Bellman equations for infinite-horizon probabilistic properties. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, Beijing, PRC, pp. 227–236 (April 2012)
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
Esmaeil Zadeh Soudjani, S., Abate, A. (2012). Higher-Order Approximations for Verification of Stochastic Hybrid Systems. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-33386-6_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33385-9
Online ISBN: 978-3-642-33386-6
eBook Packages: Computer ScienceComputer Science (R0)