To formalize such statements, we would start with the primitive
propositions involved.These could be
(``a train is approaching the crossing'')
(``a train is passing the crossing'')
(``the light is flashing'')
(``the gate is down'')
This choice forces us to not refer to individual trains
and, thus we must simplifysome of our properties,
e.g. ,
``If a train is approaching, the gate will be down beforethe next train passes.''
(Think about the consequences of not making this change.)
Some of these English descriptions are ambiguous, however.
E.g. , can a single train be approaching
and passing simultaneously?When writing formal specifications,
we'll be forced to think about what we mean to say,and provide an unambiguous answer, one way or the other.
Continuing this example, we'll say that once a train is passing, itis no longer considered to be approaching.
Encode some of the properties from the
previous exercise in temporal logic.
It is often helpful to first turn the statement into a timeline(essentially a trace).
``Whenever a train passing, the gate is down.''
``If a train is approaching or passing,then the light is flashing.''
``If the gate is up and the lightis not flashing, then no train is passing or approaching.''
``If a train is approaching, the gate will be downbefore the next train passes.''
``If a train has finished passing, then later thegate will be up.''
``The gate will be up infinitely many times.''
``If a train is approaching, then it will be passing,and later it
will be done passing with no train approaching.''
Keep in mind that for any concept,
there are many different (but equivalent) formulasfor expressing it.
A trace satisfying this property. Observe in the trace shown that in one instance,
the gate goes down at the same time the train passes.In the LTL version we're using, we can't express
the idea``
strictly before
the next train passes.''Instead, we'll allow this simultaneity as a possibility.
I.e. , if a train is approaching,
then a train is not passing until the gate is down.However, this still allows that the gate could be
back up by the timea train passes, and a train might never pass.
A trace satisfying this property.
Since our logic cannot talk about the past,
we have to shift ourperspective to start while the train is still passing.
We've effectively reworded the statement to saythat if a train
is passing and will finish passing, then sometime after itis no longer passing, the gate will be up.
However, the status of the gate at other timesis not commented on.
We're only saying there is one moment after thetrain passes that the gate is up.
A trace satisfying this property.
This last condition is not something that a controller
would enforce. Instead, we would expect the trainscheduling software to enforce this.
The controller would be allowed to assume this,and we'd want to verify a property
only for
traces that also satisfy our scheduling assumptions
.
Of course, we can also do this by incorporatingassumptions into the formulas:
.
