Die Problemstellung ist folgende: Eine Steuerung hat die Aufgabe, eine
Bahnschranke bei Durchfahrt eines Zuges rechtzeitig zu schliessen und
danach wieder zu öffnen. Sowohl das Herannahen eines Zuges auf eine
bestimmte Distanz als auch das Entfernen des Zuges werden der Steuerung
über Sensorsignale mitgeteilt. Es wird angenommen, dass zwischen dem
Signalisieren eines herannahenden Zuges mindestens zwei Zeiteinheiten
vergehen, bevor der Zug den Übergang erreicht, und dass er nach höchstens
fünf Zeiteinheiten den Übergangsbereich wieder verläßt. Die Schranken
benötigen maximal eine Zeiteinheit, um zu sich zu schliessen, und zwischen
einer und zwei Zeiteinheiten, um sich zu öffnen.  Die Fragestellung bei der
Analyse ist nun, ob eine gegebene Realisierung der Steuerung, zu der eine
bestimmte Wartezeit gehört, die die Steuerung zwischen dem Erkennen eines
sich nähernden Zuges und dem Schliessen der Schranken wartet, in jedem Fall
verhindert, dass ein Zug den Übergangsbereich durchfährt, ohne dass die
Schranken geschlossen sind.  Dabei muss sinnvollerweise die Lösung
ausgeschlossen werden, dass die Steuerung die Schranken ständig geschlossen
läßt.