Railway interlocking systems are apparatuses that prevent conflicting movements
of trains through an arrangement of tracks. An interlocking takes into
consideration the position of the switches (of the turnouts) and does not allow
trains to be given clear signals unless the routes to be used by the trains do
not intersect. The authors had previously developed matrix-based and algebraic
(Groebner bases) models for the same goal. These models are independent from
the topology of the station.
Now a new model, based on Boolean logic, has been developed. Its main
contribution can be summarily described as follows: according to this new
model, any given proposed situation is safe iff a certain set of formulae
(translating the position of trains and the movements allowed --the latter
depend on the position of the switches and the color of the semaphores)
is consistent. This model is independent from the topology of the station too.
The package has been implemented in the computer algebra system (CAS) Maple,
and it makes an extensive use of its "Logic" package and the facilities
provided by this CAS to operate with sets. The code is surprisingly brief. The
fact that trains could occupy more than one section is considered.
The main procedure analyzes the safety of a proposed situation and returns,
if they exist, the sections where a collision could take place. Another
procedure checks whether a given section is accessible by a train located
on other given section or not.
Regarding execution times, the model shows similar times to the previous
matrix and GB-based models in intermediate situations. Nevertheless, their
speed evolve in very different ways. The GB-based one is very fast when
there are many trains and many accesses to other sections are allowed to
those trains. Meanwhile, the model presented here is very fast when there
are few allowed "itineraries" (what would be called paths in Graph Theory).
This work was partially supported by the research projects TIN2006-06190
(Ministerio de Educación y Ciencia, Spain) and UCM2008-910563 (UCM -
BSCH Gr. 58/08, research group ACEIA).