Compositional Model Checking of product-form CTMCs

Product form Markov chains are a class of compositional Markovian models that can be proved to benefit from a decomposed solution of the steady-state distribution (i.e. the steady-state distribution is given by the product of the components' steady-state distributions). In this paper we focus on the Boucherie product processes, a specific class of product form Continuous Time Markov Chains. We show that the compositional constraints that lead to the product form result in that class, can be exploited in the model checking problem as well, leading to a decomposed semantics for a fragment of the Continuous Stochastic Logic.