Improving Online Railway Deadlock Detection using a Partial Order Reduction

TL;DR

This paper presents an improved SAT-based online deadlock detection method for railway dispatching that uses partial order reduction to enhance performance, aiding semi-autonomous control systems.

Contribution

It introduces a novel partial order reduction technique for SAT-based deadlock detection, significantly reducing computational complexity and enabling faster, more efficient online verification.

Findings

Significant performance improvements over previous methods

Reduced size of SAT instances through partial order reduction

Effective early detection of deadlocks in railway networks

Abstract

Although railway dispatching on large national networks is gradually becoming more computerized, there are still major obstacles to retrofitting (semi-)autonomous control systems. In addition to requiring extensive and detailed digitalization of infrastructure models and information systems, exact optimization for railway dispatching is computationally hard. Heuristic algorithms and manual overrides are likely to be required for semi-autonomous railway operations for the foreseeable future. In this context, being able to detect problems such as deadlocks can be a valuable part of a runtime verification system. If bound-for-deadlock situations are correctly recognized as early as possible, human operators will have more time to better plan for recovery operations. Deadlock detection may also be useful for verification in a feedback loop with a heuristic or semi-autonomous dispatching algorithm if the dispatching algorithm cannot itself guarantee a deadlock-free plan. We describe a SAT-based planning algorithm for online detection of bound-for-deadlock situations. The algorithm exploits parallel updates of train positions and a partial order reduction technique to significantly reduce the number of state transitions (and correspondingly, the sizes of the formulas) in the SAT instances needed to prove whether a deadlock situation is bound to happen in the future. Implementation source code and benchmark instances are supplied, and a direct comparison against another recent study demonstrates significant performance gains.