=Paper=
{{Paper
|id=Vol-2396/paper13
|storemode=property
|title=Timed Trace Expressions
|pdfUrl=https://ceur-ws.org/Vol-2396/paper13.pdf
|volume=Vol-2396
|authors=Luca Ciccone,Angelo Ferrando,Davide Ancona,Viviana Mascardi
|dblpUrl=https://dblp.org/rec/conf/cilc/CicconeFAM19
}}
==Timed Trace Expressions==
https://ceur-ws.org/Vol-2396/paper13.pdf
Timed Trace Expressions
1 2 1 1
Luca Ciccone , Angelo Ferrando , Davide Ancona , and Viviana Mascardi
1
University of Genova, Genova, Italy,
4077756@studenti.unige.it,davide.ancona@unige.it,viviana.mascardi@unige.it
2
Liverpool University, Liverpool, United Kingdom,
angelo.ferrando@liverpool.ac.uk ?
Abstract Trace expressions are a compact and expressive formalism
initially devised for runtime veri cation of multiagent systems, and then
adopted for runtime veri cation of object oriented systems and of In-
ternet 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.
Keywords: Timed Temporal Logic, Timed Trace Expressions, Runtime
Veri cation
1 Introduction and Motivation
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 fol-
lowing way:
Agreement = (bob_on_time : ) |
(Alice_on_time ∨ Alice_standard_delay ∨ Alice_except_delay)
where
Alice_on_time = (alice_on_time : alice_and_bob_enter_together : )
Alice_standard_delay = (alice_late : ((bob_enters : ) | (alice_enters : )))
Alice_except_delay = (alice_too_late : ((bob_enters : ) | (alice_gives_up : )))
?
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
3
agreement, and that are de ned by equations that could be recursive ; 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 shu e | 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
speci ed. 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 de ne 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 de ne 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 [3,4,5] with time constraints. Timed Trace Expressions can be used
to formalize the above Agreement between Bob and Alice. Given that the the-
oretical underpinning of this extension is given by Interval Temporal Logic and
Metric Interval Temporal Logic, we present a survey of Temporal Logics for-
malisms in Section 2. Section 3 introduces Timed Trace Expressions, and Section
4 concludes and outlines the future directions of our work.
2 Background on (Interval) Temporal Logics
Many surveys on Temporal Logics exist, starting from [10,16] and moving to
more recent works like [8,14,18], which take time and intervals into account.
In this section we summarize the works more relevant to ours; the survey is
driven by our goal, namely runtime veri cation [12] of distributed systems in
general, and of multiagent systems [11,19,20] in particular.
2.1 Linear Temporal Logic, LTL
Linear Temporal Logic (LTL, [15]) does not deal with discrete time intervals,
but introducing its syntax and semantics is a step forward introducing Timed
Temporal Logic and Metric Temporal Logic in the sequel. LTL nds it main
application in model checking [6]. In order to use LTL for runtime veri cation,
it was extended to LTL3 [7].
LTL Syntax. Let AP be a set of atomic propositions:
S
φ ::= true | a | φ1 ∧ φ2 | ¬ φ | φ | φ1 φ2
Where:
a ∈ AP
S is for next
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:
Fφ (♦ φ) ≡ true φS
S
Gφ ( φ) ≡ ¬(true ¬ φ)
LTL Semantics. Let Σ be an alphabet such that Σ = 2AP . We consider an
in nite trace w = a0 a1 a2 ... ∈ Σ ω . Let φi be an LTL formula. By w[j...] we
identify the su x of w starting in position j , namely aj aj+1 ...
w |= true
w |= a i a ∈ a0
w |= φ1 ∧ φ2 i w |= φ1 and w |= φ2
w |= ¬ φ i w 2 φ
w |= φS i w[1...] |= φ
w |= φ1 φ2 i ∃j ≥ 0 such that w [j ...] |= φ2 and w [i...] |= φ1 for all 0
≤i).
φ will not hold in any scenario. We can evaluate φ on the nite word w to
f alse (⊥).
Neither true nor f alse values can be determined for φ. We say that φ on the
nite word w is inconclusive (?)
Monitors. Given the LTL3 logics, we can de ne runtime monitors that evaluate
nite portions (pre xes ) of in nite traces. The next elements of a given pre x are
called continuations ; the three-valued semantics can be formally de ned in terms
of pre xes and continuations. A monitor able to evaluate a given LTL3 formula
on a nite pre x can be implemented as a Finite State Machine with only three
output symbols that correspond to the three truth values. The pre xes 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 veri cation can be applied to systems that emit events at speci c time
points. These event-triggered systems are characterized by time-stamps associ-
ated with the events. A run of such a system leads to a timed word where each
≥0
element belongs to Σ x IR . In order to cope with timed words, we need a
logic whose semantics is able to express their properties. We will consider Met-
ric Temporal Logic as an example of Timed Linear Temporal Logic [17] which
is a variant of LTL.
Timed Words. We can write a formal de nition for timed words following from
[1]. A timed word w over the alphabet Σ is a sequence (a0 , t0 )(a1 , t1 )... where
each (ai , ti ) is a timed event ∈ Σ x IR≥0 such that:
∀i ∈ N we have that ti < ti+1 (strict monotonicity )
if w is in nite, ∀t ∈ IR≥0 ∃i ∈ N with ti > t (progress )
Starting from the considerations we made in the previous sections, we need to
deal with in nite words. In case of a nite timed word w = (a0 , t0 )(a1 , t1 )...(ai ,
ti ), its continuations are the timed words that start with (ai+1 , ti+1 ) such that
ti+1 > ti
Where. Timed logics are useful every time the crucial point of the analysis is the
time. For example we can consider a distributed, asynchronous system in which
we want to model not only the single elements but also the whole system.
2.4 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:
S
φ ::= true | a | φ1 ∧ φ2 | ¬ φ | φ1 I φ2
S
Where a ∈ AP and is the until operator we saw before.
We can see that MTL syntax is very similar to the LTL one. The big dier-
ence 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 ∪ {∞}. If
we consider:
S
φ ::= φ1 φ2
we assume that I = [0, ∞) 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 φ≡⊥ I φ S
S
FI φ = ♦I φ ≡ > I φ
GI φ = I φ ≡ ¬♦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 se-
mantics 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
in nite 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 ρ |= φ is de ned as (for until operator):
ρ |= φ1
S
I φ2 i ∃j such that 0 < j < |ρ|, ρ[j ...] |= φ2 , ρ[k ...] |= φ1 ∀k such
that 0 < k < j and (τj - τ0 ) ∈ I
MTL Models. Each MTL formula de nes a set of models that can be classi ed
according to their length. Let φ be a MTL formula. The set of nite models is
de ned as:
Lf (φ) = {ρ ∈ (Σ x R≥ 0 ) : ρ |= φ}
The set of in nite models is de ned 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 in nite words satisfy both monotonicity and progress while
the nite ones only monotonicity.
2.5 Metric Interval Temporal Logic
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.
until operator and I = [a, b] with a, b ∈ R≥ 0 . We impose that b
S
Let I be the
> a so we cannot have I = [a, a]. MITL [2] was introduced since MTL models
cannot be translated into automata, as we did for LTL. In this case we can
introduce Timed Büchi Automata in which we have to add time constraints.
Timed Büchi Automaton. A Timed Büchi Automaton, TBA, in an extension of
[9] in which we add clock constraints.
De nition (Clock Constraints) A clock constraint is a conjunctive formula
x ./ a
Where:
x is a clock
a is a constant
./ ∈ {<, >, ≤, ≥}
More formally, a TBA is a tuple (S , S0 , X , I , E , F , AP , L) where:
S is a set of states
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 ∈ S and v is a clock valuation that satis es the
constraints I (s). In order to change state a timed event has to satisfy at least
one clock constraint de ned in the set of transitions E ; the transition leads to
a new state that satis es its set of constraints speci ed 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 [13].
3 Timed Trace Expressions
In this section we discuss how to extend Trace Expressions with time intervals.
We rst summarize the Trace Expressions formalism, and then we present its
extension, along with examples.
3.1 Trace Expressions
Trace expressions [3,4,5] are based on the notions of event and event type. We
denote by E the xed universe of events subject to monitoring. An event trace
over E is a possibly in nite sequence of events in E , and a trace expression over
E denotes a set of event traces over E . Trace expressions are built on top of event
types (chosen from a set ET ), each specifying a subset of events in E . A trace
expression τ ∈ T represents a set of possibly in nite event traces, and is de ned
on top of the following operators, some of which have already been introduced
in Section 1:
• (empty trace), denoting the singleton set {} containing the empty event
trace .
• ϑ:τ (pre x ), 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 .
• τ1 |τ2 (shu e ), denoting the set obtained by shu ing 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 speci ed by a transition relation δ ⊆
T × E × T , where T and E denote the set of trace expressions and of events,
ev ev
respectively. We write τ1 −→ τ2 to mean (τ1 , ev, τ2 ) ∈ δ ; the transition τ1 −→ τ2
expresses the property that the system under monitoring can safely move from
the state speci ed by τ1 into the state speci ed 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 de ne δ .
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.
ev ev
τ1 −→ τ10 τ2 −→ τ20
(pre x) ev ev∈ϑ (or-l) ev (or-r) ev
ϑ:τ −→ τ τ1 ∨τ2 −→ τ10 τ1 ∨τ2 −→ τ20
ev ev ev ev
τ1 −→ τ10 τ2 −→ τ20 τ1 −→ τ10 τ2 −→ τ20
(and) ev (shu e-l) ev (shu e-r) ev
τ1 ∧τ2 −→ τ10 ∧τ20 τ1 |τ2 −→ τ10 |τ2 τ1 |τ2 −→ τ1 |τ20
ev ev
τ1 −→ τ10 τ2 −→ τ20
(cat-l) ev (cat-r) ev (τ1 )
τ1 ·τ2 −→ τ10 ·τ2 τ1 ·τ2 −→ τ20
Figure 1. Operational semantics of trace expressions
Timed Event Types. Time constraints must be also associated with event types
which become couples as well:
ϑ = h ξϑ , Cϑ i
where the rst element denotes a set of events while the second one is a conjunc-
tion of time intervals, identifying all the time instants where an event ev ∈ ξϑ
can be observed, to match the event type ϑ.
With respect to trace expressions, the only modi cation in timed trace ex-
pressions lies in the notions of events and event types, and in the de nition of
when an event belongs to an event type, which is given pairwise on the two
elements of the couples: h ev , t i ∈ h ξϑ , Cϑ i i ev ∈ ξϑ and t ∈ Cϑ .
By default, any event type is de ned in the interval [0, ∞). This provides a
means to transform each trace expression into a timed one, just by associating
this interval to each event type.
The semantics is the same as that of trace expressions.
This extension is extremely simple, and if fact the implementation of a timed
monitor driven by a timed trace expression comes almost for free, by extending
the existing Prolog implementation of the non-timed monitor. This simplicity
has one major drawback described by Examples 1 and 2 below.
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 = h{a}, [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 speci cation, but not our intuition. We point out that
an event can belong to dierent timed event types; this leads to the following
solution:
A = h{a}, [0, 5)i
B = h{a}, [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:
A = h{a}, [2, 7) ∪ (15, 20]i
B = h{b}, [0, ∞)i
τ = A : τ1 ∨ A : B : τ2
τ1 = ...something...
τ2 = ...something...
But this de nition 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 = h{a}, [2, 7)i
B = h{b}, [0, ∞)i
C = h{a}, (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 ≥ 16, the
rightmost branch must be selected to continue the monitoring.
Example 3. Finally, we can note that a trace expression τ might be unsatis -
able, in the sense that no actual trace of timed events can meet the speci cation
given by τ . The following simple trace exempli es this situation.
A = h{a}, [5, 9)i
B = h{b}, [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 satis able.
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 speci cation, 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 de ned in a
recursive way, the correct formalization may be di cult 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 [5] for the notion of scope of a parameter. This
would also require a change in the semantics.
The other feature that we point out, is the ability to write timed trace expres-
sions which are useless, as their structure is non compliant with the temporal
constraints therein. Given that the monitoring engine for timed trace expres-
4
sions is implemented in SWI Prolog , we are exploring the possibility to exploit
5
the support that SWI Prolog oers to constraint logic programming , to detect
these design errors at compile time.
4 Conclusions and Future Work
Dierent techniques exist for de nition, model checking and runtime veri cation
of complex, distributed systems where time plays a crucial role, such as Tem-
poral 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 speci ed 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
veri cation by Amir Pnueli [15] and it was extended to LTL3 by Bauer, Leucker,
Schallhart [7] for runtime veri cation.
In real-time systems it is likely that time bounded properties must be spec-
i ed: Timed Linear Temporal Logic was proposed by Raskin [17] and it is the
counterpart of LTL for timed words. As for LTL, Timed LTL can be extended for
runtime veri cation (TLTL3 , [7]). Metric Temporal Logic is another example of
Timed Logic: a subset of MTL, which is called Metric Interval Temporal Logic,
is usually considered due to its good decidability properties.
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 [4] we demonstrated that an LTL formula
(with LTL3 semantics) can be translated into an equivalent Trace Expression
passing through the concept of Büchi Automaton. We aim at investigating if the
same procedure can be applied to TLTL3 and Timed Trace Expressions through
Timed Büchi Automata.
References
1. R. Alur and D. L. Dill. A theory of timed automata. Theor. Comput. Sci.,
126(2):183235, 1994.
2. R. Alur, T. Feder, and T. A. Henzinger. The bene ts of relaxing punctuality. In
L. Logrippo, editor, Proceedings of the Tenth Annual ACM Symposium on Prin-
ciples of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991,
pages 139152. ACM, 1991.
3. D. Ancona, A. Ferrando, L. Franceschini, and V. Mascardi. Parametric trace
expressions for runtime veri cation of Java-like programs. In FTfJP@ECOOP,
pages 10:110:6. ACM, 2017.
4. D. Ancona, A. Ferrando, and V. Mascardi. Comparing trace expressions and linear
temporal logic for runtime veri cation. InTheory and Practice of Formal Methods,
volume 9660 of LNCS, pages 4764, 2016.
5. D. Ancona, A. Ferrando, and V. Mascardi. Parametric runtime veri cation of
multiagent systems. In K. Larson, M. Winiko, S. Das, and E. H. Durfee, editors,
Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Sys-
tems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017, pages 14571459. ACM,
2017.
6. C. Baier and J.-P. Katoen. Principles of model checking. MIT press, 2008.
7. A. Bauer, M. Leucker, and C. Schallhart. Runtime veri cation for LTL and TLTL.
ACM Trans. Softw. Eng. Methodol., 20(4):14:114:64, 2011.
8. P. Bellini. Interval temporal logic for real-time systems: Speci cation, execution
and veri cation processes. PhD. Thesis, University of Florence, Italy, 2001.
9. J. R. Büchi. On a decision method in restricted second order arithmetic. In
Proceedings of the International Congress on Logic, Methodology and Philosophy
of Science. Stanford University Press, 1962.
10. T. A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J. W.
de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors, Real-Time:
Theory in Practice, REX Workshop, Mook, The Netherlands, June 3-7, 1991,
Proceedings, volume 600 of Lecture Notes in Computer Science, pages 226251.
Springer, 1991.
11. N. R. Jennings, K. P. Sycara, and M. Wooldridge. A roadmap of agent research
and development. Autonomous Agents and Multi-Agent Systems, 1(1):738, 1998.
The Journal
12. M. Leucker and C. Schallhart. A brief account of runtime veri cation.
of Logic and Algebraic Programming, 78(5):293303, 2009.
13. A. Nikou, J. Tumova, and D. V. Dimarogonas. Cooperative task planning of multi-
agent systems under timed temporal speci cations. In 2016 American Control
Conference, ACC 2016, Boston, MA, USA, July 6-8, 2016, pages 71047109. IEEE,
2016.
14. J. Ouaknine and J. Worrell. Some recent results in metric temporal logic. In
F. Cassez and C. Jard, editors,Formal Modeling and Analysis of Timed Systems,
6th International Conference, FORMATS 2008, Saint Malo, France, September 15-
17, 2008. Proceedings, volume 5215 of Lecture Notes in Computer Science, pages
113. Springer, 2008.
15. A. Pnueli.The temporal logic of programs. In Proceedings of the 18th Annual
Symposium on Foundations of Computer Science (FOCS'77), pages 4657. IEEE
Comp. Soc. Press, 1977.
16. A. Pnueli. Applications of temporal logic to the speci cation and veri cation of
reactive systems: A survey of current trends. In J. W. de Bakker, W. P. de Roever,
and G. Rozenberg, editors, Current Trends in Concurrency, Overviews and Tuto-
rials, volume 224 of Lecture Notes in Computer Science, pages 510584. Springer,
1986.
17. J.-F. Raskin. Logics, automata and classical theories for deciding real-time. PhD.
Thesis, Facultés universitaires Notre-Dame de la Paix, Namur, 1999.
18. F. Wang. Formal veri cation of timed systems: A survey and perspective. Pro-
ceedings of the IEEE, 92(8):12831305, 2004.
19. M. Wooldridge and N. R. Jennings, editors. Intelligent Agents, ECAI-94 Workshop
on Agent Theories, Architectures, and Languages, Amsterdam, The Netherlands,
August 8-9, 1994, Proceedings, volume 890 of Lecture Notes in Computer Science.
Springer, 1995.
20. M. Wooldridge and N. R. Jennings. Intelligent agents: theory and practice. Knowl-
edge Eng. Review, 10(2):115152, 1995.