# How to verify a property about a certain order of events in TCTL / UPPAAL?

I'd like to check if a certain order of events happens if another property holds true using UPPAAL and TCTL.

If A==true then eventually (B==true and eventually (C==true and eventually (D==true)))

But since "In contrast to TCTL, Uppaal does not allow nesting of path formulae." I'm not sure how to do this.

What I'v got so far is only something like:

E$\diamond$ (A && B)

E$\diamond$ (A && C)

E$\diamond$ (A && D)

Under the assumption that your property can be interpreted in an intuitive way, as it is written, it seems that you can formulate it both in LTL, as:

a => F(b && F(c && F d))


and in CTL, which in the given example is equivalent to TCTL, due to lack of timing constraints (you may assume they are of form [0, inf) and consider a TCTL formula as a CTL formula), as:

a => AF(b && AF(c && AF d))


but not in the logic supported in UPPAAL. Your property requires nested quantifiers, which are not supported in UPPAAL (as you suggested).

In general, it is not possible to model properties like a => F b ("whenever a is true, b should be true eventually") directly in UPPAAL. A workaround that might work is to consider all states in which a holds as the initial states and then formulate and check AF b. Of course, since you have multiple of such nested formulas, this does not seem possible in your case. Note that such properties require that for all reachable states X where a is true, there should be a state y (reachable from X), such that b is true in y (which does not fall into category of supported classes of properties in UPPAAL such as "liveness" and "safety").

Since you are trying to express a property that requires a nested CTL formula, UPPAAL is not suitable to formulate and model-check it. You should try SPIN or other tools that support full CTL.