We consider a system composed by several trains , a gate and a controller. Every automaton is described as in the figure below.

In CMC, the synchronization of the automata is given explicitly in a table.

The following file contains the full description of the system: Tsystem

Verifying this system consists in deciding properties like:

- P1 : When a train is on the crossing, the gate is down.
- P2 : When an Exit signal is sent by a train, the gate is open in less than 70 t.u. unless another train is approaching or committed in the crossing.
- P3 : When a train may perform an App or Exit signal, it can be received by the controller.

Now the verification procedure can be called by typing: Verify(F1,S,T); and Verify(F1,S,T); and Verify(F1,S,T);

- P1 : When a train is on the crossing, the gate is down.
- P2 : When an Exit signal is sent by a train, the gate is open in less than 50 t.u. unless another train is approaching or committed in the crossing.

We look for a dense-time control: the controller can prevent time elapsing and force a controllable action to happen at any point in time. We just require that there are at least D time units between two controllable actions.

Let C be the self-loop automaton generating controllable actions s.t. at least D time units separate these actions. We can then reduce the existence of a controller to a model checking problem for (Train | Train | Gate | C ) and the following formula: Note that the modalities of Lnu are not sufficient to express dense time control, and we need to use the modality [@) (its semantics is defined in the research report mentioned above). The formula X1 defined as follows expresses the existence of a dense-time controller for the train crossing:

X1 = (*:ON => gate:CLOSE) ^ [App] X1 ^ [i] X1 ^ [Exit] (z in X2) ^ X1 [@) ( < ac > X1) ;

X2 = (gate:OPEN ^ X1) v ((*:ON => gate:CLOSE) ^ z < 50 ^ [Exit] (z in X2) ^ [i] X2 ^ [App] X1 ^ X2 [@) ( < ac > X2))

Indeed the formula holds for (Train | Train | Gate | C ) : there exists a controller for the system w.r.t. the properties P1 and P2. Note that such a controller would be more efficient than the one presented in the previous section because it opens the gate sooner after the reception of an Exit signal.

Note that this formula ensures the existence of a controller, it does not provide it (see the research report for a discussion about this point).

The file of this example is available here

Consider the following automaton:

The aim is to avoid the state "bad". Clearly there is a strategy for this. It is sufficient to let time elapse during T time units with 10 < T < 15 and then perform the controllable transition c.

The existence of a dense-time controller is done by using a selfloop automaton performing c actions separated by at least D t.u. And we can verify the following formula over the system:

X1 = - P:BAD ^ [a] X1 ^ X1 [@) (- P:BAD ^ [a] X1 ^ < c > X1)

This allows us to show that there exists a dense time controller for D = 8.

X1 = - P:BAD ^ [a] X1 ^ ([c] ff v < c > X1) ^ [@] X1

In this case the power of the controller for the time elapsing is fixed in the self-loop automaton where the controllable actions are performed exactly every D t.u. Note that we add an dummy action eps in case where no active controllable action has to be performed at time D.

For the sampling control, we can show that no controller exist for D=8, but it is possible when D=3 for example. Clearly dense-time control is more general than sampling control.

Here the files for these examples: dense time and sampling

fl at lsv.ens-cachan.fr