Beyond Memoryless Distributions: Model Checking Semi-Markov Chains

Abstract. Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.

• Type: Conference
• Year: 2001
• Where: PAPM
• Authors: Gabriel G. Infante López, Holger Hermanns, Joost-Pieter Katoen
• Keywords: Holding Time Distributions, Mathematics, Negative Exponential Distributions, PAPM 2001, State Holding Times