TY - CONF AU - Della Penna, Giuseppe AU - Intrigila, Benedetto AU - Melatti, Igor AU - Tronci, Enrico AU - Venturini Zilli, Marisa ED - Hu, A.J. ED - Martin, A.K. PY - 2004 DA - 2004// TI - Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier BT - Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings T3 - Lecture Notes in Computer Science SP - 214 EP - 229 VL - 3312 PB - Springer AB - In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give 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 effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems). SN - 3-540-23738-0 L1 - http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2004.pdf UR - https://doi.org/10.1007/978-3-540-30494-4_16 DO - 10.1007/978-3-540-30494-4_16 N1 - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=87), last updated on Thu, 22 Nov 2012 14:59:18 +0100 ID - DellaPenna_etal2004 ER -