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