Strategy synthesis with UPPAAL-5.0.0 - Questions regarding TCTL winning conditions AW and AU

[antjero...@gmail.com]

Hi,

I have some questions regarding the range of TCTL winning conditions that UPPAAL (Stratego) supports. I use UPPAAL-5.0.0.

I created two simple example models, "ABC with loop" and "ABC without loop." For simplification, both automata do not have uncontrollable edges to visualize and demonstrate my questions. However, similar scenarios are reproducible for more complex timed games, e.g., the traffic model.

For the timed automaton ``ABC with loop``, I tried to generate entire strategies (I used the option 'entire winning strategy over all states') for the following winning conditions:

1.  A[ABC.A W ABC.B]
2. A[!ABC.C W ABC.B]
3. A[ABC.A U ABC.B]
4. A[!ABC.C U ABC.B]
5. A<> ABC.B
   

I attached screenshots of the model ABC_with_loop and the verifier output ABC_with_loop_verfier_output.

For the timed automaton "ABC without loop," I attempted to generate a strategy for the following winning A[ABC.A W ABC.B]. Uppaal does not generate a strategy, even if B is reachable after a delay of 1 in the initial location A. 

I attached screenshots of the model ABC_without_loop and the verifier output ABC_without_loop_verfier_output.

My questions are:

1. In the case of  A[ABC.A W ABC.B], UPPAAL seems to generate the strategy for A[] ABC.A. Why does the entire strategy not include the strategies for A[ABC.A U ABC.B] (the state transition to B)?
2. Why does Uppaal not generate a strategy for the winning condition A[ABC.A U ABC.B]? 
   If the Predecessor of the AU formula starts with a negation, UPPAAL generates a correct and entire strategy. 
3. For the winning condition A <> ABC.B, Uppaal generates the entire strategy correctly. However, due to the structure of the input model, the strategy includes one infinite loop that avoids reaching location B. Have you conducted any research on avoiding infinite loops in Uppaal strategies?
   

Thanks in advance for your feedback!