Analysis of Non-Linear Probabilistic Hybrid Systems

TL;DR

This paper extends clock and linear phase-portrait approximation techniques to probabilistic hybrid systems, enabling model-checking of complex systems by approximating non-rectangular processes with rectangular probabilistic models.

Contribution

It adapts existing non probabilistic approximation methods to probabilistic hybrid systems, broadening their applicability for system verification.

Findings

Clock approximation applies under certain restrictions.

Linear phase-approximation is unrestricted and simulates the original process.

Conditions for probabilistic processes mirror those of the classic case.

Abstract

This paper shows how to compute, for probabilistic hybrid systems, the clock approximation and linear phase-portrait approximation that have been proposed for non probabilistic processes by Henzinger et al. The techniques permit to define a rectangular probabilistic process from a non rectangular one, hence allowing the model-checking of any class of systems. Clock approximation, which applies under some restrictions, aims at replacing a non rectangular variable by a clock variable. Linear phase-approximation applies without restriction and yields an approximation that simulates the original process. The conditions that we need for probabilistic processes are the same as those for the classic case.