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 arebounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in . 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φ verifier. We call FHP-Murφ (Finite Horizon Probabilistic Murφ) such extension of the Murφ verifier. We give experimental results comparing FHP-Murφ 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φ 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).

Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M. (2004). Bounded Probabilistic Model Checking with the Murφ Verifier. ??????? it.cilea.surplus.oa.citation.tipologie.CitationProceedings.prensentedAt ??????? Formal Methods in Computer-Aided Design [10.1007/978-3-540-30494-4_16].

Bounded Probabilistic Model Checking with the Murφ Verifier

INTRIGILA, BENEDETTO;
2004-01-01

Abstract

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 arebounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in . 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φ verifier. We call FHP-Murφ (Finite Horizon Probabilistic Murφ) such extension of the Murφ verifier. We give experimental results comparing FHP-Murφ 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φ 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).
Formal Methods in Computer-Aided Design
Rilevanza internazionale
contributo
2004
Settore INF/01 - INFORMATICA
English
probabilistic systems, sysstem verification, probabilistic model checking
Intervento a convegno
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M. (2004). Bounded Probabilistic Model Checking with the Murφ Verifier. ??????? it.cilea.surplus.oa.citation.tipologie.CitationProceedings.prensentedAt ??????? Formal Methods in Computer-Aided Design [10.1007/978-3-540-30494-4_16].
Della Penna, G; Intrigila, B; Melatti, I; Tronci, E; Zilli, M
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/30789
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact