Abstract.
In this paper we extend CSL (Continuous Stochastic Logic) with an expected time and
an expected reward operator, both of which are parameterized by
a random terminal time. With the help of such operators we can
state for example that the expected sojourn time in a set of goal
states within some generally distributed delay is at most (at
least) some time threshold. In addition, certain performance
measures of systems which contain general distributions can be
calculated with the aid of this extended logic. We extend the
efficient model checking of CTMCs against the logic CSL developed
by Katoen et al. to cater for the new
operator. Our method involves precomputing a family of mixed
Poisson expected sojourn time coefficients for a range of random
variables which includes Pareto, uniform and gamma distributions,
but otherwise carries the same computational cost as calculating
CSL until formulae.
|