Synthesis of railway-signaling plans using reachability games

Patrick Frederik Soelmark Kasting, Michael Reichhardt Hansen, Steen Vester

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

580 Downloads (Pure)


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.
Original languageEnglish
Title of host publication28th Symposium on the Implementation and Application of Functional Programming Languages,
Number of pages13
VolumePart F127410
PublisherAssociation for Computing Machinery
Publication date2016
ISBN (Print)9781450347679
Publication statusPublished - 2016
Event28th Symposium on the Implementation and Application of Functional Programming Languages - KU Leuven, Leuven, Belgium
Duration: 31 Aug 20162 Sep 2016


Conference28th Symposium on the Implementation and Application of Functional Programming Languages
LocationKU Leuven
SeriesAcm Int. Conf. Proc. Ser


  • Computer Programming
  • Computer Programming Languages
  • Information Sources and Analysis
  • Applied Mathematics
  • Computer programming languages
  • Functions
  • Problem oriented languages
  • Railroads
  • Signaling
  • Translation (languages)
  • Transportation
  • Compact representation
  • Correct-by-construction
  • Development time
  • Domain specific languages
  • Imperative features
  • Mathematical formulation
  • Railway signaling
  • Translation functions
  • Functional programming


Dive into the research topics of 'Synthesis of railway-signaling plans using reachability games'. Together they form a unique fingerprint.

Cite this