| Home | << 1 >> |
|
| Record | |||||
|---|---|---|---|---|---|
| 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 | 8 | Issue | 4 | Pages | 397-409 |
| Keywords | |||||
| 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). | ||||
| Address | |||||
| 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 | |||||