TSMV
The bridge crossing problem

This example illustrates how TSMV is efficient at dealing with long durations.

The problem

The bridge-crossing problem is a famous mathematical puzzle with time critical aspects [Rot02]. A group of four persons, called P1, P2, P3 and P4, have to cross a bridge at night. It is dark and they can only cross the bridge if they carry a lamp. Only one lamp is available and at most two persons can cross at the same time. Therefore any solution requires that, after the first two persons cross the bridge, one of them returns, bringing back the lamp with him for the remaining people. The four persons have different maximal speeds: here P1 crosses in 5 time units (t.u.), P2 in 10 t.u., P3 in 20 t.u. and P4 in 25 t.u. When a pair crosses the bridge, they move at the speed of the slowest person in the pair. Now, how much time is required before the whole group is on the other side?

A person is described as an SMV module with his crossing time as a parameter. His possible steps are to stay where he is, or move to the other side. He can only cross when the lamp is on his side (and then the lamp crosses with him). When he crosses, the transition takes at least his crossing time. This way, when four persons are synchronized, the crossing time is any integer greater or equal to the maximum crossing time of the crossing persons. The complete system is obtained by combining four persons (four instances of the same person module, with different crossing times) with a Boolean lamp value keeping track of the position of the lamp, and adding a further constraint (an INVAR in SMV) telling that at most two persons cross in one move. The system is further labeled with two propositions: initial for the initial configuration, and safe for the configurations where everyone is on the other side of the bridge.

We can ask how much time is required for crossing:

	COMPUTE MIN[initial, safe]
The answer (60 t.u.) is obtained in a few milliseconds. The bridge example readily gives rise to many variants with more than four persons, with different crossing times, and where a larger number of persons can cross in the same step.

We ask

	SPEC  AG EF<=60 safe
and get a negative answer: in some reachable configurations, more than 60 t.u. are required.

Indeed, if we start after just one person has crossed, that person will have to come back before we can implement the 60 t.u. solution. Hence 85 t.u. (=25+60) are sometimes required. We check that this is indeed the worst case with

	SPEC  (AG EF<=85 safe) & !(AG EF<=84 safe)

Comparison with NuSMV

The same example can be treated with NuSMV. This is easy since the example does not use zero-length steps. For long steps, we use the method advocated in [CC01] and introduce a counter forcing several t.u. between actual system moves. It can be argued that this model is slightly more cumbersome.

The answer 60 t.u. for COMPUTE MIN[initial, safe] is obtained a little less quickly than with TSMV (see table below).

When verifying SPEC (AG EF<=85 safe) & !(AG EF<=84 safe) we obtain a negative answer! This is because the models are different. In fact, the NuSMV encoding describes a different TKS, where all intermediate positions exists along what should be long steps. The AG modality quantifies over these intermediate positions too. The intended semantics can be recovered by adapting the TCTL formula. The new formula relies on a new inbetween proposition that has to be added: it labels the intermediate configurations that should not exist in the TKS. The resulting formula

	SPEC  AG (!inbetween -> EBF 0..85 (safe & !inbetween))
is satisfied.

TSMV and sensitivity to scaling up the durations

The bridge problem is an example of a system where durations are mostly ``long'' (greater than 1). The algorithms used in TSMV are designed in such a way that only useful durations are considered [MS03] (we were influenced by the complexity analysis in [LMS02]). As a result, TSMV is mostly insensitive to scaling up the durations. Assume that we define a model ``bridge x 10'' by replacing 5, 10, 20 and 25 with (resp.) 50, 100, 200, and 250, TSMV computes the minimum delay of 600 t.u. in more or less the same time it needed for the initial problem

This must be contrasted with nuSMV behavior. When we scale up the durations, the computation time increases dramatically. In fact, there is no way to avoid this: nuSMV does not know about TKS's and is bound to compute all sets associated with different values of the counter for intermediate states. Computing these sets is a tedious and mostly repetitive task that cannot be avoided unless a notion of TKS is introduced.

The following table shows how running time and memory requirements (for the COMPUTE MIN statement only) grow when we scale up the timing parameters of the bridge problem of TSMV. Observe that the TKS defined with bridge x 10 is not exactly a scaling up of bridge since we use conditions of the form ``duration >= 100'' that allow all values 100, 101, 102, ...

NuSMV TSMV
time memory time memory
bridge 0.13 sec.9112 KB0.02 sec.1284 KB
bridge x 10 4.14 sec.18860 KB0.04 sec.1284 KB
bridge x 20 22.44 sec.19508 KB0.07 sec.1288 KB
bridge x 50 176.55   sec.28640 KB0.22 sec.9920 KB
bridge x 100844.25   sec.50964 KB0.45 sec.11580 KB
bridge x 2004889.93   sec.98212 KB1.03 sec.14956 KB

In order to be really closer to a scale up of the initial model, we can specify that the time step can be the gcd of all crossing times (for instance, in "bridge x 20", crossing times are 100, 200, 400 and 500, and their gcd is 100). In the case of NuSMV, when using timing requirements, we must then multiply the result by the gcd of all crossing times in order to find the real result. We then get the following time and memory usage when computing the minimum total crossing time:

NuSMV TSMV
time memory time memory
bridge0.03 sec.1280 KB0.02 sec.1280 KB
bridge x 100.12 sec.8716 KB0.03 sec.1280 KB
bridge x 200.47 sec.8948 KB0.04 sec.1280 KB
bridge x 503.24 sec.11260 KB0.07 sec.1280 KB
bridge x 10012.65 sec.11260 KB0.12 sec.9236 KB
bridge x 20050.75 sec.14240 KB0.26 sec.10168 KB
This demonstrates why long durations should not be replaced by sequences of unit-steps (unless one really depends on the precise branching-time semantics associated with intermediary states).

Download model files

Bibliography

[CC01]         Sergio Campos and Edmund Clarke. The Verus language: representing time efficiently with BDDs. Theoretical Computer Science, 253(1):95-118, February 2001.
[LMS02]         François Laroussinie, Nicolas Markey and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (extended abstract). In Proc. 5th Int. Conf. Foundations of Software Science and Computation Structures (FoSSaCS'2002), Grenoble, France, Apr. 2002, volume 2303 of Lecture Notes in Computer Science, pages 264-279. Springer, 2002.
[MS03]         Nicolas Markey and Philippe Schnoebelen. Symbolic Model Checking of Simply-Timed Systems. Research Report LSV-03-14, Lab. Specification and Verification, ENS de Cachan, Cachan, France, October 2003.
[Rot02]         Günter Rote. Crossing the bridge at night EATCS Bulletin, 78:241-246, October 2002.

About LSV