Analysis of timed and long-run objectives for Markov automata

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

  • 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.
Original languageUndefined
Pages (from-to)17
Number of pages29
JournalLogical methods in computer science
Volume10
Issue number3
DOIs
StatePublished - 10 Sep 2014

Fingerprint

Petri nets
Markov processes
Semantics
Chemical analysis
Modeling languages

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

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

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

Research output: Scientific - peer-reviewArticle

@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",
doi = "10.2168/LMCS-10(3:17)2014",
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: Scientific - peer-reviewArticle

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 -