Scaling model checking of railway interlocking systems by safe automated decomposition
Anne E. Haxthausen, Alessandro Fantechi, Gloria Gori, S. Hagen Petersen, Óli Kárason Mikkelsen · European Transport Research Review · 2026
Model checking techniques applied to the verification of railway interlocking systems may fail to scale to interlockings controlling large railway networks, composed by hundreds of controlled entities, due to the state space explosion problem. Compositional methods have been proposed to reduce the size of networks to be model checked: the idea is to divide the network of the system into sub-networks and then model check the model instances for these sub-networks instead of that for the full network. It has been proved that, under given well-formedness conditions for the network, model checking safety properties of all such sub-networks guarantees safety properties of the full network. In this paper, we first observe that such a network division can be repeated, so that in the end, the full network is divided into a number of sub-networks of minimal size. This strategy is implemented as a division algorithm that we prove to be able to decompose any well-formed network into a set of elementary networks, each being an instance of one of a limited set of “elementary networks”, for which safety proofs have easily been given by model checking once for all: the successful application of the proposed algorithm hence proves the safety of the network. The algorithm is applied to some example networks of different complexity, showing that the execution time for such verification-by-division approach turns out to be a very small fraction of the time needed for a model checker to verify safety of the full network.