ACCELERATING ITERATIVE METHODS FOR BOUNDED REACHABILITY PROBABILITIES IN MARKOV DECISION PROCESSES

Computer and Knowledge Engineering

مقالات آماده انتشار، پذیرفته شده، انتشار آنلاین از تاریخ 11 آذر 1399  

نوع مقاله: Software Engineering-Bagheri

شناسه دیجیتال (DOI): 10.22067/cke.2020.39288

نویسنده

Mohammadsadegh Mohagheghi

Vali-e-Asr University of Rafsanjan

چکیده

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. In this paper we propose 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.