Synthesis of railway-signaling plans using reachability games

In this work, we show the feasibility of using functional programming (more specifically F#) in connection with gamebased methods for synthesis of correct-by-construction controllers (also called signaling plans) for railway networks. This is a massively resource-demanding application. A model for railway networks comprising trains, signals, linear sections, and points is established together with a domain-specific language capturing the important concepts in the model. A translation from railway network models to two-player reachability games is provided. In these games, the existential player (the control system) controls signals and points and the universal player (the antagonistic environment) controls movement of trains. A winning strategy for the existential player provides a signaling plan that will safely guide trains through the network. The concepts from the railway network model and the twoplayer reachability game are captured, in a natural manner, by type declarations in F#. Furthermore, the F# translation functions are formulated in a manner that is close to the mathematical formulations. This increases confidence in the correctness of the implementation and it decreases the development time. Imperative features of F# proved useful in two places: Hash tables and arrays were used in the representations of the railway network model and the reachability game. This allowed for more compact representations and a more efficient game solver (providing the winning strategy). Experiments show that we are able to synthesize signaling plans for real railway networks of substantial size.