Output details

Approximate model checking of stochastic hybrid systems

<11>

This work relates a problem in control (probabilistic invariance characterised via Bellman recursions), and a known specification (bounded until) in PCTL logic. This new connection allows leveraging probabilistic model checking algorithms for the computation of probabilistic invariance for stochastic models over continuous spaces. Employing a formal discretization approach with quantified explicit bounds on the approximation error, this approach represents a formal and quantitative abstraction technique applicable to any uncountable state-space model.

These results have spurred further work on abstractions, on practical computability (adaptive and sequential approximations), and on more general properties (covering full PCTL and temporal specifications over automata).