Compositional Abstraction of Stochastic Systems

Joost P. Katoen, Daniel Klink, M. Neuhausser

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

25 Citations (Scopus)
56 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 languageUndefined
Title of host publicationFormal Modeling and Analysis of Timed Systems
Place of PublicationBerlin
PublisherSpringer
Pages195-211
Number of pages17
ISBN (Print)978-3-642-04367-3
DOIs
Publication statusPublished - 3 Sep 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume5813
ISSN (Print)0302-9743

Keywords

  • METIS-264292
  • EWI-17105
  • IR-69313

Cite this

Katoen, J. P., Klink, D., & Neuhausser, M. (2009). Compositional Abstraction of Stochastic Systems. In Formal Modeling and Analysis of Timed Systems (pp. 195-211). [10.1007/978-3-642-04368-0_16] (Lecture Notes in Computer Science; Vol. 5813). Berlin: Springer. https://doi.org/10.1007/978-3-642-04368-0_16
Katoen, Joost P. ; Klink, Daniel ; Neuhausser, M. / Compositional Abstraction of Stochastic Systems. Formal Modeling and Analysis of Timed Systems. Berlin : Springer, 2009. pp. 195-211 (Lecture Notes in Computer Science).
@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",
year = "2009",
month = "9",
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. 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 proceedingConference contributionAcademicpeer-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

ER -

Katoen JP, Klink D, Neuhausser M. Compositional Abstraction of Stochastic Systems. In 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). https://doi.org/10.1007/978-3-642-04368-0_16