Analysis of Timed and Long-Run Objectives for Markov Automata

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

doi:10.2168/LMCS-10(3:17)2014

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 ; Joost-Pieter Katoen ; 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.

https://doi.org/10.2168/LMCS-10(3:17)2014

Source: arXiv.org:1407.7356

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

Licence: arXiv.org - Non-exclusive license to distribute

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

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

22 Documents citing this article

Bruno Lacerda;Anna Gautier;Alex Rutherford;Alex Stephens;Charlie Street;et al., 2022, Decision-making under uncertainty for multi-robot systems, Oxford University Research Archive (ORA) (University of Oxford), 35, 4, pp. 433-441, 10.3233/aic-220118, https://ora.ox.ac.uk/objects/uuid:f0d3f55d-cf71-4b0a-83f0-f6088858a0d7.

Tim Quatmann;Joost-Pieter Katoen, Lecture notes in computer science, Multi-objective Optimization of Long-run Average and Total Rewards, pp. 230-249, 2021, 10.1007/978-3-030-72016-2_13, https://doi.org/10.1007/978-3-030-72016-2_13.

Carlos Azevedo;Bruno Lacerda;Nick Hawes;Pedro Lima, Oxford University Research Archive (ORA) (University of Oxford), Long-Run Multi-Robot Planning under Uncertain Action Durations for Persistent Tasks, pp. 4323-4328, 2020, Las Vegas, NV, USA, 10.1109/iros45743.2020.9340901, https://ora.ox.ac.uk/objects/uuid:a19cd643-0e9a-42ee-9cc9-82487b69d30c.

Arnd Hartmanns;Holger Hermanns, Lecture notes in computer science, A Modest Markov Automata Tutorial, pp. 250-276, 2019, 10.1007/978-3-030-31423-1_8.

Arpit Sharma, 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE), Stuttering for Markov Automata, 2019, Guilin, China, 10.1109/tase.2019.000-7.

Yuliya Butkova;Arnd Hartmanns;Holger Hermanns, Lecture notes in computer science, A Modest Approach to Modelling and Checking Markov Automata, pp. 52-69, 2019, 10.1007/978-3-030-30281-8_4.

Yuliya Butkova;Gereon Fox, Lecture notes in computer science, Optimal Time-Bounded Reachability Analysis for Concurrent Systems, pp. 191-208, 2019, 10.1007/978-3-030-17465-1_11, https://doi.org/10.1007/978-3-030-17465-1_11.

Arpit Sharma, Lecture notes in computer science, Trace Relations and Logical Preservation for Markov Automata, pp. 162-178, 2018, 10.1007/978-3-030-00151-3_10.

Yuliya Butkova;Ralf Wimmer;Holger Hermanns, Lecture notes in computer science, Markov Automata on Discount!, pp. 19-34, 2018, 10.1007/978-3-319-74947-1_2.

Hassan Hatefi;Ralf Wimmer;Bettina Braitling;Luis María Ferrer Fioriti;Bernd Becker;et al., 2017, Cost vs. time in stochastic games and Markov automata, Formal Aspects of Computing, 29, 4, pp. 629-649, 10.1007/s00165-016-0411-1.

Joost-Pieter Katoen;Mariëlle Stoelinga, Lecture notes in computer science, Boosting Fault Tree Analysis by Formal Methods, pp. 368-389, 2017, 10.1007/978-3-319-68270-9_19.

Sebastian Junges;Dennis Guck;Joost-Pieter Katoen;Arend Rensink;Mariëlle Stoelinga, 2017, Fault trees on a diet: automated reduction by graph rewriting, Data Archiving and Networked Services (DANS), 29, 4, pp. 651-703, 10.1007/s00165-016-0412-0, https://research.utwente.nl/en/publications/be39c829-807d-41b5-86af-68fc1488a19b.

Tim Quatmann;Sebastian Junges;Joost-Pieter Katoen, arXiv (Cornell University), Markov Automata with Multiple Objectives, pp. 140-159, 2017, 10.1007/978-3-319-63387-9_7, http://arxiv.org/abs/1704.06648.

Yuliya Butkova;Ralf Wimmer;Holger Hermanns, Lecture notes in computer science, Long-Run Rewards for Markov Automata, pp. 188-203, 2017, 10.1007/978-3-662-54580-5_11.

Ali Jafari;Ehsan Khamespanah;Marjan Sirjani;Holger Hermanns;Matteo Cimini, 2016, PTRebeca: Modeling and analysis of distributed and asynchronous systems, Science of Computer Programming, 128, pp. 22-50, 10.1016/j.scico.2016.03.004.

Hao Wu;Xiaoxiao Yang;Joost-Pieter Katoen, Lecture notes in computer science, Performance Evaluation of Concurrent Data Structures, pp. 38-49, 2016, 10.1007/978-3-319-47677-3_3.

Joost-Pieter Katoen, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, The Probabilistic Model Checking Landscape, 2016, New York NY USA, 10.1145/2933575.2934574.

Joost-Pieter Katoen;Hao Wu, 2016, Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow, ACM Transactions on Design Automation of Electronic Systems, 22, 1, pp. 1-27, 10.1145/2914788.

Mark Timmer;Joost-Pieter Katoen;Jaco van de Pol;Mariëlle Stoelinga, 2016, Confluence reduction for Markov automata, Theoretical Computer Science, 655, pp. 193-219, 10.1016/j.tcs.2016.01.017, https://doi.org/10.1016/j.tcs.2016.01.017.

Gijs Kant;Alfons Laarman;Jeroen Meijer;Jaco van de Pol;Stefan Blom;et al., Lecture notes in computer science, LTSmin: High-Performance Language-Independent Model Checking, pp. 692-707, 2015, 10.1007/978-3-662-46681-0_61.

Hassan Hatefi;Bettina Braitling;Ralf Wimmer;Luis María Ferrer Fioriti;Holger Hermanns;et al., Lecture notes in computer science, Cost vs. Time in Stochastic Games and Markov Automata, pp. 19-34, 2015, 10.1007/978-3-319-25942-0_2.

Bettina Braitling;Luis María Ferrer Fioriti;Hassan Hatefi;Ralf Wimmer;Bernd Becker;et al., Lecture notes in computer science, Abstraction-Based Computation of Reward Measures for Markov Automata, pp. 172-189, 2014, 10.1007/978-3-662-46081-8_10.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2100 times.

This article's PDF has been downloaded 998 times.