Analysis of Non-Linear Probabilistic Hybrid Systems

Joseph Assouramou
(Université Laval)
Josée Desharnais
(Université Laval)

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.

In Mieke Massink and Gethin Norman: Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), Saarbrücken, Germany, April 1-3, 2011, Electronic Proceedings in Theoretical Computer Science 57, pp. 104–119.
Published: 4th July 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: