WeakUntil Operator

[BentleyJOakes]

Thanks for the tool.

Is it possible for the WeakUntil operator to be added to RTAMT? My research utilizes a mapping of specification patterns to STL (from [1]), and this mapping uses WeakUntil for quite a few patterns.

For example, Before R, Existence of P -> ¬R W (P ∧ ¬R)

Of course, the WeakUntil transforms as: A W B -> Always(A) or A Until B, so this is semantic sugar. But it would be preferable on my side to move this complexity down into the RTAMT library.

Thanks for your time.
Bentley

[1] M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, and A. Tang, “Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar,” IEEE Transactions on Software Engineering, vol. 41, no. 7, pp. 620–638, 2015.

Edit: Fixed Always(B) to Always(A)

[nickovic]

You are welcome, and I apologize for the late answer, I had an important project deadline.

Thanks for the pointer to the specification patterns, I was not aware of this paper.

The short answer is yes, we can (and should) implement the weak until.

The long answer is slightly more complicated. RTAMT has been mainly targeting so far online monitoring. For online monitors, we allow only future temporal operators that are bounded in time (so that we can resolve the non-determinism by delaying the time of evaluation of the formula). Hence, for online monitors, we do not allow unbounded future temporal operators (except always and eventually, but only if they are the top operator in the formula).

On the other hand, we are planning to also support offline monitors, since all the infrastructure to do it is there. We already support them to some extent, but right now the offline monitors just call the online monitoring procedure. We want a clearer separation between the two, and a proper (more efficient) offline monitoring implementation that does not call the online procedure. This is where I see the implementation of weak until would fit.

My plan is to do this by the end of August/mid Septermber.

Your feedback is welcome.

[BentleyJOakes]

Thanks for your response.

First, yes I definitely see the value in separating the offline and online monitoring for specialization and efficiency. I expect to use both approaches in my work.

However, I don't see why the WeakUntil operator would not be relevant for both the online and offline monitoring approaches. Yes, as you correctly mention, it would have to be time-bounded for the online monitoring, but it is still valid semantic sugar for both approaches.

From some quick reasoning, perhaps it would simply be: A W[t1, t2] B -> Always[t1,t2](A) or A Until[t1,t2] B?

This time-bounded version should be sufficient for the use of the patterns in my (off-line) usage. I could set the time range to be the length of the trace, and this should provide the correct semantics.

[nickovic]

I agree and I can add the bounded weak until this week.

[nickovic]

The unless operator is added to the library.