We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
ANALYSIS OF TIMED AND LONG-RUN OBJECTIVES FOR MARKOV AUTOMATA.
- Authors
GUCK, DENNIS; HATEF, HASSAN; HERMANNS, HOLGER; KATOEN, JOOST-PIETER; TIMMER, MARK
- Abstract
Markov automata (MAs) extend labelled transition systems with random de-lays 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 engineer-ing 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 proto-typical tool implementation of the algorithms, driven by the MAPA modelling language for efficiently generating MAs.
- Subjects
MACHINE theory; ALGORITHMS; ARCHITECTURE Analysis &; Design Language; MODELING languages (Computer science); MARKOV processes; STOCHASTIC processes
- Publication
Logical Methods in Computer Science (LMCS), 2014, Vol 10, Issue 3, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.2168/LMCS-10(3:17)2014