کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
465003 | 697466 | 2011 | 15 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
The ins and outs of the probabilistic model checker MRMC
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
شبکه های کامپیوتری و ارتباطات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for continuous-time Markov decision processes (CTMDPs) and CSL model checking by discrete-event simulation. This paper presents the tool’s current status and its implementation details.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Performance Evaluation - Volume 68, Issue 2, February 2011, Pages 90–104
Journal: Performance Evaluation - Volume 68, Issue 2, February 2011, Pages 90–104
نویسندگان
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen,