Gul Agha & Karl Palmskog (2018):
A Survey of Statistical Model Checking.
ACM Trans. Model. Comput. Simul. 28(1),
pp. 6:1–6:39,
doi:10.1145/3158668.
Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger & Pei-Hsin Ho (1992):
Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems.
In: Robert L. Grossman, Anil Nerode, Anders P. Ravn & Hans Rischel: Hybrid Systems,
Lecture Notes in Computer Science 736.
Springer,
pp. 209–229,
doi:10.1007/3-540-57318-6_30.
Rajeev Alur & David L. Dill (1994):
A Theory of Timed Automata.
Theor. Comput. Sci. 126(2),
pp. 183–235,
doi:10.1016/0304-3975(94)90010-8.
Christel Baier (2016):
Probabilistic Model Checking.
In: Javier Esparza, Orna Grumberg & Salomon Sickert: Dependable Software Systems Engineering,
NATO Science for Peace and Security Series – D: Information and Communication Security 45.
IOS Press,
pp. 1–23,
doi:10.3233/978-1-61499-627-9-1.
Christel Baier, Luca de Alfaro, Vojtech Forejt & Marta Kwiatkowska (2018):
Model Checking Probabilistic Systems.
In: Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith & Roderick Bloem: Handbook of Model Checking.
Springer,
pp. 963–999,
doi:10.1007/978-3-319-10575-8_28.
Christel Baier & Joost-Pieter Katoen (2008):
Principles of model checking.
MIT Press.
Richard Bellman (1957):
A Markovian decision process.
Journal of Mathematics and Mechanics 6(5),
pp. 679–684.
Henrik C. Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns & Joost-Pieter Katoen (2006):
MoDeST: A Compositional Modeling Formalism for Hard and Softly Timed Systems.
IEEE Trans. Software Eng. 32(10),
pp. 812–830,
doi:10.1109/TSE.2006.104.
Henrik C. Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen & Ric Klaren (2003):
The Modest Modeling Tool and Its Implementation.
In: Peter Kemper & William H. Sanders: 13th International Conference on Computer Performance Evaluations, Modelling Techniques and Tools (TOOLS),
Lecture Notes in Computer Science 2794.
Springer,
pp. 116–133,
doi:10.1007/978-3-540-45232-4_8.
Blai Bonet & Hector Geffner (2003):
Labeled RTDP: Improving the Convergence of Real-Time Dynamic Programming.
In: Enrico Giunchiglia, Nicola Muscettola & Dana S. Nau: 13th International Conference on Automated Planning and Scheduling (ICAPS).
AAAI,
pp. 12–21.
Carlos E. Budde, Pedro R. D'Argenio & Arnd Hartmanns (2019):
Automated compositional importance splitting.
Sci. Comput. Program. 174,
pp. 90–108,
doi:10.1016/j.scico.2019.01.006.
Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns & Sean Sedwards (2020):
An efficient statistical model checker for nondeterminism and rare events.
Int. J. Softw. Tools Technol. Transf. 22(6),
pp. 759–780,
doi:10.1007/s10009-020-00563-2.
Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges & Andrea Turrini (2017):
JANI: Quantitative Model and Tool Interaction.
In: Axel Legay & Tiziana Margaria: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Lecture Notes in Computer Science 10206,
pp. 151–168,
doi:10.1007/978-3-662-54580-5_9.
Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretínský, David Parker, Tim Quatmann, Andrea Turrini & Zhen Zhang (2020):
On Correctness, Precision, and Performance in Quantitative Verification (QComp 2020 Competition Report).
In: Tiziana Margaria & Bernhard Steffen: 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA),
Lecture Notes in Computer Science 12479.
Springer,
pp. 216–241,
doi:10.1007/978-3-030-83723-5_15.
Yuliya Butkova, Arnd Hartmanns & Holger Hermanns (2021):
A Modest Approach to Markov Automata.
ACM Trans. Model. Comput. Simul. 31(3),
pp. 14:1–14:34,
doi:10.1145/3449355.
Pedro R. D'Argenio, Juan A. Fraire & Arnd Hartmanns (2020):
Sampling Distributed Schedulers for Resilient Space Communication.
In: Ritchie Lee, Susmit Jha & Anastasia Mavridou: 12th International NASA Formal Methods Symposium (NFM),
Lecture Notes in Computer Science 12229.
Springer,
pp. 291–310,
doi:10.1007/978-3-030-55754-6_17.
Pedro R. D'Argenio, Arnd Hartmanns, Axel Legay & Sean Sedwards (2016):
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata.
In: Erika Ábrahám & Marieke Huisman: 12th International Conference on Integrated Formal Methods (iFM),
Lecture Notes in Computer Science 9681.
Springer,
pp. 99–114,
doi:10.1007/978-3-319-33693-0_7.
Pedro R. D'Argenio, Arnd Hartmanns & Sean Sedwards (2018):
Lightweight Statistical Model Checking in Nondeterministic Continuous Time.
In: Tiziana Margaria & Bernhard Steffen: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA),
Lecture Notes in Computer Science 11245.
Springer,
pp. 336–353,
doi:10.1007/978-3-030-03421-4_22.
Pedro R. D'Argenio, Bertrand Jeannet, Henrik Ejersbo Jensen & Kim Guldstrand Larsen (2002):
Reduction and Refinement Strategies for Probabilistic Analysis.
In: Holger Hermanns & Roberto Segala: Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV),
Lecture Notes in Computer Science 2399.
Springer,
pp. 57–76,
doi:10.1007/3-540-45605-8_5.
Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis & Zheng Wang (2011):
Time for Statistical Model Checking of Real-Time Systems.
In: Ganesh Gopalakrishnan & Shaz Qadeer: 23rd International Conference on Computer Aided Verification (CAV),
Lecture Notes in Computer Science 6806.
Springer,
pp. 349–355,
doi:10.1007/978-3-642-22110-1_27.
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen & Matthias Volk (2017):
A Storm is Coming: A Modern Probabilistic Model Checker.
In: Rupak Majumdar & Viktor Kuncak: 29th International Conference on Computer Aided Verification (CAV),
Lecture Notes in Computer Science 10427.
Springer,
pp. 592–600,
doi:10.1007/978-3-319-63390-9_31.
Christian Eisentraut, Holger Hermanns & Lijun Zhang (2010):
On Probabilistic Automata in Continuous Time.
In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS).
IEEE Computer Society,
pp. 342–351,
doi:10.1109/LICS.2010.41.
Ansgar Fehnker & Kaylash Chaudhary (2018):
Twenty Percent and a Few Days – Optimising a Bitcoin Majority Attack.
In: Aaron Dutle, César A. Muñoz & Anthony Narkawicz: 10th International NASA Formal Methods Symposium (NFM),
Lecture Notes in Computer Science 10811.
Springer,
pp. 157–163,
doi:10.1007/978-3-319-77935-5_11.
Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick & Lijun Zhang (2011):
Measurability and safety verification for stochastic hybrid systems.
In: Marco Caccamo, Emilio Frazzoli & Radu Grosu: 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC).
ACM,
pp. 43–52,
doi:10.1145/1967701.1967710.
Sergio Giro & Pedro R. D'Argenio (2007):
Quantitative Model Checking Revisited: Neither Decidable Nor Approximable.
In: Jean-François Raskin & P. S. Thiagarajan: 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS),
Lecture Notes in Computer Science 4763.
Springer,
pp. 179–194,
doi:10.1007/978-3-540-75454-1_14.
Sergio Giro & Pedro R. D'Argenio (2009):
On the Expressive Power of Schedulers in Distributed Probabilistic Systems.
Electron. Notes Theor. Comput. Sci. 253(3),
pp. 45–71,
doi:10.1016/j.entcs.2009.10.005.
Ernst Moritz Hahn & Arnd Hartmanns (2016):
A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques.
In: Martin Fränzle, Deepak Kapur & Naijun Zhan: Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA),
Lecture Notes in Computer Science 9984,
pp. 85–100,
doi:10.1007/978-3-319-47677-3_6.
Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretínský, David Parker, Tim Quatmann, Enno Ruijters & Marcel Steinmetz (2019):
The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models (QComp 2019 Competition Report).
In: Dirk Beyer, Marieke Huisman, Fabrice Kordon & Bernhard Steffen: 25 Years of TACAS: TOOLympics,
Lecture Notes in Computer Science 11429.
Springer,
pp. 69–92,
doi:10.1007/978-3-030-17502-3_5.
Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns & Joost-Pieter Katoen (2013):
A compositional modelling and analysis framework for stochastic hybrid systems.
Formal Methods Syst. Des. 43(2),
pp. 191–232,
doi:10.1007/s10703-012-0167-z.
Arnd Hartmanns & Holger Hermanns (2014):
The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification.
In: Erika Ábrahám & Klaus Havelund: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Lecture Notes in Computer Science 8413.
Springer,
pp. 593–598,
doi:10.1007/978-3-642-54862-8_51.
Arnd Hartmanns & Holger Hermanns (2015):
Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage.
In: Bernd Finkbeiner, Geguang Pu & Lijun Zhang: 13th International Symposium on Automated Technology for Verification and Analysis (ATVA),
Lecture Notes in Computer Science 9364.
Springer,
pp. 131–147,
doi:10.1007/978-3-319-24953-7_10.
Arnd Hartmanns & Holger Hermanns (2019):
A Modest Markov Automata Tutorial.
In: Markus Krötzsch & Daria Stepanova: 15th International Reasoning Web Summer School,
Lecture Notes in Computer Science 11810.
Springer,
pp. 250–276,
doi:10.1007/978-3-030-31423-1_8.
Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann & Enno Ruijters (2019):
The Quantitative Verification Benchmark Set.
In: Tomás Vojnar & Lijun Zhang: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Lecture Notes in Computer Science 11427.
Springer,
pp. 344–350,
doi:10.1007/978-3-030-17462-0_20.
Arnd Hartmanns, Sean Sedwards & Pedro R. D'Argenio (2017):
Efficient simulation-based verification of probabilistic timed automata.
In: 2017 Winter Simulation Conference (WSC).
IEEE,
pp. 1419–1430,
doi:10.1109/WSC.2017.8247885.
Ronald A. Howard (1960):
Dynamic Programming and Markov Processes.
MIT Press.
Michaela Klauck & Holger Hermanns (2021):
A Modest Approach to Dynamic Heuristic Search in Probabilistic Model Checking.
In: Alessandro Abate & Andrea Marin: 18th International Conference on Quantitative Evaluation of Systems (QEST),
Lecture Notes in Computer Science 12846.
Springer,
pp. 15–38,
doi:10.1007/978-3-030-85172-9_2.
Maximilian A. Köhl, Michaela Klauck & Holger Hermanns (2021):
Momba: JANI Meets Python.
In: Jan Friso Groote & Kim Guldstrand Larsen: 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Lecture Notes in Computer Science 12652.
Springer,
pp. 389–398,
doi:10.1007/978-3-030-72013-1_23.
Marta Z. Kwiatkowska, Gethin Norman & David Parker (2011):
PRISM 4.0: Verification of Probabilistic Real-Time Systems.
In: Ganesh Gopalakrishnan & Shaz Qadeer: 23rd International Conference on Computer Aided Verification (CAV),
Lecture Notes in Computer Science 6806.
Springer,
pp. 585–591,
doi:10.1007/978-3-642-22110-1_47.
Marta Z. Kwiatkowska, Gethin Norman, David Parker & Jeremy Sproston (2006):
Performance analysis of probabilistic timed automata using digital clocks.
Formal Methods Syst. Des. 29(1),
pp. 33–78,
doi:10.1007/s10703-006-0005-2.
Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala & Jeremy Sproston (2002):
Automatic verification of real-time systems with discrete probability distributions.
Theor. Comput. Sci. 282(1),
pp. 101–150,
doi:10.1016/S0304-3975(01)00046-9.
Axel Legay, Sean Sedwards & Louis-Marie Traonouez (2014):
Scalable Verification of Markov Decision Processes.
In: Carlos Canal & Akram Idani: 4th Workshop on Formal Methods in the Development of Software (WS-FMDS),
Lecture Notes in Computer Science 8938.
Springer,
pp. 350–362,
doi:10.1007/978-3-319-15201-1_23.
Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Rajesh Jayashankara Shridevi, Koushik Chakraborty, Sanghamitra Roy & Zhen Zhang (2019):
Probabilistic Verification for Reliable Network-on-Chip System Design.
In: Kim Guldstrand Larsen & Tim A. C. Willemse: 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS),
Lecture Notes in Computer Science 11687.
Springer,
pp. 110–126,
doi:10.1007/978-3-030-27008-7_7.
Fernando D. Raverta, Juan A. Fraire, Pablo G. Madoery, Ramiro A. Demasi, Jorge M. Finochietto & Pedro R. D'Argenio (2021):
Routing in Delay-Tolerant Networks under uncertain contact plans.
Ad Hoc Networks 123,
pp. 102663,
doi:10.1016/j.adhoc.2021.102663.
Riley Roberts, Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty & Zhen Zhang (2021):
Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System.
In: Alberto Lluch-Lafuente & Anastasia Mavridou: 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS),
Lecture Notes in Computer Science 12863.
Springer,
pp. 232–248,
doi:10.1007/978-3-030-85248-1_16.
Gerardo Rubino & Bruno Tuffin (2009):
Rare Event Simulation using Monte Carlo Methods.
Wiley,
doi:10.1002/9780470745403.
Jeremy Sproston (2000):
Decidable Model Checking of Probabilistic Hybrid Automata.
In: Mathai Joseph: 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT),
Lecture Notes in Computer Science 1926.
Springer,
pp. 31–45,
doi:10.1007/3-540-45352-0_5.