Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings

Interlockings implement Railway Signalling Principles which ensure the safe movements of trains along a track system. They are safety critical systems which require a thorough analysis. We are aiming at supporting the safety analysis by automated tools, namely model checkers.

Model checking provides a full state space exploration and is thus intrinsically limited in the problem’s state space. Current research focuses on extending these limits and pushing the boundaries. In our work we investigate possible optimisations for symbolic model checking. Symbolic model checkers exploit a compact representation of the model using Binary Decision Diagram. These structures provide a canonical representation which allows for reductions. The compactness of this data structure and possible reductions are dependent on two orderings: the ordering of variables and the ordering in which sub-structures are manipulated. This paper reports on findings of how a near to optimal ordering can be generated for the domain of interlocking verification.