The Ins and Outs of the Probabilistic Model Checker MRMC
By Joost-Pieter Katoen, Ivan S. Zapreev, E. M. Hahn, Holger Hermanns, D. Jansen. 2009 Sixth International Conference on the Quantitative Evaluation of Systems, 2009
377 citations recorded by the source corpus.
Subfields: Computational Theory and Mathematics, Safety, Risk, Reliability and Quality, Software
View Paper: https://www.semanticscholar.org/paper/8a6818f092710d5b03bd713bf74059346cff1678
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computational Theory and Mathematics
- Marta Z. Kwiatkowska
- David Parker
- Gethin Norman
- Joost-Pieter Katoen
- Vojtěch Forejt
- Nam Sung Kim
- Todd Mytkowicz
- Qiang Xu
In Safety, Risk, Reliability and Quality
- David Parker
- Gethin Norman
- Marta Z. Kwiatkowska
- Joost-Pieter Katoen
- Sohag Kabir
- Ashish Tiwari
- Patrick Lincoln
In Software
- Joost-Pieter Katoen
- Marta Z. Kwiatkowska
- David Parker
- Gethin Norman
- Nam Sung Kim
- Todd Mytkowicz
- Qiang Xu
- Thomas A. Henzinger
Citations in the corpus
- Approximate Computing: A Survey (2016, methodology): “The popular tools MRMC [29] and PRISM [31] have been used in diverse fields ranging from analyzing the source code of wireless protocols for faults to modeling human driver behavior for use in autonomous driving systems.”
- A Storm is Coming: A Modern Probabilistic Model Checker (2017, background): “Like its main competitors Prism [1], MRMC [2], and iscasMC [3], Storm relies on numerical and symbolic computations.”
- Probabilistic programming (2014, background): “Though the idea has been around since the 80’s [34, 56], in the past decade there has been a lot of progress in building model checkers such as PRISM [36] and MRMC [29].”
- Statistical Model Checking: An Overview (2010, neutral): “Both Ymer and Vesta as well as their successors [23,24] focus on the verification of classical stochastic extension of temporal logics.”
- Automated Verification Techniques for Probabilistic Systems (2011, background): “There are also various other probabilistic model checkers for discrete- and continuous-time Markov chains, notably MRMC [61].”
- PRISM 4.0: Verification of Probabilistic Real-Time Systems (2011, neutral): “Finally, MRMC [7], a probabilistic model checker for Markov chains and Markov reward models, has recently also added support for continuous-time MDPs, another model combining nondeterministic, probabilistic and real-time features.”