First presenter Co-presenter(s)
Name :  Eugenio Roanes-Lozano * Name:  Antonio Hernando *
E-mail: E-mail:  
Affiliation: Universidad Complutense de Madrid Name:  Jose Antonio Alonso
Department:   E-mail:    
City: Name:   
State/Province:   E-mail:    
Country: Spain Name:   
12-04  E-mail:    
Session: 12- Nonstandard Applications of Computer Algebra Schedule:
Thursday, 16:00
Related website:  
Title of
A Logic Approach to Railway Interlocking Systems using Maple

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).