Model Checking Probabilistic Systems
David Jo, Barros Henriques · 2009
In this work, we present the implementation of an efficient model checking tool for formulas of a formal probabilistic logic (EPPL) over non-reliable digital circuits. In order to increase efficiency, we capitalize on several specific properties of these structures; however, the tool remains very open ended, allowing for adaptation to other, more complex, models. A method to minimize space problems on model checkers over a subset of probabilistic systems representable by Bayesian networks, is also introduced. For this, we consider factorizations of stochastic processes associated with the probability spaces generated by the systems. Implications of considering a temporal extension to the logic are discussed, a model checking procedure is proposed for the temporal case and implementation options are presented.