How to verify a property about a certain order of events in TCTL / UPPAAL?
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 =&gt; F(b &amp;&amp; F(c &amp;&amp; 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 =&gt; AF(b &amp;&amp; AF(c &amp;&amp; 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 =&gt; 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.