Dennis Guck ; Hassan Hatefi ; Holger Hermanns ; Joost-Pieter Katoen ; Mark Timmer - Analysis of Timed and Long-Run Objectives for Markov Automata

lmcs:943 - Logical Methods in Computer Science, September 10, 2014, Volume 10, Issue 3 - https://doi.org/10.2168/LMCS-10(3:17)2014
Analysis of Timed and Long-Run Objectives for Markov AutomataArticle

Authors: Dennis Guck ; Hassan Hatefi ; Holger Hermanns ORCID; Joost-Pieter Katoen ORCID; Mark Timmer

    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.


    Volume: Volume 10, Issue 3
    Published on: September 10, 2014
    Imported on: January 6, 2014
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • smARt RAilroad maintenance eNGinEERing with stochastic model checking (ArRangeer); Funder: Netherlands Organisation for Scientific Research (NWO); Code: 12238
    • SYmbolic RedUction of Probabilistic Models (SYRUP); Funder: Netherlands Organisation for Scientific Research (NWO); Code: 612.063.817
    • 452-12-001; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 036.003.087
    • Mobility between Europe and Argentina applying Logics to Systems; Funder: European Commission; Code: 295261

    22 Documents citing this article

    Consultation statistics

    This page has been seen 2095 times.
    This article's PDF has been downloaded 997 times.