C.3 The Model Checking Problem 563
is open. A safety requirement is that “the signal is never green when the road is
open.” Given this property as input, the model checker should return “yes.” Indeed,
there is no state of the system where the road is open and the signal is green.
We are also interested in the liveness requirements, i.e., properties that assure that
the system “works,” such as the fact that “if the signal is red, then eventually in the
future it will be green.” This corresponds to the fact that we want to allow some train
to proceed sooner or later. In this case the model checker finds a counterexample. It
is represented by the infinite sequences of states that start with red and closed, and
then have red and open forever.
Some remarks ...