Compositional Abstraction of Stochastic Systems

Joost P. Katoen; Daniel Klink; M. Neuhausser

doi:10.1007/978-3-642-04368-0_16

Compositional Abstraction of Stochastic Systems

Joost P. Katoen, Daniel Klink, M. Neuhausser

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

26 Citations (Scopus)

277 Downloads (Pure)

Abstract

We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.

Original language	Undefined
Title of host publication	Formal Modeling and Analysis of Timed Systems
Place of Publication	Berlin
Publisher	Springer
Pages	195-211
Number of pages	17
ISBN (Print)	978-3-642-04367-3
DOIs	https://doi.org/10.1007/978-3-642-04368-0_16
Publication status	Published - 3 Sept 2009
Event	7th International Conference on Formal Modeling and Analysis of Timed Systems - Budapest, Hungary Duration: 14 Sept 2009 → 16 Sept 2009

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	5813
ISSN (Print)	0302-9743

Conference

Conference	7th International Conference on Formal Modeling and Analysis of Timed Systems
Period	14/09/09 → 16/09/09
Other	14-16 Sept 2009

Keywords

METIS-264292
EWI-17105
IR-69313

Access to Document

10.1007/978-3-642-04368-0_16

http://eprints.eemcs.utwente.nl/secure2/17105/02/fulltext.pdf

Cite this

@inproceedings{d69abf6c122644f0a22d4811870aa581,

title = "Compositional Abstraction of Stochastic Systems",

abstract = "We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.",

keywords = "METIS-264292, EWI-17105, IR-69313",

author = "Katoen, {Joost P.} and Daniel Klink and M. Neuhausser",

note = "10.1007/978-3-642-04368-0_16 ; 7th International Conference on Formal Modeling and Analysis of Timed Systems ; Conference date: 14-09-2009 Through 16-09-2009",

year = "2009",

month = sep,

day = "3",

doi = "10.1007/978-3-642-04368-0_16",

language = "Undefined",

isbn = "978-3-642-04367-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "195--211",

booktitle = "Formal Modeling and Analysis of Timed Systems",

}

Katoen, JP, Klink, D & Neuhausser, M 2009, Compositional Abstraction of Stochastic Systems. in Formal Modeling and Analysis of Timed Systems., 10.1007/978-3-642-04368-0_16, Lecture Notes in Computer Science, vol. 5813, Springer, Berlin, pp. 195-211, 7th International Conference on Formal Modeling and Analysis of Timed Systems, 14/09/09. https://doi.org/10.1007/978-3-642-04368-0_16

Compositional Abstraction of Stochastic Systems. / Katoen, Joost P.; Klink, Daniel; Neuhausser, M.
Formal Modeling and Analysis of Timed Systems. Berlin: Springer, 2009. p. 195-211 10.1007/978-3-642-04368-0_16 (Lecture Notes in Computer Science; Vol. 5813).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Compositional Abstraction of Stochastic Systems

AU - Katoen, Joost P.

AU - Klink, Daniel

AU - Neuhausser, M.

N1 - 10.1007/978-3-642-04368-0_16

PY - 2009/9/3

Y1 - 2009/9/3

N2 - We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.

AB - We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.

KW - METIS-264292

KW - EWI-17105

KW - IR-69313

U2 - 10.1007/978-3-642-04368-0_16

DO - 10.1007/978-3-642-04368-0_16

M3 - Conference contribution

SN - 978-3-642-04367-3

T3 - Lecture Notes in Computer Science

SP - 195

EP - 211

BT - Formal Modeling and Analysis of Timed Systems

PB - Springer

CY - Berlin

T2 - 7th International Conference on Formal Modeling and Analysis of Timed Systems

Y2 - 14 September 2009 through 16 September 2009

ER -