Accelerating Iterative Methods for Bounded Reachability Probabilities in Markov Decision Processes
Publish place: Computer and Knowledge Engineering، Vol: 3، Issue: 2
Publish Year: 1400
نوع سند: مقاله ژورنالی
زبان: English
View: 237
This Paper With 7 Page And PDF Format Ready To Download
- Certificate
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
JR_CKE-3-2_003
تاریخ نمایه سازی: 25 خرداد 1401
Abstract:
Probabilistic model checking is a formal method for verification of the quantitative and qualitative properties of computer systems with stochastic behaviors. Markov Decision Processes (MDPs) are well-known formalisms for modeling this class of systems. Bounded reachability probabilities are an important class of properties that are computed in probabilistic model checking. Iterative numerical computations are used for this class of properties. A significant draw-back of the standard iterative methods is the redundant computations that do not affect the final results of the computations, but increase the running time of the computations. The study proposes two new approaches to avoid redundant computations for bounded reachability analysis. The general idea of these approaches is to identify and avoid useless numerical computations in iterative methods for computing bounded reachability probabilities.
Keywords:
Authors
Mohammadsadegh Mohagheghi
Department of Computer science, Vali-e-Asr University of Rafsanjan, Rafsanjan, Iran.
مراجع و منابع این Paper:
لیست زیر مراجع و منابع استفاده شده در این Paper را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود Paper لینک شده اند :