### Abstract

Language | Undefined |
---|---|

Pages | 17 |

Number of pages | 29 |

Journal | Logical methods in computer science |

Volume | 10 |

Issue number | 3 |

DOIs | |

Publication status | Published - 10 Sep 2014 |

### Keywords

- timed reachability
- EC Grant Agreement nr.: FP7/318490
- EC Grant Agreement nr.: FP7/2007-2013
- EWI-25348
- Long-run average
- Markov Automata
- expected time
- METIS-309680
- IR-93324
- Continuous time
- Quantitative analysis

### Cite this

*Logical methods in computer science*,

*10*(3), 17. https://doi.org/10.2168/LMCS-10(3:17)2014

}

*Logical methods in computer science*, vol. 10, no. 3, pp. 17. https://doi.org/10.2168/LMCS-10(3:17)2014

**Analysis of timed and long-run objectives for Markov automata.** / Guck, Dennis; Hatefi, Hassan; Hermanns, H.; Katoen, Joost P.; Timmer, Mark.

Research output: Contribution to journal › Article › Academic › peer-review

TY - JOUR

T1 - Analysis of timed and long-run objectives for Markov automata

AU - Guck, Dennis

AU - Hatefi, Hassan

AU - Hermanns, H.

AU - Katoen, Joost P.

AU - Timmer, Mark

N1 - eemcs-eprint-25348

PY - 2014/9/10

Y1 - 2014/9/10

N2 - Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a nondeterministic variation of continuous-time Markov chains. MAs are compositional and are used to provide a semantics for engineering frameworks such as (dynamic) fault trees, (generalised) stochastic Petri nets, and the Architecture Analysis & Design Language (AADL). This paper considers the quantitative analysis of MAs. We consider three objectives: expected time, long-run average, and timed (interval) reachability. Expected time objectives focus on determining the minimal (or maximal) expected time to reach a set of states. Long-run objectives determine the fraction of time to be in a set of states when considering an infinite time horizon. Timed reachability objectives are about computing the probability to reach a set of states within a given time interval. This paper presents the foundations and details of the algorithms and their correctness proofs. We report on several case studies conducted using a prototypical tool implementation of the algorithms, driven by the MAPA modelling language for efficiently generating MAs.

AB - Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a nondeterministic variation of continuous-time Markov chains. MAs are compositional and are used to provide a semantics for engineering frameworks such as (dynamic) fault trees, (generalised) stochastic Petri nets, and the Architecture Analysis & Design Language (AADL). This paper considers the quantitative analysis of MAs. We consider three objectives: expected time, long-run average, and timed (interval) reachability. Expected time objectives focus on determining the minimal (or maximal) expected time to reach a set of states. Long-run objectives determine the fraction of time to be in a set of states when considering an infinite time horizon. Timed reachability objectives are about computing the probability to reach a set of states within a given time interval. This paper presents the foundations and details of the algorithms and their correctness proofs. We report on several case studies conducted using a prototypical tool implementation of the algorithms, driven by the MAPA modelling language for efficiently generating MAs.

KW - timed reachability

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EWI-25348

KW - Long-run average

KW - Markov Automata

KW - expected time

KW - METIS-309680

KW - IR-93324

KW - Continuous time

KW - Quantitative analysis

U2 - 10.2168/LMCS-10(3:17)2014

DO - 10.2168/LMCS-10(3:17)2014

M3 - Article

VL - 10

SP - 17

JO - Logical methods in computer science

T2 - Logical methods in computer science

JF - Logical methods in computer science

SN - 1860-5974

IS - 3

ER -