Modular construction of the symbolic observation graph

Model checking for Linear Time Logic (LTL) is usually based on converting the (negation of a) property into a Buchi automaton, composing the automaton and the model, and finally checking for emptiness of the language of the composed system. The last step is the crucial stage of the verification process because of the state explosion problem. In this work, we present a solution which builds, in a modular way, an observation graph represented in a non-symbolic manner but where the nodes are essentially symbolic sets of states and the edges either labeled by events occurring in the formula or by synchronization actions between the system components. Due to the small number of events to be observed in a typical formula, this graph has a very moderate size and thus the time complexity for verification is negligible w.r.t. the time to build the observation graph. Experimental results show that our method outperforms both a non-modular generation of the symbolic graph and existing non-symbolic approaches (modular or not).