Term Assignment - Railway Station

Summary: Design a control system of a railway station, formalize it, and prove its safety.

A railway station is a connected directed graph, see input formats for details on input format files. Nodes without outgoing edges are called exits, nodes without incoming edges are called entrances. We consider only graphs where there is a path from every entrance to every exit. Every node has a unique label which begins with a lower-case letter.

1. Every node with more than one outgoing edge is a switch.
2. Time dependent elements of a railway station are:
   1. positions of moving trains
   2. states of signalling devices at entrance nodes
   3. states of switches
3. A train is located at exactly one node in each moment.
4. Train movement always follow graph edge orientation (they can not go reverse).
5. When there is a train in some node, then it has arrived there before (it was not there from time immemorial) and it shall depart later (but it is not clear when – it depends on the “will of an engine driver”).
6. Signalling devices are located at entrance nodes only. A signalling device can block the entrance node: When the signalling device is closed, a train can not enter the railway station and it must wait at the entrance node; when the signalling device is opened, the train might (but doesn't have to) enter the railway station. Every train (or its engine driver) always respects signalling devices. Every entrance node has exactly one outgoing edge, that is, it is never a switch.
7. Every train has assigned an exit it wants to reach. This exit remains fixed during the train movement in the railway station.
8. The railway station control system routes the train to its exit by switching switches. The control system can arbitrarily switch any switch.
9. When an entrance node is empty, then a new train can appear there at any moment (even right after the entrance of the previous train).

We recognize the following critical situations in a railway station:

1. A train is situated at a switch node when the switch is switched.
2. There are two or more trains at the same node at the same time.
3. A signalling device never opens (it stays closed all the time).

Write a program, which:

1. designs a railway station control system for any railway station and formalizes it accordingly to the description above;
2. proves that the designed control system can not reach a critical state

Summarize the result of your work in a short technical report where you describe your method and, in particular, your achieved results.

The railway station graph input format is as follows.

digraph my_station {
  entry1 -> node1;
  ...
  node1 -> exit1;
  node1 -> exit2;
}

digraph station {
  in -> v;
  v -> out1;
  v -> out2;
}

A railway station is modeled in discrete time. Time is linear and every time moment has exactly one previous and one successive moment. At every time moment, the control system has to define the state of switches and signalling devices.

Your program should process the following tasks for an arbitrary input railway stations using automated reasoning tools.

1. Railway station formalization:
   1. Formalize in the First Order Logic in the TPTP language the “physical” railway station behavior, that is, how trains go through the railway station based on the state of signaling devices and engine driver decisions. Every time dependent predicate p that describe something that we are able to establish has to be described by at most one formula of the shape p(T+1) ⇔ φ where formula φ depends only conditions in time T or antecedent (this syntactically guaranties correctness of the definition). This covers the state of switches, position of trains, and so on. This does not cover the engine driver will which we do not know (we know only that every train departs at some time).
   2. Prove that this formalization is not contradictory with additional conditions which say that a train moves from one node to another as soon as possible (that is, the engine driver decides to depart immediately).

1. Formalize the railway station control system in the same way as in point 1.
2. Prove that the formalization of the railway station together with the control system is not contradictory.
3. Prove that a critical state can not appear.
4. A railway station must allow a train to enter the railway station as soon as there is free path from its starting entrance node to its departure exit. You need to prove that in the following railway station with 2 trains at time T, the first at out1 and the second at in both going to exit out2, the signaling device at in will be opened at time T+1.

1. The output of your program will be commented files in the TPTP language together with the output of a selected theorem prover or a model checker.
2. Use heavily the TPTP directive include to keep TPTP files readable and without duplicity.
3. Your program must be executable in a computer lab without additional SW (except the theorem prover or model checker). Otherwise you will need to present your solution on your computer.

A railway station can be modeled both in discrete or in continues time. The control system determines the state of switches and signaling devices at every time moment.

Your program should do the following tasks for an arbitrary input railway station.

1. Railway station formalization:
   1. Formalize in the UPPALL System the “physical” railway station behavior, that is, how trains go through the railway station based on the state of signaling devices and engine driver decisions.
   2. Show (using suitable UPPALL queries) that this formalization is not contradictory with additional conditions which say that a train moves from one node to another as soon as possible (that is, the engine driver decides to depart immediately).
2. Formalize the railway station control system in the same way as in point 1.
3. Prove (using suitable UPPALL queries) that a critical state can not appear.
4. A railway station must allow a train to enter the railway station as soon as there is free path from its starting entrance node to its departure exit. You need to prove that in the following railway station with 2 trains at time T, the first at out1 and the second at in both going to exit out2, the signaling device at in will be opened at time T+1.

1. The output of your program should be in XML format acceptable by the UPPALL system and the output of the UPPALL system which proves required properties.
2. Your program must be executable in a computer lab without additional SW. Otherwise you will need to present your solution on your computer.