Abstract
| Original language | Undefined |
|---|---|
| Title of host publication | Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST) |
| Editors | K.R. Joshi, M. Siegle, Mariëlle Ida Antoinette Stoelinga, P.R. d' Argenio |
| Place of Publication | Berlin |
| Publisher | Springer |
| Pages | 55-71 |
| Number of pages | 17 |
| ISBN (Print) | 978-3-642-40195-4 |
| DOIs | |
| State | Published - Aug 2013 |
| Event | 10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - Buenos Aires, Argentina |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Verlag |
| Volume | 8054 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 10th International Conference on Quantitative Evaluation of Systems, QEST 2013 |
|---|---|
| Abbreviated title | QEST |
| Country | Argentina |
| City | Buenos Aires |
| Period | 27/08/13 → 30/08/13 |
| Internet address |
Fingerprint
Keywords
- EC Grant Agreement nr.: FP7/2007-2013
- EC Grant Agreement nr.: FP7/295261
- EC Grant Agreement nr.: FP7/318490
- EC Grant Agreement nr.: FP7/257005
- EWI-23542
- Process Algebra
- Quantitative analysis
- IR-87075
- Continuous time
- Markov Automata
- METIS-297747
Cite this
}
Modelling, Reduction and Analysis of Markov Automata. / Guck, Dennis; Hatefi, Hassan; Hermanns, H.; Katoen, Joost P.; Timmer, Mark.
Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST). ed. / K.R. Joshi; M. Siegle; Mariëlle Ida Antoinette Stoelinga; P.R. d' Argenio. Berlin : Springer, 2013. p. 55-71 (Lecture Notes in Computer Science; Vol. 8054).Research output: Scientific - peer-review › Conference contribution
TY - CHAP
T1 - Modelling, Reduction and Analysis of Markov Automata
AU - Guck,Dennis
AU - Hatefi,Hassan
AU - Hermanns,H.
AU - Katoen,Joost P.
AU - Timmer,Mark
N1 - eemcs-eprint-23542
PY - 2013/8
Y1 - 2013/8
N2 - Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.
AB - Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.
KW - EC Grant Agreement nr.: FP7/2007-2013
KW - EC Grant Agreement nr.: FP7/295261
KW - EC Grant Agreement nr.: FP7/318490
KW - EC Grant Agreement nr.: FP7/257005
KW - EWI-23542
KW - Process Algebra
KW - Quantitative analysis
KW - IR-87075
KW - Continuous time
KW - Markov Automata
KW - METIS-297747
U2 - 10.1007/978-3-642-40196-1_5
DO - 10.1007/978-3-642-40196-1_5
M3 - Conference contribution
SN - 978-3-642-40195-4
T3 - Lecture Notes in Computer Science
SP - 55
EP - 71
BT - Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST)
PB - Springer
ER -