2011/07/06 by Joseph Assouramou, Josée Desharnais
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.57.8
published as EPTCS 57, 2011, pp. 104-119 · In Proceedings QAPL 2011, arXiv:1107.0746
arxiv created 2011/07/06 · arxiv updated 2011/07/07
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.