PT Unknown
AU Della Penna, G
   Intrigila, B
   Melatti, I
   Tronci, E
   Venturini Zilli, M
TI Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier
SE Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings
PY 2003
BP 58
EP 71
VL 2841
DI 10.1007/978-3-540-45208-9_6
AB Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach.
ER