TY  - CONF
AU  - Della Penna, Giuseppe
AU  - Intrigila, Benedetto
AU  - Melatti, Igor
AU  - Tronci, Enrico
AU  - Venturini Zilli, Marisa
ED  - Blundo, C.
ED  - Laneve, C.
PY  - 2003
DA  - 2003//
TI  - Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier
BT  - Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings
T3  - Lecture Notes in Computer Science
SP  - 58
EP  - 71
VL  - 2841
PB  - Springer
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.
SN  - 3-540-20216-1
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003b.pdf
UR  - https://doi.org/10.1007/978-3-540-45208-9_6
DO  - 10.1007/978-3-540-45208-9_6
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=90), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - DellaPenna_etal2003
ER  -