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 journalArticleAcademicpeer-review

    23 Citations (Scopus)
    86 Downloads (Pure)

    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
    Publication statusPublished - 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