research-article

Open access

A Modest Approach to Markov Automata

Authors:

Yuliya Butkova,

Arnd Hartmanns,

Holger HermannsAuthors Info & Claims

ACM Transactions on Modeling and Computer Simulation (TOMACS), Volume 31, Issue 3

Article No.: 14, Pages 1 - 34

https://doi.org/10.1145/3449355

Published: 24 August 2021 Publication History

All formats PDF

Abstract

Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In this article, we present extensions to MODEST, an expressive high-level language with roots in process algebra, that allow large Markov automata models to be specified in a succinct, modular way. We illustrate the advantages of MODEST over alternative languages. Model checking Markov automata models requires dedicated algorithms for time-bounded and long-run average reward properties. We describe and evaluate the state-of-the-art algorithms implemented in the mcsta model checker of the MODEST TOOLSET. We find that mcsta improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools. We explain a partial-exploration approach based on the BRTDP method designed to mitigate the state space explosion problem of model checking, and experimentally evaluate its effectiveness. This problem can be avoided entirely by purely simulation-based techniques, but the nondeterminism in Markov automata hinders their straightforward application. We explain how lightweight scheduler sampling can make simulation possible, and provide a detailed evaluation of its usefulness on several benchmarks using the MODEST TOOLSET’s modes simulator.

References

[1]

Elvio Gilberto Amparore, Gianfranco Balbo, Marco Beccuti, Susanna Donatelli, and Giuliana Franceschinis. 2016. 30 years of GreatSPN. In Principles of Performance and Reliability Modeling and Evaluation. Springer, 227–254.

[2]

Pranav Ashok, Tomás Brázdil, Jan Kretínský, and Ondrej Slámecka. 2018. Monte Carlo tree search for verifying reachability in Markov decision processes. In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 11245. Springer, 322–335.

[3]

Pranav Ashok, Yuliya Butkova, Holger Hermanns, and Jan Kretínský. 2018. Continuous-time Markov decisions based on partial exploration. In Proceedings of ATVA (Lecture Notes in Computer Science), Vol. 11138. Springer, 317–334.

[4]

Carlos Azevedo, Bruno Lacerda, Nick Hawes, and Pedro U. Lima. 2020. Long-run multi-robot planning with uncertain task durations. In Proceedings of AAMAS. International Foundation for Autonomous Agents and Multiagent Systems, 1750–1752.

[5]

Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. 2018. Model checking probabilistic systems. In Handbook of Model Checking.Springer, 963–999.

[6]

Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2010. Performance evaluation and model checking join forces. Commun. ACM 53, 9 (2010), 76–85.

Digital Library

[7]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.

Digital Library

[8]

Christel Baier, Joachim Klein, Linda Leuschner, David Parker, and Sascha Wunderlich. 2017. Ensuring the reliability of your model checker: Interval iteration for Markov decision processes. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 10426. Springer, 160–180.

[9]

Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, and Thomas Noll. 2014. A review of statistical model checking pitfalls on real-time stochastic models. In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 8803. Springer, 177–192.

[10]

Henrik C. Bohnenkamp, Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. 2006. MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32, 10 (2006), 812–830.

Digital Library

[11]

Blai Bonet and Hector Geffner. 2003. Labeled RTDP: Improving the convergence of real-time dynamic programming. In Proceedings of ICAPS. AAAI Press, 12–21.

[12]

Hichem Boudali, Pepijn Crouzen, and Mariëlle Stoelinga. 2010. A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput. 7, 2 (2010), 128–143.

Digital Library

[13]

Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, and Mateusz Ujma. 2014. Verification of Markov decision processes using learning algorithms. In Proceedings of ATVA (Lecture Notes in Computer Science), Vol. 8837. Springer, 98–114.

[14]

Tomás Brázdil, Holger Hermanns, Jan Krcál, Jan Kretínský, and Vojtech Rehák. 2012. Verification of open interactive Markov chains. In Proceedings of FSTTCS (LIPIcs), Vol. 18. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 474–485.

[15]

Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana, Spyridon Samothrakis, and Simon Colton. 2012. A survey of Monte Carlo tree search methods. IEEE Trans. Comput. Intell. AI Games 4, 1 (2012), 1–43.

[16]

Carlos E. Budde, Pedro R. D’Argenio, and Arnd Hartmanns. 2019. Automated compositional importance splitting. Sci. Comput. Program. 174 (2019), 90–108.

[17]

Carlos E. Budde, Pedro R. D’Argenio, Arnd Hartmanns, and Sean Sedwards. 2020. An efficient statistical model checker for nondeterminism and rare events. Proceedings of STTT 22, 6 (2020), 759–780.

Digital Library

[18]

Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini. 2017. JANI: Quantitative model and tool interaction. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 10206. 151–168.

Digital Library

[19]

Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretínský, David Parker, Tim Quatmann, Andrea Turrini, and Zhen Zhang. 2021. On correctness, precision, and performance in quantitative verification (QComp 2020 competition report). In Proceedings of ISoLA (Lecture Notes in Computer Science). Springer. To appear.

[20]

Yuliya Butkova. 2019. A Modest Approach to Modelling and Checking Markov Automata (Artifact). 4TU.ResearchData.

[21]

Yuliya Butkova and Gereon Fox. 2019. Optimal time-bounded reachability analysis for concurrent systems. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 11428. Springer, 191–208.

[22]

Yuliya Butkova, Arnd Hartmanns, and Holger Hermanns. 2019. A modest approach to modelling and checking Markov automata. In Proceedings of QEST (Lecture Notes in Computer Science), Vol. 11785. Springer, 52–69.

[23]

Yuliya Butkova, Hassan Hatefi, Holger Hermanns, and Jan Krcál. 2015. Optimal continuous time Markov decisions. In Proceedings of ATVA (Lecture Notes in Computer Science), Vol. 9364. Springer, 166–182.

[24]

Yuliya Butkova, Ralf Wimmer, and Holger Hermanns. 2017. Long-run rewards for Markov automata. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 10206. 188–203.

Digital Library

[25]

Yuliya Butkova, Ralf Wimmer, and Holger Hermanns. 2018. Markov automata on discount! In Proceedings of MMB (Lecture Notes in Computer Science), Vol. 10740. Springer, 19–34.

[26]

Adrien Couëtoux, Jean-Baptiste Hoock, Nataliya Sokolovska, Olivier Teytaud, and Nicolas Bonnard. 2011. Continuous upper confidence trees. In Proceedings of LION (Lecture Notes in Computer Science), Vol. 6683. Springer, 433–445.

Digital Library

[27]

Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, and Tatjana Petrov. 2017. Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18, 2 (2017), 12:1–12:25.

Digital Library

[28]

Pedro D’Argenio, Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2015. Smart sampling for lightweight verification of Markov decision processes. STTT 17, 4 (2015), 469–484.

Digital Library

[29]

Pedro R. D’Argenio, Juan A. Fraire, and Arnd Hartmanns. 2020. Sampling distributed schedulers for resilient space communication. In Proceedings of NFM (Lecture Notes in Computer Science), Vol. 12229. Springer, 291–310.

Digital Library

[30]

Pedro R. D’Argenio, Arnd Hartmanns, Axel Legay, and Sean Sedwards. 2016. Statistical approximation of optimal schedulers for probabilistic timed automata. In Proceedings of iFM (Lecture Notes in Computer Science), Vol. 9681. Springer, 99–114.

Digital Library

[31]

Pedro R. D’Argenio, Arnd Hartmanns, and Sean Sedwards. 2018. Lightweight statistical model checking in nondeterministic continuous time. In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 11245. Springer, 336–353.

[32]

Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist. 2015. Uppaal Stratego. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 9035. Springer, 206–211.

[33]

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, and Zheng Wang. 2011. Time for statistical model checking of real-time systems. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 6806. Springer, 349–355.

[34]

Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. A Storm is coming: A modern probabilistic model checker. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 10427. Springer, 592–600.

[35]

J. B. Dugan, S. J. Bavuso, and M. A. Boyd. 1992. Dynamic fault-tree models for fault-tolerant computer systems. IEEE Trans. Reliabil. 41, 3 (1992), 363–377.

[36]

Christian Eisentraut. 2017. Principles of Markov Automata. Ph.D. Dissertation. Saarland University, Germany. publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/27085/1/thesis-Pflichtexemplar.pdf.

[37]

Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, and Lijun Zhang. 2013. A semantics for every GSPN. In Proceedings of Petri Nets (Lecture Notes in Computer Science), Vol. 7927. Springer, 90–109.

Digital Library

[38]

Christian Eisentraut, Holger Hermanns, and Lijun Zhang. 2010. On probabilistic automata in continuous time. In Proceedings of LICS. IEEE Computer Society, 342–351.

Digital Library

[39]

Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. 2013. CADP 2011: A toolbox for the construction and analysis of distributed processes. STTT 15, 2 (2013), 89–107.

[40]

Marcus Gerhold, Arnd Hartmanns, and Mariëlle Stoelinga. 2019. Model-based testing of stochastically timed systems. Innov. Syst. Softw. Eng. 15, 3-4 (2019), 207–233.

[41]

Timo P. Gros. 2018. Markov Automata Taken by Storm. Master’s thesis. Saarland University, Germany.

[42]

Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuhäußer. 2012. Quantitative timed analysis of interactive Markov chains. In Proceedings of NFM (Lecture Notes in Computer Science), Vol. 7226. Springer, 8–23.

[43]

Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, and Mark Timmer. 2014. Analysis of timed and long-run objectives for Markov automata. Logic. Methods Comput. Sci. 10, 3 (2014).

[44]

Dennis Guck, Mark Timmer, Hassan Hatefi, Enno Ruijters, and Mariëlle Stoelinga. 2014. Modelling and analysis of Markov reward automata. In Proceedings of ATVA (Lecture Notes in Computer Science), Vol. 8837. Springer, 168–184.

[45]

Serge Haddad and Benjamin Monmege. 2018. Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735 (2018), 111–131.

[46]

Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretínský, David Parker, Tim Quatmann, Enno Ruijters, and Marcel Steinmetz. 2019. The 2019 comparison of tools for the analysis of quantitative formal models. In Proceedings of 25 Years of TACAS: TOOLympics (Lecture Notes in Computer Science), Vol. 11429. Springer, 69–92.

[47]

Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen. 2013. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Design 43, 2 (2013), 191–232.

Digital Library

[48]

Arnd Hartmanns. 2021. A Modest Approach to Markov Automata (Artifact). 4TU.ResearchData.

[49]

Arnd Hartmanns and Holger Hermanns. 2014. The modest toolset: An integrated environment for quantitative modelling and verification. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 8413. Springer, 593–598.

[50]

Arnd Hartmanns and Holger Hermanns. 2015. Explicit model checking of very large MDP using partitioning and secondary storage. In Proceedings of ATVA (Lecture Notes in Computer Science), Vol. 9364. Springer, 131–147.

[51]

Arnd Hartmanns and Holger Hermanns. 2019. A modest Markov automata tutorial. In Proceedings of 15th International Reasoning Web Summer School (Lecture Notes in Computer Science), Vol. 11810. Springer, 250–276.

[52]

Arnd Hartmanns and Benjamin Lucien Kaminski. 2020. Optimistic value iteration. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 12225. Springer, 488–511.

Digital Library

[53]

Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, and Enno Ruijters. 2019. The quantitative verification benchmark set. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 11427. Springer, 344–350.

[54]

Arnd Hartmanns, Sean Sedwards, and Pedro R. D’Argenio. 2017. Efficient simulation-based verification of probabilistic timed automata. In Proceedings of Winter Simulation Conference. IEEE, 1419–1430.

[55]

Hassan Hatefi. 2017. Finite Horizon Analysis of Markov Automata. Ph.D. Dissertation. Saarland University, Germany. scidok.sulb.uni-saarland.de/volltexte/2017/6743/.

[56]

Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. 2004. Approximate probabilistic model checking. In Proceedings of VMCAI (Lecture Notes in Computer Science), Vol. 2937. Springer, 73–84.

[57]

C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall.

Digital Library

[58]

Michael J. Kearns, Yishay Mansour, and Andrew Y. Ng. 2002. A sparse sampling algorithm for near-optimal planning in large Markov decision processes. Mach. Learn. 49, 2-3 (2002), 193–208.

[59]

Michaela Klauck. 2020. Modest Fret-pi LRTDP. Retrieved from https://dgit.cs.uni-saarland.de/Michaela/modest-fret-pi-lrtdp.

[60]

Andrey Kolobov, Mausam, Daniel S. Weld, and Hector Geffner. 2011. Heuristic search for generalized stochastic shortest path MDPs. In Proceedings of ICAPS. AAAI Press.

[61]

Jan Krcál and Pavel Krcál. 2015. Scalable analysis of fault trees with dynamic features. In Proceedings of DSN. IEEE Computer Society, 89–100.

Digital Library

[62]

Stuart Kurkowski, Tracy Camp, and Michael Colagrosso. 2005. MANET simulation studies: The incredibles. Mobile Comput. Commun. Rev. 9, 4 (2005), 50–61.

Digital Library

[63]

Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 6806. Springer, 585–591.

[64]

Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. 2002. Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282, 1 (2002), 101–150.

Digital Library

[65]

Kim Guldstrand Larsen and Axel Legay. 2018. Statistical model checking the 2018 edition! In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 11245. Springer, 261–270.

[66]

Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2014. Scalable verification of Markov decision processes. In Proceedings of WS-FMDS at SEFM (Lecture Notes in Computer Science), Vol. 8938. Springer, 350–362.

[67]

Masoumeh Mansouri, Bruno Lacerda, Nick Hawes, and Federico Pecora. 2019. Multi-robot planning under uncertain travel times and safety constraints. In Proceedings of IJCAI. ijcai.org, 478–484.

[68]

H. Brendan McMahan, Maxim Likhachev, and Geoffrey J. Gordon. 2005. Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In Proceedings of ICML (ACM International Conference Proceeding Series), Vol. 119. ACM, 569–576.

[69]

Robin Milner. 1989. Communication and Concurrency. Prentice-Hall.

Digital Library

[70]

Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc.

[71]

Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen. 2017. Markov automata with multiple objectives. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 10426. Springer, 140–159.

[72]

Tim Quatmann and Joost-Pieter Katoen. 2018. Sound value iteration. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 10981. Springer, 643–661.

[73]

Markus N. Rabe and Sven Schewe. 2011. Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. Acta Info. 48, 5-6 (2011), 291–315.

[74]

Daniël Reijsbergen, Pieter-Tjerk de Boer, Werner R. W. Scheinhardt, and Boudewijn R. Haverkort. 2015. On hypothesis testing for statistical model checking. Proceedings of STTT 17, 4 (2015), 377–395.

Digital Library

[75]

Gerardo Rubino and Bruno Tuffin (Eds.). 2009. Rare Event Simulation Using Monte Carlo Methods. Wiley.

[76]

Roberto Segala. 1995. Modeling and Verification of Randomized Distributed Real-time Systems. Ph.D. Dissertation. Massachusetts Institute of Technology, Cambridge, MA, USA. hdl.handle.net/1721.1/36560.

Digital Library

[77]

Marcel Steinmetz, Jörg Hoffmann, and Olivier Buffet. 2016. Goal probability analysis in probabilistic planning: Exploring and enhancing the state of the art. J. Artif. Intell. Res. 57 (2016), 229–271.

[78]

Kevin J. Sullivan, Joanne Bechta Dugan, and David Coppit. 1999. The Galileo fault tree analysis tool. In Proceedings of FTCS. IEEE Computer Society, 232–235.

[79]

Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, and Mariëlle Stoelinga. 2012. Efficient modelling and generation of Markov automata. In Proceedings of CONCUR (Lecture Notes in Computer Science), Vol. 7454. Springer, 364–379.

[80]

Håkan L. S. Younes and Reid G. Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 2404. Springer, 223–235.

Cited By

Budde CD’Argenio PFraire JHartmanns AZhang Z(2024)Modest Models and Tools for Real Stochastic Timed SystemsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_6(115-142)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_6
Andriushchenko RBork ABudde CČeška MGrover KHahn EHartmanns AIsraelsen BJansen NJeppson JJunges SKöhl MKönighofer BKřetínský JMeggendorfer TParker DPranger SQuatmann TRuijters ETaylor LVolk MWeininger MZhang Z(2024)Tools at the Frontiers of Quantitative VerificationTOOLympics Challenge 202310.1007/978-3-031-67695-6_4(90-146)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_4
Khan SKatoen JBouissou M(2023)A Compositional Semantics of Boolean-Logic Driven Markov ProcessesIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2023.326127021:2(701-716)Online publication date: 24-Mar-2023
https://dl.acm.org/doi/10.1109/TDSC.2023.3261270
Show More Cited By

Index Terms

A Modest Approach to Markov Automata
1. Computing methodologies
  1. Modeling and simulation
2. Theory of computation
  1. Formal languages and automata theory
    1. Automata extensions
      1. Quantitative automata
  2. Logic
    1. Verification by model checking

Recommendations

Model checking probabilistic systems against pushdown specifications

Model checking is a fully automatic verification technique traditionally used to verify finite-state systems against regular specifications. Although regular specifications have been proven to be feasible in practice, many desirable specifications are ...
Markov automata with multiple objectives
Abstract
Markov automata combine probabilistic branching, exponentially distributed delays and nondeterminism. This compositional variant of continuous-time Markov decision processes is used in reliability engineering, performance evaluation and stochastic ...
Checking timed Büchi automata emptiness on simulation graphs

Timed automata [Alur and Dill 1994] comprise a popular model for describing real-time and embedded systems and reasoning formally about them. Efficient model-checking algorithms have been developed and implemented in tools such as Kronos [Daws et al. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Modeling and Computer Simulation

ACM Transactions on Modeling and Computer Simulation Volume 31, Issue 3

Special Issue on Qest 2019

July 2021

149 pages

ISSN:1049-3301

EISSN:1558-1195

DOI:10.1145/3476822

Editor:
Francesco Quaglia
University of Rome Tor Vergata, Italy

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 August 2021

Accepted: 01 February 2021

Revised: 01 September 2020

Received: 01 April 2020

Published in TOMACS Volume 31, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

European Research Council
Guangdong Province
Nederlandse Organisatie voor Wetenschappelijk Onderzoek
Deutsche Forschungsgemeinschaft

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
707
Total Downloads

Downloads (Last 12 months)277
Downloads (Last 6 weeks)45

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Budde CD’Argenio PFraire JHartmanns AZhang Z(2024)Modest Models and Tools for Real Stochastic Timed SystemsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_6(115-142)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_6
Andriushchenko RBork ABudde CČeška MGrover KHahn EHartmanns AIsraelsen BJansen NJeppson JJunges SKöhl MKönighofer BKřetínský JMeggendorfer TParker DPranger SQuatmann TRuijters ETaylor LVolk MWeininger MZhang Z(2024)Tools at the Frontiers of Quantitative VerificationTOOLympics Challenge 202310.1007/978-3-031-67695-6_4(90-146)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_4
Khan SKatoen JBouissou M(2023)A Compositional Semantics of Boolean-Logic Driven Markov ProcessesIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2023.326127021:2(701-716)Online publication date: 24-Mar-2023
https://dl.acm.org/doi/10.1109/TDSC.2023.3261270
Street CMansouri MLacerda B(2023)Formal Modelling for Multi-Robot Systems Under UncertaintyCurrent Robotics Reports10.1007/s43154-023-00104-04:3(55-64)Online publication date: 15-Aug-2023
https://doi.org/10.1007/s43154-023-00104-0
Hartmanns A(2022)An Overview of Modest Models and Tools for Real Stochastic Timed SystemsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.355.1355(1-12)Online publication date: 21-Mar-2022
https://doi.org/10.4204/EPTCS.355.1
Archibald BCalder MSevegnani M(2022)Probabilistic BigraphsFormal Aspects of Computing10.1145/354518034:2(1-27)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1145/3545180
Hartmanns AKlauck M(2022)The Modest State of Learning, Sampling, and Verifying StrategiesLeveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning10.1007/978-3-031-19759-8_25(406-432)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19759-8_25

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents