View article

Model checking is a powerful and widespread technique for the verification of finite state concurrent systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. In [16], we proposed an incremental and compositional verification approach where the system model is partitioned according to the actions occurring in the property to be verified and where the environment of a component is taken into account. But the verification at each increment might be costly. On the other hand, Symbolic Observation Graphs provide a compact analysis means for LTL∖X properties. We have shown a purely modular construction of these in [15]. Therefore, in this paper, we combine both techniques to benefit from their pros. Also, we propose a novel approach for incrementally checking the validity of the counter-example.