A method of enhancing probabilistic verification efficiency for computer and telecommunication systems

A. M. Mironov^a, S. L. Frenkel<sup>ba

a</sup> Institute of Informatics Problems, Russian Academy of Sciences, 44-2 Vavilov Str., Moscow 119333, Russian Federation
^b Moscow Institute of Radio, Electronics, and Automation (MIREA), 78 Prosp. Vernadskogo, Moscow 119454, Russian Federation

Abstract: The paper considers the problem of reduction of probabilistic transition systems (PTS) in order to reduce the complexity of model checking of such systems. The problem of model checking of a PTS is to calculate truth values of formulas of temporal probabilistic computational tree logic (PCTL) in the initial state of the PTS. The paper introduces the concept of equivalence of states of a PTS and represents an algorithm for removing equivalent states. The result of this algorithm is a PTS such that all its properties expressed by formulas of PCTL coincide with those of the original PTS.

Keywords: verification; model checking; probabilistic transition systems; probabilistic temporal logic; reduction of probabilistic models.

Received: 05.11.2014

DOI: 10.14357/19922264140408

Bibliographic databases:

•