Strategy synthesis with UPPAAL STATEGO (Version 4.1.20-7)

[Antje Rogalla]

For some time we have been working with UPPAAL STRATEGO and the possibility to generate strategies. We have noticed some points which are not quite clear to us.

1. Output of the verifier in case of optimal strategies
Find attached our simple stayHealthy model. If we check strategy StayHealthy = control: A<> M.StayHealthy using the verifier, we get the result true: green button. Although optimal strategies in case of time bound 40 and 200 exist, we get the result false (red button) for optimal strategy generation minCost1 and minCost2 using the verifier. Nevertheless, we can generate those optimal strategies correctly using the command line. These optimal strategies will only be generated, if we exclude the timelock automaton from the system in the system declaration. If we add the timelock automaton to the system (with no impact on the strategy generation of the StayHealthy model) using the command line, we get the same error message as in the verifier and optimal strategies will not be generated.

In which case can UPPAAL generate optimal strategies and in which not?

2. Message: State is time-locked
If we check strategy minCost1 using the verifier, we get the message State M.SanitizerAtMarket is time-locked, but only one path starts in state M.SanitizerAtMarket and this path is infinite and time-divergent.

Why does M.SanitizerAtMarket contain a timelock according to the UPPAAL?

3. Strategy generation under another strategy generation
Strategies LowCost = control: A[] cost <= 30 and ShortTime = control: A[] T <= 40 exist and the correct strategies are generated. The strategies StayHealthyUNDERLowCost and StayHealthyUNDERShortTime exist, that is correct, but the generated strategies are equal to the strategie StayHealthy, which is wrong. Therefore by "under" we can generate strategies, which are no winning strategies and should not exist (see strategy LowCostUNDERStayHealthyUNDERShortTime). On the contrary, the strategy generation of LowCostUNDERStayHealthy and ShortTimeUNDERStayHealthy works correctly.

Why does the strategy generation with under work correctly under the reachability property A<> M.StayHealthy but not under another property specifications as A[] cost <= 30?

Thank you for your help!