Trace expressions are a compact and expressive formalism initially devised for runtime verication of multiagent systems, and then adopted for runtime verication of object oriented systems and of Internet of Things applications. In this paper we survey dierent logics to cope with time intervals, and we exploit the ideas underlying these logics to extend the trace expressions formalism with the explicit management of time.
Alice and Bob will attend CILC 2019: they agree to meet in front of the CILC venue between 9.00 AM and 9.20 AM, and enter the building together. Bob is always on time. He knows that Alice tends to be late, so he points out that if she will not be there between 9.00 AM and 9.20 AM, he will enter, without waiting for her. Entering the venue makes sense only before 11.00. So if Alice is late, but not too late, she enters as soon as she reaches the venue. If she is too late, she gives up attending that session.
We may formally specify the agreement between Alice and Bob in the following way: Agreement = (bob_on_time : ) j (Alice_on_time _ Alice_standard_delay _ Alice_except_delay) where ? Work supported by EPSRC as part of the ORCA [EP/R026173] and RAIN [EP/R026084] Robotics and AI Hubs.
We use italic to denote expressions and sub-expressions that represent the agreement, and that are dened by equations that could be recursive 3; we use lowercase strings to denote the types of events that are expected to take place.
To grasp the intuition behind the above formalization, we need to gently introduce the operators appearing therein, and to better clarify the notion of types of events that are expected to take place.
ev_type:Expr means that an event whose type is ev_type takes place before the events modelled by Expr. The empty expression is represented by , hence ev_type: means that after an event with type ev_type took place, nothing more should happen. The operator shue j applies to two expressions, and means that the events taking place in the left expression can be interleaved in whatever way with those in the right expression (but the event order within the two expressions must be preserved). The operator _ denotes mutually exclusive choice between two expressions, and Expr1 Expr2 means that after the events modelled by Expr1 took place, then those in Expr2 will start to take place (concatenation).
Now let us move to better shaping the meaning of bob_on_time. Bob is on time if he reaches the CILC venue between 9.00 AM and 9.20 AM; many real events match this type, where the interval of validity must be explicitly specied. We can state that bob_on_time is characterized by the actual events to be observed and the time interval when they should be observed: bob_on_time = h {bob in front of CILC venue}, [9.00 AM, 9.20 AM] i.
In the same way we can dene alice_on_time = h {alice in front of CILC venue}, [9.00 AM, 9.20 AM] i, alice_late = h {alice in front of CILC venue}, (9.20 AM, 11.00 AM] i, and alice_too_late = h {alice in front of CILC venue}, (11.00 AM, 12.00 PM] i.
We might want to model the event of being in the right place in a more detailed way. So, for example, the events B1 = bob in front of the main door of the CILC venue, B2 = bob on the external stairs of the CILC venue, B3 = bob in the main entrance of the CILC venue, might all be considered valid to state that Bob reached the CILC venue. In this case, we might dene bob_on_time = h {B1, B2, B3}, [9.00 AM, 9.20 AM] i.
The event of entering together should be associated with the interval [9.00 AM, 9.20 AM], while entering alone can take place the interval (9.20 AM, 11.00 AM] for both Alice and Bob; giving up takes place when Alice realizes she is too late; it holds in (11.00 AM, 12.00 PM].
Let us suppose the following events are observed, each associated with the time it was observed: h bob is in front of the CILC venue, 9.00 AM i, h alice is in front of the CILC venue, 9.09 AM i, h alice and bob enter together, 9.12 AM i. If a runtime monitor were in charge of verifying the Agreement, it should output yes after observing the events above.
The sequence h bob is in front of the CILC venue, 9.00 AM i, h bob enters the CILC venue alone, 9.05 AM i, h alice is in front of the CILC venue, 9.15 3 They are not in these examples, but Cheers = alice_says_hello : Cheers would be a perfectly legal expression.
AM i does not meet the Agreement, as Bob should not enter alone before 9.20 AM. The monitor should output no, or raise some alarm, in this case.
Finally, we observe that the Agreement does not even consider the possibility for Bob to be late. If Bob does not reach the venue in time, the monitor should output no as well.
In this paper we present Timed Trace Expressions, an extension of Trace
Expressions [
Background on (Interval) Temporal Logics
Many surveys on Temporal Logics exist, starting from [
In this section we summarize the works more relevant to ours; the survey is
driven by our goal, namely runtime verication [
Linear Temporal Logic, LTL
Linear Temporal Logic (LTL, [
LTL Syntax. Let AP be a set of atomic propositions: Where: a 2 AP
is for next
S is for until LTL formulae are evaluated on a sequence of states. Additional operators can be obtained by combining the ones above, like the necessity and possibility modal operators that can be expressed from a temporal point of view as: LTL Semantics. Let be an alphabet such that = 2AP . We consider an innite trace w = a0a1a2... 2 !. Let i be an LTL formula. By w[j...] we identify the sux of w starting in position j, namely aj aj+1...
w j= true w j= a w j= w j= : w j= w j= 1 S i < j 1 ^ 2 i a 2 a0
i w j= i w 2 i w[1...] j= 2 i 9j 1 and w j=
2 0 such that w[j...] j= 2 and w[i...] j= 1 for all 0 Paths can also satisfy the necessity and possibility operators.
w j= F i 9j w j= G i 8j 0 such that w[j...] j= 0, w[j...] j= LTL Models. Each LTL formula provides a set of models. Given a formula set of models can be dened as: , its L( ) = { w 2 ! | w j= } This leads to the notion of equivalence between two LTL-formulae. Let be two LTL-formulae, they are equivalent i L( ) = L( ) and we write: and
quence of states observed so far, where and
! ! ! Does the sequence satisfy ? Given that the sequence is nite, an answer based on Pnueli’s semantics, which takes innite sequences or paths into account, is hard to provide: is in fact satised if, from some time point j 0 on, becomes true. If the sequence is only a prex of a (possibly) longer sequence, where the next states are unknown so far just because they must still be observed, then it might be the case that , if in some successive observed state became true. Given that runtime verication aims monitoring the behaviour of a system, and raising errors only when these errors actually took place, the correct answer to the question above in a runtime verication setting would be it might, or it might not.... In other words, the verdict is inconclusive.
LTL3 has been proposed by Bauer, Leucker, Schallhart [
Three-Valued LTL Three-Valued Semantics Introduction. Let w be a nite word and a property. We can distinguish three situations according to what we can prove from w: holds always, even if we do not know the behaviour of the system in the future. We can evaluate on the nite word w to true (>).
will not hold in any scenario. We can evaluate on the nite word f alse (?).
Neither true nor f alse values can be determined for . We say that nite word w is inconclusive (?) on the w to Monitors. Given the LTL3 logics, we can dene runtime monitors that evaluate nite portions ( prexes ) of innite traces. The next elements of a given prex are called continuations ; the three-valued semantics can be formally dened in terms of prexes and continuations. A monitor able to evaluate a given LTL 3 formula on a nite prex can be implemented as a Finite State Machine with only three output symbols that correspond to the three truth values. The prexes will be evaluated as good or bad leading respectively to true and f alse, in the other cases they will be considered inconclusive. 2.3
Real-Time Setting
Runtime verication can be applied to systems that emit events at specic time
points. These event-triggered systems are characterized by time-stamps
associated with the events. A run of such a system leads to a timed word where each
element belongs to x IR 0. In order to cope with timed words, we need a
logic whose semantics is able to express their properties. We will consider
Metric Temporal Logic as an example of Timed Linear Temporal Logic [
Timed Words. We can write a formal denition for timed words following from
[
Metric Temporal Logic In this section we introduce Metric Temporal Logic (MTL) and Metric Interval Temporal Logic (MITL) as examples of timed logics. Many logics of this kind exist but we selected these since they are the simplest timed counterparts of LTL. As we will see, LTL and MTL share many underlying notions. MTL Syntax. Let AP be a set of atomic propositions, MTL formulae are built as: Where a 2 AP and S is the until operator we saw before.
We can see that MTL syntax is very similar to the LTL one. The big dierence lies inside I which is a an interval that can be open, closed or half open. We have that I R 0 whose left and right arguments belong to N [ {1}. If we consider: ::= we assume that I = [0, 1) which is the case of LTL formulae. Also in this case we can derive the usual next, always and eventually operators constrained by the intervals:
I F I G I = = ? SI I I > SI : I : MTL Semantics. MTL semantics can be point-based or continuous. The rst one is applied when we deal with timed events (which is our case of study) while the other is applied considering signals.
We have to recall LTL Semantics and Timed Words. We report only the semantics for the until operator for the sake of simplicity since the semantics is very similar to the LTL one.
Let = ( , ) be a timed word (where = 1 2::: is a non-empty nite or innite word and = 1 2::: is a time sequence of the same length such that each couple ( i; i) is a timed event) and a MTL formula. The satisfaction relation j= is dened as (for until operator):
j= 1 SI 2 i 9j such that 0 < j < | |, [j...] j= that 0 < k < j and ( j - 0) 2 I 2, [k...] j= 1 8k such MTL Models. Each MTL formula denes a set of models that can be classied according to their length. Let be a MTL formula. The set of nite models is dened as:
Lf ( ) = { The set of innite models is dened in the same way and is denoted by L!( ).
Recalling the properties stated in Section 2.3, the dierence between the two
sets is that all the innite words satisfy both monotonicity and progress while
the nite ones only monotonicity.
Metric Interval Temporal Logic shares both the syntax and the semantics with
MTL so we can say that it is a sort of restricted MTL. The dierence is that we
add the constraint on time intervals, in particular to what is called punctuality.
Let SI be the until operator and I = [a, b] with a, b 2 R 0. We impose that b
> a so we cannot have I = [a, a]. MITL [
x ./ a
x is a clock a is a constant ./ 2 {<, >, ,
} More formally, a TBA is a tuple ( S, S0, X, I, E, F , AP , L) where:
S0 is a set of initial states such that S0 S X is a set of clocks I: S ! X is a map that labels states into sets of clock constraints E S x X x 2X x S is a set of transitions F S is the set of nal states AP is the set of atomic propositions
L is a function that labels each state with a subset of AP So a state is a pair (s, v) with s 2 S and v is a clock valuation that satises the constraints I(s). In order to change state a timed event has to satisfy at least one clock constraint dened in the set of transitions E; the transition leads to a new state that satises its set of constraints specied by I. We can recall the concept of accepting run we saw before.
Where. MITL is used for model checking. Given a multi-agent system, we can
model each agent with timed runs. We can also model the whole system through
a collective run [
Trace Expressions
Trace expressions [
(empty trace), denoting the singleton set f g containing the empty event trace .
#: (prex ), denoting the set of all traces whose rst event ev matches the event type #, and the remaining part is a trace of .
1 2 (concatenation ), denoting the set of all traces obtained by concatenating the traces of 1 with those of 2.
1^ 2 (intersection ), denoting the intersection of the traces of 1 and 2. 1_ 2 (union ), denoting the union of the traces of 1 and 2.
1j 2 (shue ), denoting the set obtained by shuing the traces of 1 with the traces of 2.
Trace expressions support recursion through cyclic terms expressed by nite sets of recursive syntactic equations, as supported by modern Prolog systems.
The semantics of trace expressions is specied by a transition relation rTespeEctiveTly,. WwheewreriTte an1de!Ev de2ntootemtehaen s(et1;oefv;tra2c)e2ex;ptrhesesitornanssaitnidonof 1evee!vnts,2 expresses the property that the system under monitoring can safely move from the state specied by 1 into the state specied by 2 when event ev is observed. A trace expression models the current state of a protocol. Protocol state transitions are ruled by the transition system shown in Figure 1, which dene . 3.2
Timed Trace Expressions In order to constrain the set of event traces denoted by a trace expression we need a set of time constraints .
Timed Events. In Timed Trace Expressions, events are associated with the time when they have been observed. A timed event is represented by a couple hev; ti, where ev is the observed event, and t is the time stamp associated with it. (and) 1 #: ev ! 1_ 2 ev 0 ! 1 ev ! 10 1 e!v 10 ev ! 10 j 2 1_ 2 (shue-r) ( 1)
2
Example 1. Let us assume that we have an event a and we intend to model the situation where a should take place two times, the rst one in the interval [0; 5) and the second one in the interval [10; 20]. If we write a timed trace expression in this way:
A = hfag; [0; 5) [ [10; 20]i
= A : A : does not correctly model the scenario we have in mind, as the sequence ha; 1i ha; 2i respects the formal specication, but not our intuition. We point out that an event can belong to dierent timed event types; this leads to the following solution:
A = hfag; [0; 5)i B = hfag; [10; 20]i
= A : B : Example 2. We consider a more sophisticated example, where the monitor can accept an event a in dierent time intervals, and according to the timestamp of the event the execution proceeds on a dierent branch, for example by moving to 1 in one case, and by waiting for an event b in the second case, and then moving to 2. The resulting timed trace expression might look like: But this denition of is nondeterministic, as ha; 4i, as well as ha; 17i might both be accepted to move either in 1 or in B : 2. We must rewrite the trace expressions as follows, by creating a new timed event type:
A = hfag; [2; 7) [ (15; 20]i
B = hfbg; [0; 1)i = A : 1 _ A : B : 2 1 = ...something... 2 = ...something...
A = hfag; [2; 7)i B = hfbg; [0; 1)i C = hfag; (15; 20]i = A : 1 _ C : B : 2 1 = ...something...
2 = ...something...
In this case, if the monitor observes the event a with timestamp t rightmost branch must be selected to continue the monitoring. 16, the Example 3. Finally, we can note that a trace expression might be unsatisable, in the sense that no actual trace of timed events can meet the specication given by . The following simple trace exemplies this situation.
A = hfag; [5; 9)i B = hfbg; [0; 3)i
= A : B : In this trace, the temporal constraints are not consistent with respect to the properties of timed words such as monotonicity ; the : operator forces a to take place before b, but the intervals associated with A and B make this structural property of not satisable.
Discussion: limitations of Timed Trace Expressions. Examples 1 and 2 show
that the simple formalization that may come to the mind of the trace expression
designer to meet some informal specication, may easily turn out to be the
wrong one. The burden of ensuring that dierent instances of the same event
that must take place in dierent intervals are modelled by distinct event types,
insists entirely on the designer’s shoulders. When timed trace expressions are
more complex than those shown in this paper, and when they are dened in a
recursive way, the correct formalization may be dicult to specify. One possible
solution to overcome this problem, could be to associate intervals with sub-traces,
rather that with event types. In fact, intervals associated with event types have
a global scope, but in some cases it might be more convenient to have intervals
with a local scope. This extension, however, would require to change the syntax
of trace expressions (while so far we only changed the syntax of events and event
types), by introducing an explicit notion of scope of an interval, as we did with
parametric trace expressions [
The other feature that we point out, is the ability to write timed trace expressions which are useless, as their structure is non compliant with the temporal constraints therein. Given that the monitoring engine for timed trace expressions is implemented in SWI Prolog 4, we are exploring the possibility to exploit the support that SWI Prolog oers to constraint logic programming 5, to detect these design errors at compile time. 4
Conclusions and Future Work
Dierent techniques exist for denition, model checking and runtime verication
of complex, distributed systems where time plays a crucial role, such as
Temporal Logics. Interval Temporal Logic is one of the rst formalisms that had an
impact in the Multiagent System research eld even if it was born for hardware
reasoning. As the name suggests, the time is specied in terms of intervals. On
the other hand, Linear Temporal Logic is a kind of modal logic that can be used
for specifying temporal properties of the systems. It was proposed for formal
verication by Amir Pnueli [
In real-time systems it is likely that time bounded properties must be
specied: Timed Linear Temporal Logic was proposed by Raskin [
In this paper we have applied the ideas supported by the logics above to the Trace Expressions formalism, resulting into Timed Trace Expressions. 4 http://www.swi-prolog.org/, accessed on March 25, 2019. 5 http://www.swi-prolog.org/pldoc/man?section=clp, accessed on March 25, 2019.
Our future directions of research are related with overcoming the limitations
discussed in Section 3. Besides this, in [