View article

System specifications have long been expressed through automata based languages, enabling verification techniques such as model checking. These verification techniques can assess whether a property holds or not, given a system specification. However, model checking techniques suffer from the traditionally called state explosion problem, that is, models which are useful for analysis grow exponentially in size when verifying their concurrent behaviour. This state explosion problem is a serious limitation of model checking techniques, often making the application of tools that apply them infeasible, and limiting techniques to only a partial exploration of the complete state space. In this work we propose a novel approach that could help gather useful, quantified domain-related information from such incomplete explorations, leveraging on the concept of probabilistic behaviour models of the environment, for …