Higher-Order Approximations for Verification of Stochastic Hybrid Systems

摘要: 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 higher-order function approximation, for efficient computation solutions with explicit bounds error. Approximation error related to approximations can be substantially lower than those piece-wise constant (zeroth-order) known in literature and, unlike latter, display convergence time a finite value. Furthermore, approximation procedures, which depend partitioning space, lead partition cardinality ones. is first presented Euclidean spaces and thereafter extended hybrid characterizing models Stochastic Hybrid Systems.