Analysis of timed and long-run objectives for Markov automata

Dennis Guck, Hassan Hatefi, H. Hermanns, Joost P. Katoen, Mark Timmer

Research output: Contribution to journalArticle

  • 17 Citations

Abstract

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.
LanguageUndefined
Pages17
Number of pages29
JournalLogical methods in computer science
Volume10
Issue number3
DOIs
StatePublished - 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

@article{6f5526a88a2548d0862e5e551050bfe9,
title = "Analysis of timed and long-run objectives for Markov automata",
abstract = "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.",
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",
author = "Dennis Guck and Hassan Hatefi and H. Hermanns and Katoen, {Joost P.} and Mark Timmer",
note = "eemcs-eprint-25348",
year = "2014",
month = "9",
day = "10",
doi = "10.2168/LMCS-10(3:17)2014",
language = "Undefined",
volume = "10",
pages = "17",
journal = "Logical methods in computer science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "3",

}

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

In: Logical methods in computer science, Vol. 10, No. 3, 10.09.2014, p. 17.

Research output: Contribution to journalArticle

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 -