MITL queries in UPPAAL SMC

[Raghav G]

Hi all,

I haven't been able to come up with strong probabilistic queries in UPPAAL SMC. There are some properties(through queries) which I would like to check in UPPAAL SMC. These are:

1) I understand that the deadlock and livelock properties which requires a complete state space exploration cannot be performed using SMC with random() function. Does anyone have any suggestions on how we can handle such queries with random() function? Can we use reachability properties or other properties to check for deadlocks in the system(May not be exhaustive though)? 

2) I was trying to form a query to check on occurrence of a transition, but I haven't been successful on this. For example, there are two transitions A and B. I want to write a query to check if B always happens only after A, but also always before the next occurrence of A. It would be really great if you could provide some suggestions on this. I setup a counter for each of the transition and tried  to check if value of counterA is greater than counterB when B transition happens. Similarly, to check if value of counterB is greater than counterA when A transition happens.

This works to a little extent, however I feel this is very cumbersome and maybe we can do this in a better way with forall. However, everytime I use forall something roughly like this: Pr[<=1000] (forall(counterA : int) (<> Model.counterA imply Model.B imply (Model.counterA +1)), I get a syntax error and I am not able to get past this. Does anyone have any suggestions on this?

3) Liveness properties to specify something like when A happens, B eventually happens (such as A --> B) does not work when random() function is used. So, this coerces us to use a weaker alternative which is "A imply B". However, this doesn't help much since both (A imply B) and also (A imply not B) have the same probabilistic value of 0.99. How do you specify liveness properties such as these in UPPAAL SMC?

4) I am trying to compute the Worst case response time(WCRT) for a signal in UPPAAL SMC. I am able to simulate and find the variable value(but I can't pin point the exact maximum value in there). Other options are to use Supremum or find maximum value using E[#<=10000;10000](max:ClockTB). However, when using Supremum you cannot use a random() function, but I do have a random() function and so, I cannot use Supremum. When I try using E[#<=10000;10000](max:ClockTB), it gives the value as 0 which is incorrect. So, could you please let me know how we can obtain the worst case response time for a signal in UPPAAL?

5) There are very limited examples on nested queries in MITL in UPPAAL. I have found only one paper which covers nested queries. Do you have any pointers towards how we can make nested queries in MITL for UPPAAL SMC?

It would be really great if someone could help me with these queries since I have been working on this for quite some time and I am not able to get this done. So, any assistance on this would be much appreciated!

Thanks in advance!