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 verication of multiagent systems, and then adopted for runtime verication 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 Verication 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 dened 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 shue | 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 [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 verication [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 verication, 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 innite trace w = a0 a1 a2 ... ∈ Σ ω . Let φi be an LTL formula. By w[j...] we identify the sux 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 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 LTL3 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 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 denition 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 innite, ∀t ∈ IR≥0 ∃i ∈ N with ti > t (progress ) Starting from the considerations we made in the previous sections, we need to deal with innite 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 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 ρ |= φ is dened 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 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 (φ) = {ρ ∈ (Σ x R≥ 0 ) : ρ |= φ} 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. 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. Denition (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 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 [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 innite 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 innite event traces, and is dened 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 . • ϑ:τ (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 . • τ1 |τ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 δ ⊆ 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 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. ev ev τ1 −→ τ10 τ2 −→ τ20 (prex) 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 (shue-l) ev (shue-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 modication in timed trace ex- pressions lies in the notions of events and event types, and in the denition 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 dened 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 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 = 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 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 = 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 specication given by τ . The following simple trace exemplies 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 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 [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 denition, model checking and runtime verication 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 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 [15] and it was extended to LTL3 by Bauer, Leucker, Schallhart [7] for runtime verication. In real-time systems it is likely that time bounded properties must be spec- ied: 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 verication (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 benets 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 verication 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 verication. InTheory and Practice of Formal Methods, volume 9660 of LNCS, pages 4764, 2016. 5. D. Ancona, A. Ferrando, and V. Mascardi. Parametric runtime verication 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 verication 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: Specication, execution and verication 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 verication. 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 specications. 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 specication and verication 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 verication 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.