View article

Model checking is considered as a promising approach for assuring the reliability of concurrent systems. Besides its strength it suffers from the state explosion problem, which reduces its applicability especially when systems grow larger. In this paper we propose a bounded rational verification approach for on-the-fly model checking of LTL properties. We optimize memory usage by increasing the probability of finding counter-examples. Since in on-the-fly model checking we do not have complete knowledge about the model, we use a machine learning method based on interaction and reward receiving. Based on the concept of fairness we propose a heuristic for defining rewards. We also exploit the ideas of probabilistic model checking in order to find a measure of correctness of the system in the case where no violations are found after generating a certain number of runs of the system. The experimental …