Analysis of Timed and Long-Run Objectives for Markov Automata
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 nondete...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2014-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/943/pdf |
| _version_ | 1797268686417952768 |
|---|---|
| author | Dennis Guck Hassan Hatefi Holger Hermanns Joost-Pieter Katoen Mark Timmer |
| author_facet | Dennis Guck Hassan Hatefi Holger Hermanns Joost-Pieter Katoen Mark Timmer |
| author_sort | Dennis Guck |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:25Z |
| format | Article |
| id | doaj.art-3ac2c4d87a244f7eb6adafb18be67674 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:25Z |
| publishDate | 2014-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-3ac2c4d87a244f7eb6adafb18be676742024-03-08T09:37:13ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742014-09-01Volume 10, Issue 310.2168/LMCS-10(3:17)2014943Analysis of Timed and Long-Run Objectives for Markov AutomataDennis GuckHassan HatefiHolger Hermannshttps://orcid.org/0000-0002-2766-9615Joost-Pieter Katoenhttps://orcid.org/0000-0002-6143-1926Mark TimmerMarkov 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.https://lmcs.episciences.org/943/pdfcomputer science - logic in computer sciencecomputer science - formal languages and automata theory |
| spellingShingle | Dennis Guck Hassan Hatefi Holger Hermanns Joost-Pieter Katoen Mark Timmer Analysis of Timed and Long-Run Objectives for Markov Automata Logical Methods in Computer Science computer science - logic in computer science computer science - formal languages and automata theory |
| title | Analysis of Timed and Long-Run Objectives for Markov Automata |
| title_full | Analysis of Timed and Long-Run Objectives for Markov Automata |
| title_fullStr | Analysis of Timed and Long-Run Objectives for Markov Automata |
| title_full_unstemmed | Analysis of Timed and Long-Run Objectives for Markov Automata |
| title_short | Analysis of Timed and Long-Run Objectives for Markov Automata |
| title_sort | analysis of timed and long run objectives for markov automata |
| topic | computer science - logic in computer science computer science - formal languages and automata theory |
| url | https://lmcs.episciences.org/943/pdf |
| work_keys_str_mv | AT dennisguck analysisoftimedandlongrunobjectivesformarkovautomata AT hassanhatefi analysisoftimedandlongrunobjectivesformarkovautomata AT holgerhermanns analysisoftimedandlongrunobjectivesformarkovautomata AT joostpieterkatoen analysisoftimedandlongrunobjectivesformarkovautomata AT marktimmer analysisoftimedandlongrunobjectivesformarkovautomata |