CSL Model Checking for the GreatSPN Tool

CSL is a stochastic temporal logic that has been defined for continuous time Markov chains, and that allows the checking of whether a single state, or a set of states, satisfies a given probabilistic condition defined over states or over a path of states. In this paper we consider the problem of CSL model checking in the context of Generalized Stochastic Petri Nets. We present a translation from Generalized Stochastic Petri Nets to the input formats of two well-known CSL model checkers, namely ETMCC and Prism. The transformation to ETMCC is realized at the Markov Chain level, while that to Prism is defined, as much as possible, at the net level. The translations are applied to a multiserver polling model taken from the literature.