Notes:
The original publication is available at www.springerlink.com.

Abstract.
Continuous Time Markov Chains (CTMCs) are widely used as the underlying
stochastic process in performance and dependability analysis. Model
checking of CTMCs against Continuous Stochastic Logic (CSL) has
been investigated previously by a number of authors [2, 4, 13].
CSL contains a timebounded until operator that allows one to express
properties such as "the probability of 3 servers becoming faulty within
7.01 seconds is at most 0.1".
In this paper we extend CSL with a random timebounded until operator,
where the time bound is given by a random variable instead of a fixed
realvalued time (or interval).
With the help of such an operator we can state that
the probability of reaching a set of goal states within some
generally distributed delay while passing only through states that satisfy
a certain property is at most (at least) some probability threshold.
In addition, certain transient properties of
systems which contain general distributions can be expressed with the
extended logic.
We extend the efficient model checking
of CTMCs against the logic CSL developed in [13]
to cater for the new operator.
Our method involves precomputing a family of coefficients for a range of
random variables which includes Pareto, uniform and gamma
distributions, but otherwise carries the same computational cost as
that for ordinary timebounded until in [13].
We implement the algorithms in Matlab and evaluate them by
means of a queueing system example.
