Model Checking Multivariate State Rewards

Bo Friis Nielsen, Flemming Nielson, Hanne Riis Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    We consider continuous stochastic logics with state rewards that are interpreted over continuous time Markov chains. We show how results from multivariate phase type distributions can be used to obtain higher-order moments for multivariate state rewards (including covariance). We also generalise the treatment of eventuality to unbounded path formulae. For all extensions we show how to obtain closed form definitions that are straightforward to implement and we illustrate our development on a small example.
    Original languageEnglish
    Title of host publicationSeventh International Conference on the Quantitative Evaluation of Systems
    Pages7-16
    ISBN (Print)978-0-7695-4188-4
    DOIs
    Publication statusE-pub ahead of print - 2010
    EventSeventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, VA, USA September 15-September 18 -
    Duration: 1 Jan 2010 → …

    Conference

    ConferenceSeventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, VA, USA September 15-September 18
    Period01/01/2010 → …

    Fingerprint Dive into the research topics of 'Model Checking Multivariate State Rewards'. Together they form a unique fingerprint.

    Cite this