A Dynamic Transaction Reduction Theorem based on Weak Conditional Independence

Nowadays, model checking is a well-established formal technique for verifying safety-critical systems. However, one of its main disadvantages is the so-called state-space explosion, as it is necessary to examine every possible configuration reached by the execution of the (possibly parallel) system. This issue is of exponential order and still remains a fundamental challenge in model checking research. It is therefore crucial to find methods that can either manipulate large sets of configurations (states) at a single time (symbolic methods), or let us forget the problem of checking all the possible parallel interleavings by reducing the amount of states to check without losing any significance (reduction methods). The majority of the existing state-reducing methods are mostly based on Partial Order Reduction (POR) and Transaction Reduction (TR). Both reduction methods rely on the concept of (in)dependence between the execution order of certain statements. If the order of execution of two statements does not matter then they reach the same state. If so, it is not necessary to check every possible intermediate state the parallel system may witness. POR algorithms generally perform a selective state-space search by exploring a only a subset of the reachable states, whereas TR algorithms merge multiple sequential statements and disregard the states reached in between. This thesis focuses on finding new methods for tackling the state-space explosion and assessing their effectiveness. To this purpose, the first contribution is the systematic presentation of different POR and TR techniques in a single formal setting in order to ease their understanding. The main innovative contribution consists in a novel dynamic TR method based on a concept of independence that is called weakly conditional. The new method is presented, implemented and successively tested against other existing methods to see what degree of improvement is made.