Analysis of Timed and Long-Run Objectives for Markov Automata

TL;DR

This paper develops algorithms for analyzing Markov automata with respect to expected time, long-run averages, and timed reachability, supported by case studies and a dedicated tool implementation.

Contribution

It introduces foundational algorithms for quantitative analysis of Markov automata focusing on timed and long-run objectives, with proofs and practical case studies.

Findings

Algorithms for expected time, long-run average, and timed reachability are correct.

Prototypical tool implementation demonstrates practical applicability.

Case studies validate the effectiveness of the proposed methods.

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.