Efficient Modelling, Generation and Analysis of Markov Automata

Mark Timmer, K. Iwama (Editor)

Research output: Contribution to journalArticleAcademic

41 Downloads (Pure)

Abstract

Quantitative model checking is concerned with the verification of both quantitative and qualitative properties over models incorporating quantitative information. Increases in expressivity of the models involved allow more types of systems to be analysed, but also raise the difficulty of their efficient analysis. Three years ago, the Markov automaton (MA) was introduced as a generalisation of probabilistic automata and interactive Markov chains, supporting nondeterminism, discrete probabilistic choice as well as stochastic timing (Markovian rates). Later, the tool IMCA was developed to compute time-bounded reachability probabilities, expected times and long-run averages for sets of goal states within an MA. However, an efficient formalism for modelling and generating MAs was still lacking. Additionally, the omnipresent state space explosion also threatened the analysability of these models. This thesis solves the first problem and contributes significantly to the solution of the second.
Original languageUndefined
Pages (from-to)139-140
Number of pages2
JournalBulletin of the European Association for Theoretical Computer Science
Volume112
Publication statusPublished - Feb 2014

Keywords

  • EWI-24602
  • IR-90553
  • METIS-304036

Cite this

@article{be59e41115cc4e3d8927d1822b15ed1b,
title = "Efficient Modelling, Generation and Analysis of Markov Automata",
abstract = "Quantitative model checking is concerned with the verification of both quantitative and qualitative properties over models incorporating quantitative information. Increases in expressivity of the models involved allow more types of systems to be analysed, but also raise the difficulty of their efficient analysis. Three years ago, the Markov automaton (MA) was introduced as a generalisation of probabilistic automata and interactive Markov chains, supporting nondeterminism, discrete probabilistic choice as well as stochastic timing (Markovian rates). Later, the tool IMCA was developed to compute time-bounded reachability probabilities, expected times and long-run averages for sets of goal states within an MA. However, an efficient formalism for modelling and generating MAs was still lacking. Additionally, the omnipresent state space explosion also threatened the analysability of these models. This thesis solves the first problem and contributes significantly to the solution of the second.",
keywords = "EWI-24602, IR-90553, METIS-304036",
author = "Mark Timmer and K. Iwama",
note = "Abstract of PhD Thesis",
year = "2014",
month = "2",
language = "Undefined",
volume = "112",
pages = "139--140",
journal = "Bulletin of the European Association for Theoretical Computer Science",
issn = "0252-9742",
publisher = "European Association for Theoretical Computer Science",

}

Efficient Modelling, Generation and Analysis of Markov Automata. / Timmer, Mark; Iwama, K. (Editor).

In: Bulletin of the European Association for Theoretical Computer Science, Vol. 112, 02.2014, p. 139-140.

Research output: Contribution to journalArticleAcademic

TY - JOUR

T1 - Efficient Modelling, Generation and Analysis of Markov Automata

AU - Timmer, Mark

A2 - Iwama, K.

N1 - Abstract of PhD Thesis

PY - 2014/2

Y1 - 2014/2

N2 - Quantitative model checking is concerned with the verification of both quantitative and qualitative properties over models incorporating quantitative information. Increases in expressivity of the models involved allow more types of systems to be analysed, but also raise the difficulty of their efficient analysis. Three years ago, the Markov automaton (MA) was introduced as a generalisation of probabilistic automata and interactive Markov chains, supporting nondeterminism, discrete probabilistic choice as well as stochastic timing (Markovian rates). Later, the tool IMCA was developed to compute time-bounded reachability probabilities, expected times and long-run averages for sets of goal states within an MA. However, an efficient formalism for modelling and generating MAs was still lacking. Additionally, the omnipresent state space explosion also threatened the analysability of these models. This thesis solves the first problem and contributes significantly to the solution of the second.

AB - Quantitative model checking is concerned with the verification of both quantitative and qualitative properties over models incorporating quantitative information. Increases in expressivity of the models involved allow more types of systems to be analysed, but also raise the difficulty of their efficient analysis. Three years ago, the Markov automaton (MA) was introduced as a generalisation of probabilistic automata and interactive Markov chains, supporting nondeterminism, discrete probabilistic choice as well as stochastic timing (Markovian rates). Later, the tool IMCA was developed to compute time-bounded reachability probabilities, expected times and long-run averages for sets of goal states within an MA. However, an efficient formalism for modelling and generating MAs was still lacking. Additionally, the omnipresent state space explosion also threatened the analysability of these models. This thesis solves the first problem and contributes significantly to the solution of the second.

KW - EWI-24602

KW - IR-90553

KW - METIS-304036

M3 - Article

VL - 112

SP - 139

EP - 140

JO - Bulletin of the European Association for Theoretical Computer Science

JF - Bulletin of the European Association for Theoretical Computer Science

SN - 0252-9742

ER -