|   | 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier Type Journal Article
Year 2006 Publication Int. J. Softw. Tools Technol. Transf. Abbreviated Journal
Volume (down) 8 Issue 4 Pages 397-409
Abstract In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
Corporate Author Thesis
Publisher Springer-Verlag Place of Publication Berlin, Heidelberg Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1433-2779 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimtz06 Serial 78
Permanent link to this record