Model Checking Multivariate State Rewards

Bo Friis Nielsen; Flemming Nielson; Hanne Riis Nielson

doi:10.1109/QEST.2010.10

Model Checking Multivariate State Rewards

Bo Friis Nielsen
, Flemming Nielson
, Hanne Riis Nielson

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Seventh International Conference on the Quantitative Evaluation of Systems
Pages	7-16
ISBN (Print)	978-0-7695-4188-4
DOIs	https://doi.org/10.1109/QEST.2010.10
Publication status	E-pub ahead of print - 2010
Event	7th International Conference on the Quantitative Evaluation of Systems - Williamsburg, United States Duration: 15 Sept 2010 → 18 Sept 2010 Conference number: 7

Conference

Conference	7th International Conference on the Quantitative Evaluation of Systems
Number	7
Country/Territory	United States
City	Williamsburg
Period	15/09/2010 → 18/09/2010

Access to Document

10.1109/QEST.2010.10

http://www.computer.org/portal/web/csdl/doi/10.1109/QEST.2010.10

OpenUrl availability

Full text

Cite this

@inproceedings{b6104a3829d144ce9e7487a04415489e,

title = "Model Checking Multivariate State Rewards",

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.",

author = "Nielsen, \{Bo Friis\} and Flemming Nielson and Nielson, \{Hanne Riis\}",

year = "2010",

doi = "10.1109/QEST.2010.10",

language = "English",

isbn = "978-0-7695-4188-4",

pages = "7--16",

booktitle = "Seventh International Conference on the Quantitative Evaluation of Systems",

note = "7th International Conference on the Quantitative Evaluation of Systems ; Conference date: 15-09-2010 Through 18-09-2010",

}

TY - GEN

T1 - Model Checking Multivariate State Rewards

AU - Nielsen, Bo Friis

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

N1 - Conference code: 7

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1109/QEST.2010.10

DO - 10.1109/QEST.2010.10

M3 - Article in proceedings

SN - 978-0-7695-4188-4

SP - 7

EP - 16

BT - Seventh International Conference on the Quantitative Evaluation of Systems

T2 - 7th International Conference on the Quantitative Evaluation of Systems

Y2 - 15 September 2010 through 18 September 2010

ER -

Model Checking Multivariate State Rewards

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this