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. © 2012 Springer-Verlag.
CITATION STYLE
Esmaeil Zadeh Soudjani, S., & Abate, A. (2012). Higher-order approximations for verification of stochastic hybrid systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7561 LNCS, pp. 416–434). https://doi.org/10.1007/978-3-642-33386-6_32
Mendeley helps you to discover research relevant for your work.