@article{KWIATKOWSKA2006305,
    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. [1] 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.},
    Author = {Kwiatkowska, M. and Norman, G. and Pacheco, A.},
    File = {Model checking expected time and expected reward formulae with random time bounds - 1-s2.0-0898122105004682-main - a.pdf},
    ISSN = {0898-1221},
    Journal = {Computers \& Mathematics with Applications},
    Keywords = {Continuous time Markov chains, Continuous stochastic logic, Expected time operator, Expected reward operator, Markov reward processes, Mixed Poisson expected sojourn times, Uniformisation},
    Note = {Stochastic Risk Modelling for Finance, Insurance, Production and Reliability},
    Number = {2},
    Pages = {305-316},
    Title = {Model checking expected time and expected reward formulae with random time bounds},
    URL = {https://www.sciencedirect.com/science/article/pii/0898122105004682},
    Volume = {51},
    Year = {2006},
    bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/0898122105004682},
    bdsk-url-2 = {https://doi.org/10.1016/j.camwa.2005.11.016},
    date-added = {2022-12-28 10:18:02 +0100},
    date-modified = {2022-12-28 10:18:02 +0100},
    doi = {10.1016/j.camwa.2005.11.016}
}

@article{KWIATKOWSKA2006305, 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. [1] 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.}, Author = {Kwiatkowska, M. and Norman, G. and Pacheco, A.}, File = {Model checking expected time and expected reward formulae with random time bounds - 1-s2.0-0898122105004682-main - a.pdf}, ISSN = {0898-1221}, Journal = {Computers \& Mathematics with Applications}, Keywords = {Continuous time Markov chains, Continuous stochastic logic, Expected time operator, Expected reward operator, Markov reward processes, Mixed Poisson expected sojourn times, Uniformisation}, Note = {Stochastic Risk Modelling for Finance, Insurance, Production and Reliability}, Number = {2}, Pages = {305-316}, Title = {Model checking expected time and expected reward formulae with random time bounds}, URL = {https://www.sciencedirect.com/science/article/pii/0898122105004682}, Volume = {51}, Year = {2006}, bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/0898122105004682}, bdsk-url-2 = {https://doi.org/10.1016/j.camwa.2005.11.016}, date-added = {2022-12-28 10:18:02 +0100}, date-modified = {2022-12-28 10:18:02 +0100}, doi = {10.1016/j.camwa.2005.11.016} }