Compositional Model Checking of product-form CTMCs

Paolo Ballarini and András Horváth

Abstract:

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.
Keywords: Compositional Stochastic Model Checking, Product-form Markov Chains

PDF

[Publications of András Horváth]