Abstract
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.
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 | |
Publication status | Published - Aug 2013 |
Event | 10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - University of Buenos Aires, Buenos Aires, Argentina Duration: 27 Aug 2013 → 30 Aug 2013 Conference number: 10 http://www.qest.org/qest2013/ |
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/Territory | Argentina |
City | Buenos Aires |
Period | 27/08/13 → 30/08/13 |
Internet address |
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