Thomas Brihaye Umons

Arthur Milchior
email: arthur.milchior@ulb.ac.be

Gilles Geeraerts
email: gilles.geeraerts@ulb.ac.be

Hsi-Ming Ho

Benjamin Monmege
email: benjamin.monmege@univ-amu.fr

Efficient algorithms and tools for MITL model-checking and synthesis

Keywords: MITL, Model-checking, Synthesis, Timed automata

Metric Interval Temporal Logic (MITL) is an extension of the classical Linear Time Logic (LTL) that can be used to characterise real-time properties of computer systems. While the practical interest of MITL is undeniable, there is still today a remarkable lack of tool support for this logic. In this short paper, we report on our on-going work effort to complete the theoretical knowledge about MITL. We also report on our recently introduced tool MightyL, which translates MITL formulae into timed automata, enabling efficient modelchecking of this logic. Finally, we sketch the future directions of our current line of research, which will be to extend MightyL to support reactive synthesis of MITL properties.

I. INTRODUCTION

The development of reactive and critical real-time systems is known to be a difficult problem, since the safety of those systems does not only rely on their correct interaction with their environment, but also on the precise timings of these interactions. Two major approaches have been advocated by the formal methods community to ensure strong guarantees about the behaviour of such systems, namely: model-checking and synthesis. Roughly speaking, model-checking allows one to check whether some model of the system satisfies a given property. Synthesis extends the scope of computer-assisted design of hardware/software systems beyond the capabilities of model-checking: given a model of the environment, synthesis amounts to computing (if possible) a controller that enforces a given property.

In the untimed settings, theoretical and practical contributions on these two problems abound, and many tools are available to perform model-checking and synthesis when the system and the environment are specified as (Büchi) automata, and the properties are given in Linear Temporal Logic (LTL for short) [START_REF] Pnueli | The temporal logic of programs[END_REF]. See for example [START_REF] Bohy | Acacia+, a tool for LTL synthesis[END_REF], [START_REF] Cimatti | NuSMV2: An opensource tool for symbolic model checking[END_REF] for tools that allow to perform LTL model-checking and synthesis respectively.

In the real-time setting, timed automata [START_REF] Alur | A theory of timed automata[END_REF] are now established as the prime automaton model, and several tools such as Uppaal [START_REF] Kim | Uppaal in a nutshell[END_REF], Uppaal TiGa or LTSMin (with the Opaal plug-in) [START_REF] Kant | LTSmin: High-performance language-independent model checking[END_REF] support them. Those tools, however, accept timed automata as the model of the system, but the properties that they can verify or synthesise are essentially untimed, which limits their range of applications. For example, Uppaal supports mainly CTL properties with some restricted TCTL queries.

The most natural real-time extension of LTL is arguably the metric temporal logic (MTL) [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF]. In MTL, one can write properties such as (a → ♦ [x,y] b), where [x, y] is an interval, and meaning 'every a should eventually be followed by a b after at least x and at most y time units'. Unfortunately, MTL is mostly undecidable [START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF], a limitation which has prompted Alur et al. to introduce the metric interval temporal logic (MITL) as a fragment of MTL where punctual (i.e singular) intervals are disallowed [START_REF] Alur | The benefits of relaxing punctuality[END_REF]. They have showed that MITL satisfiability is decidable (in EXPSPACE) and that MITL formulae can be translated into timed automata thereby enabling automata-based modelchecking. MITL thus seems to be an excellent real-time counterpart to LTL. Unfortunately, and albeit the works of Alur et al. have appeared 20 years ago, tool support for MITL is still lacking.

In this short paper, we present our ongoing research effort, that aims at providing the formal methods community with (hopefully efficient) tools to perform MITL model-checking and synthesis. During the past decade, we have been working to extend the theory about MITL (we have, for instance, characterised the decidability of synthesis, and proposed new translation techniques to timed automata), and to develop tools based on these new results. The cornerstone of our contribution is our recently introduced tool MightyL, which performs efficient translation of MITL into timed automata [START_REF] Brihaye | MightyL: A compositional translation from MITL to timed automata[END_REF], [START_REF] Brihaye | Timed-automata-based verification of MITL over signals[END_REF], thereby enabling efficient automata-based modelchecking of MITL (thanks to efficient model-checking engines such as Uppaal [START_REF] Kim | Uppaal in a nutshell[END_REF] or LTSMin [START_REF] Kant | LTSmin: High-performance language-independent model checking[END_REF] with Opaal plugin as back-ends). We plan to continue this line of research by extending MightyL to perform efficient synthesis of MITL, based on the techniques presented in [START_REF] Filiot | An antichain algorithm for LTL realizability[END_REF] for LTL.

II. THE METRIC INTERVAL TEMPORAL LOGIC

We start by defining the syntax of MITL. Let Σ be a finite alphabet that models the possible actions of the system. Then, MITL formulae over Σ are generated by the grammar:

ϕ := | ⊥ | σ | ϕ ∧ ϕ | ϕ ∨ ϕ | ¬ϕ | ϕU I ϕ
, where σ ∈ Σ and I is a non-singular interval with endpoints in N ≥0 ∪{∞}. As in the case of LTL, the U I operator is read 'until'. So intuitively (see below for a formal definition), pU I q means 'p should hold until q holds, and this happens after t time units, with t ∈ I'. As is usual, also in the case of LTL, we rely on useful shorthands such as the 'eventually' operator ♦ I ϕ ≡ U I ϕ and the 'globally' operator I ϕ ≡ ¬♦ I ¬ϕ. For example, (req → (♦ (0,3) grant)) is an MITL formula, while pU [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | A theory of timed automata[END_REF] q is not, because the [1, 1] interval is singular.

Let us now discuss the semantics of MITL. Two semantics have been considered in the literature, namely: the continuous and the pointwise semantics. In the continuous semantics [START_REF] Alur | The benefits of relaxing punctuality[END_REF], MITL formulae are interpreted over signals, i.e. functions that associated valuations of propositional variables to all timestamps (which are modeled by the nonnegative real). In this short paper, we consider the so-called pointwise semantics only, because it is the most natural when relying on timed automata for the models of the system. That is, formulae of MITL will be interpreted over timed words which are infinite sequences of pairs of the form (action, timestamp), where the action is an element from Σ, and the sequence of timestamps along the timed word is nondecreasing, in order to model faithfully the elapsing of time. Formally, a timed word over some alphabet Σ is an infinite sequence ρ = (σ 0 , τ 0 )(σ 1 , τ 1 ) • • • over Σ × R + with (τ i ) i∈N a non-decreasing sequence of non-negative real numbers. We let T Σ ω be the set of timed words over Σ. A timed language is a subset of T Σ ω .

We can now define the (pointwise) semantics of MITL as a timed language. We say that a timed word ρ = (σ 0 , τ 0 )(σ 1 , τ 1 ) • • • over Σ satisfies ϕ at position i (written ρ, i |= ϕ) if ρ, i and ϕ respect one of the inductive rules:

• ρ, i |= and ρ, i |= ⊥; • ρ, i |= σ if σ = σ i and ρ, i |= ¬φ if ρ, i |= φ; • ρ, i |= φ 1 ∧ φ 2 if ρ, i |= φ 1 and ρ, i |= φ 2 ; • ρ, i |= φ 1 ∨ φ 2 if ρ, i |= φ 1 or ρ, i |= φ 2 ; • ρ, i |= φ 1 U I φ 2 if there exists j > i, ρ, j |= φ 2 , τ j -τ i ∈ I,
and, for all i < k < j, ρ, k |= φ 1 . We write ρ |= ϕ when ρ, 0 |= ϕ. We denote by L (ϕ) the set of all timed words ρ s.t. ρ |= ϕ, and call L (ϕ) the language of ϕ. For example, (req → (♦ (0,3) grant)) is satisfied by ρ = (req, 1)(req, 1.5)(grant, 3.6)(∅, 5)(∅, 6)(∅, 7) • • • because the (unique) grant event occurs in the words 2.6 and 2.1 time units after the respective req events.

Observe that MITL can also be interpreted on finite timed words (or signals [START_REF] Brihaye | Timed-automata-based verification of MITL over signals[END_REF]) but we omit these alternative definitions in this short paper.

q 0 q 1 a b c, x ≥ 2, {x} s 0 s 1 s 2 a,{y} b,{y} c, y = 2 c, y = 4

III. MODEL-CHECKING MITL AND THE MIGHTYL TOOL

The first main problem we are interested in about MITL is the well-known model-checking problem: model-checking allows one to prove in a mathematical sense that a model of a computer system is correct wrt a given specification, or to expose bugs. The family of models that we rely on in this work are known as timed automata (TA for short) [START_REF] Alur | A theory of timed automata[END_REF]. Roughly speaking, timed automata extend classical (nondeterministic, Büchi) automata by a finite set X of realvalued variables called clocks. The values of those clocks increase spontaneously with time elapsing, all at the same rate. Then, discrete transitions in a TA can constrain the value of the clocks (by a condition called a guard) and reset some clocks.

Formally, let X be a finite set of real-valued clocks. The set G(X) of clock constraints g over X is defined by g

:= | g ∧ g | x c
, where ∈ {≤, <, ≥, >}, x ∈ X and c ∈ N. A valuation over X is a mapping v : X → R + . We denote by 0 the valuation that maps every clock to 0. The satisfaction of a constraint g by a valuation v is defined in the usual way and noted v |= g. For t ∈ R + , we let v + t be the valuation defined by (v +t)(x) = v(x)+t for all x ∈ X. For R ⊆ X, we let v[R ← 0] be the valuation defined by

(v[R ← 0])(x) = 0 if x ∈ R, and (v[R ← 0])(x) = v(x) otherwise.
Then, a timed automaton (with Büchi acceptance condition) on the alphabet Σ is a tuple A = (L, 0 , T, F ) where: (i) L is a finite set of locations;

(ii) 0 ∈ L is the initial location; (iii) T ⊆ L × Σ × G(X) × 2 X × L
is the transition relation, where each transition consists of the source location, the letter to be read, the clock constraint (guard) to be checked, the clocks to be reset, and the target location; (iv) F ⊆ L is a set of accepting locations.

For example, Figure 1 displays two TAs (ignore the dashed arrows for the moment). The right one has three states, where s 0 is both initial and accepting (s 0 ∈ F ). The transition from s 0 to s 1 has label a, and resets clock y, while the transition from s 1 to s 2 has label c, and can be taken only when y = 2.

As expected, timed automata define timed languages. Formally, a configuration of a TA A = (L, 0 , T, F ) is a pair ( , v) where ∈ L is the current location of the automaton, and v is a valuation of the clocks in X. Given a configuration ( , v), two sorts of transitions can occur.

First, a continuous transition corresponds to the elapsing of δ time units and affects the valuation of the clocks only. Formally, for all configurations ( , v), for all δ ∈ R + , we let ( , v) δ -→ ( , v +δ). Second, a discrete transition corresponds to a change of location of the automaton, and affects both the current location and the clock valuation (through the resets). Formally, for a configuration ( , v) and a letter σ ∈ Σ, we have a discrete transition ( , v)

σ -→ ( , v ) iff there exists a transition t = ( , σ, g, R, ) ∈ T s.t. v |= g and v = v[R ← 0]. We write ( , v) δ,σ --→ ( , v ) whenever there is v s.t. ( , v) δ -→ ( , v ) σ -→ ( , v ). Then, a run (of A) on a timed word ρ = (σ 0 , τ 0 )(σ 1 , τ 1 ) • • • over Σ is an infinite sequence of tran- sitions of the form π = ( 0 , 0) δ0,σ0 ---→ ( 1 , v 1 ) δ1,σ1 ---→ ( 2 , v 2 ) • • • s.t. τ i = i j=0
δ j for all i ≥ 0. We consider Büchi acceptance conditions: a word ρ is accepted by a TA A iff A admits a run π on ρ s.t. at least one accepting location ∈ F occurs infinitely often along π. We denote by L(A) the timed language made up of all words accepted by A. As an example, the timed language of the TA on the left of Figure 1 accepts all timed words of the form

(α 0 , τ 0 )(c, τ 0 )(α 1 , τ 1 )(c, τ 1 ) • • • where each α i is either a or b, and τ i -τ i-1 ≥ 2 for all i ≥ 0 (assuming τ -1 = 0).
Finally, we recall that, given two TAs A 1 and A 2 , one can build a TA A 1 × A 2 , called the synchronous product of

A 1 and A 2 , which is s.t. L(A 1 × A 2 ) = L(A 1 ) ∩ L(A 2 ) [1].
Now that we have fixed the model of timed automata, we can define the first main problem we are interested in, namely the model-checking problem. Given a TA M (modelling some computer system) and an MITL formula ϕ (modelling some requirement on the actions of the system) on the same alphabet Σ, the model-checking problem asks whether all executions of M satisfy ϕ, i.e. whether L(A) ⊆ L(ϕ).

A widely used technique (also in the untimed case) is automata-based model-checking, which consists in expressing all inputs of the problem in terms of automata, and relying on automata-based algorithms to check for the language inclusion. In our case, this amounts to: first, computing ¬ϕ (which thus represents all the undesired behaviours of the system); then, to translate ¬ϕ into a timed automaton A ¬ϕ s.t. L(A ¬ϕ ) = L(¬ϕ); and finally to check whether M and A ¬ϕ accept a common word, i.e. whether L(A ¬ϕ ) ∩ L(M ) = L(A ¬ϕ × M ) = ∅ (observe that the model-checking problem is thus reduced to a language emptiness problem for TAs). The answer to the modelchecking problem is positive iff L(A ¬ϕ )∩L(M ) = ∅, i.e. no execution of M violates ϕ.

As can be seen from this brief summary, a key ingredient to automata-based model-checking is the ability to translate MITL formulae to equivalent TAs. Such a technique can already be found (for the continuous semantics) in the seminal paper of Alur et al. [START_REF] Alur | The benefits of relaxing punctuality[END_REF], and several other proposals have been made since then [START_REF] Brihaye | On MITL and alternating timed automata of infinite words[END_REF], [START_REF] Maler | From MITL to timed automata[END_REF], including from some of the authors of the present paper. We will now discuss our recently introduced tool MightyL [START_REF] Brihaye | MightyL: A compositional translation from MITL to timed automata[END_REF], which translates efficiently MITL formulae into equivalent timed automata1 . To the best of our knowledge, MightyL is the first such tool that is freely available, although several translation algorithms have been proposed in the literature during the past 20 years. The main features of MightyL can be summarised as follows:

1) As explained, MightyL performs the translation of the MITL specification into a corresponding TA representation. An automaton equivalent to the MITL formula is output in the Uppaal XML format [START_REF] Kim | Uppaal in a nutshell[END_REF]. This allows one to use a broad range of model-checkers as the back-end to perform the actual verification, such as Uppaal (in the finite words semantics) or LTSMin [START_REF] Kant | LTSmin: High-performance language-independent model checking[END_REF].

2) The translation algorithm implemented in MightyL is compositional. Instead of building a single monolithic timed automaton corresponding to the formula, MightyL builds a network of so-called component timed automata, one for each sub-formula2 . Hence, the network of TAs retains the structure of the original MITL formula. The actual composition of these component TAs is computed by the model-checker. This can thus be performed on-the-fly, and benefit from any optimisation that the model-checker implements. In future works, we plan to study heuristics that could be incorporated in the model-checking engine and exploit the structure of the TAs that are produced by MightyL.

3) The synchronisation between the component TAs is designed in a way to mitigate the state explosion that could occur during the composition. To achieve this, we have drawn inspiration from results on very weak one-clock alternating timed automata [START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF]. 4) The total number of clocks needed by the resulting component TAs is reduced by half at most, compared to previous works [START_REF] Brihaye | On MITL and alternating timed automata of infinite words[END_REF]. This optimisation is important, as it is well-known that model-checking tools such as Uppaal are very sensitive to the number of clocks. MightyL has been written in OCaml and is freely available for download on the web at http://www.ulb.ac.be/ di/verif/mightyl. The website also allows one to test MightyL online: one can submit MITL formulae, obtain the corresponding network of TAs in the Uppaal XML format, and even run Uppaal or LTSMin online to check for satisfiability of the formulae. We are currently working on refactoring the code of MightyL to make it more readable, and easier to extend. < 1 s. 1.12 s.

(( ♦p 1 ) → (q → ♦ [0,5] r)) < 1 s. 1 s. ( ♦p 1 ∧ ♦p 2 ) → (q → ♦ [0,5] r) < 1 s. 1.2 s.
Our experiments show very promising results in practice, see [START_REF] Brihaye | MightyL: A compositional translation from MITL to timed automata[END_REF] for more details. As a benchmark, we check satisfiability of MITL formulae. i.e. whether L(ϕ) = L(A ϕ ) = ∅ for a given MITL formula ϕ. Satisfiability is thus a good benchmark for MightyL, since it can be solved by translating the MITL formula into an equivalent TA, and then checking for language emptiness, as in the case of model-checking, our target application. We report on some results in Table I.

In general, the model-checking times are more tractable with formulae from the MITL [0,∞] fragment, that consists of formulae where all intervals either start with 0 or end with +∞.

IV. TOWARDS EFFICIENT SYNTHESIS

As already argued in the introduction, model-checking is a very powerful tool, but it offers very few help to the designer when a bug is found. While model-checking tools can produce error traces (i.e. executions of the model that violate the specification), they do not offer clue as how to modify the system (and its model) in order to avoid them.

A much more powerful approach has been advocated by the formal methods community in the past 20 years: synthesis. In our setting, the reactive synthesis problem asks, given a (deterministic) TA P called the plant, and an MITL formula ϕ (the specification), to find, if possible, a TA3 C, called the controller, such that, when C controls the plant P , the whole system respects ϕ, i.e. L(C × P ) ⊆ L(ϕ).

Of course, not any deterministic TA is admissible as a controller. A proper theoretical framework for the reactive synthesis problem in the real-time setting has been introduced by D'Souza et al. in [START_REF] Deepak | Timed control synthesis for external specifications[END_REF]; let us highlight their main ideas. First, the alphabet Σ of the plant P is partitioned into controllable and uncontrollable actions, i.e. those on which the controller can and cannot act, respectively. Then, the conditions on the controller are that: (i) it cannot reset the clocks of the plant, but it can observe them, and can have its own set of clocks that it can test and reset at will; (ii) it cannot restrict the uncontrollable moves of the plant: whenever such a move is possible in the plant, it should also be possible under the controller (i.e. in P × C); and (iii) it must be non-blocking, i.e. it cannot introduce deadlocks.

For example, consider again the automata in Figure 1. The left one is an example of plant P , where the uncontrollable

Figure 1 .

 1 Figure 1. Two example timed automata: a plant and a its controller.

Formula MightyL LTSMin p 1 U

 1 [0,5] (p 2 U [0,5] (p 3 U [0,5] (p 4 U [0,5] (p 5 U [0,5] p 6 ))))

Table I RUNNING

 I TIMES OF MIGHTYL ON THE SATISFIABILITY PROBLEM.

Note that MightyL can also be used to perform MITL model-checking in the continuous semantics[START_REF] Brihaye | Timed-automata-based verification of MITL over signals[END_REF], by reducing it to a language inclusion problem in the pointwise semantics, thereby allowing to rely on the same model-checking back-end as in the pointwise case.

Note that this construction subsumes the construction implemented in LTL2BA for LTL[START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF].

with some additional restrictions, see below. actions are a and b (dashed arrow), and only c is controllable. Let us fix the MITL requirement (a → ♦ [2,3] c) ∧ (b →

♦ [START_REF] Brihaye | On MITL and alternating timed automata of infinite words[END_REF][START_REF] Brihaye | Realtime synthesis is hard! In Formal Modeling and Analysis of Timed Systems -14th International Conference[END_REF] c). That is, the goal of the controller is to ensure the proper timing of the (controllable) c actions that follow each of the (uncontrollable) a's and b's: when an a has occurred, the c must take place after at least 2 and at most 3 time units (and similarly for the b: between 4 and 5 time units). Then, the TA on the right is a possible controller for this requirement. Note that it does not restrict the uncontrollable actions of the plant (which can still perform a's and b's at will), but controls the moment at which the (controllable) c occurs. To do so, it needs an extra clock y that is reset whenever an a or b occurs. This clock is necessary because the x clock in P does not measure the time since the last a or b, but since the last c.

Unfortunately, MITL synthesis has been shown undecidable in [START_REF] Doyen | Realizability of real-time logics[END_REF], a result recently refined in [START_REF] Brihaye | Realtime synthesis is hard! In Formal Modeling and Analysis of Timed Systems -14th International Conference[END_REF]. More precisely, MITL synthesis is undecidable in the general case both on finite and infinite words, and even for very restricted fragments of the logic. Decidability can be recovered, however, when we bound a priori the resources that the controller can use. In our setting the resources mean: (i) the number of clocks that the controller can use; and (ii) the maximal constant that can appear in the guards of the controller. The reader familiar with timed automata will understand that these restrictions allow to bound a priori the number of regions that any potential controller can have. We call this new problem the bounded resources reactive synthesis problem (BRRS for short). A 3EXPTIME solution to BRRS is readily obtained by combining the algorithm of D'Souza and Madhusudan [START_REF] Deepak | Timed control synthesis for external specifications[END_REF] with any procedure to translate MITL formulae into timed automata (such as the one implemented in MightyL). Unfortunately, this complexity (together with the fact that one needs to build the full region automaton of the potential controller) makes this algorithm a very poor candidate for practical implementation. The next step in our research will thus be to look for a more feasible solution. Our aim is to adapt the efficient techniques of Jin et al. [START_REF] Filiot | An antichain algorithm for LTL realizability[END_REF] (for LTL synthesis), as we are about to explain now.

As in the case of LTL, our plan is to obtain an iterative algorithm that, given an instance (P, ϕ) of BRRS (assuming fixed resources), creates a finite sequence G 1 , G 2 , . . . , G n of games played between some protagonist (that can take all the possible actions that a potential controller could chose) against the plant. Those games have the following properties: (i) if there is a winning strategy for the protagonist in some game G i , then, this winning strategy can be readily translated into a correct controller for the specification ϕ; (ii) if no such controller exists, then, the protagonist has no winning strategy in any game of the sequence. Moreover, the size of those games increases along the sequence, with the first ones G 1 , G 2 . . . being of relatively small sizes, hence very easy to analyse using standard tools. In some sense, each G i can be seen as an approximation of the full instance, each step in the sequence being a refinement of the approximation. In the LTL case, experimental evidence shows that, on most instances, a controller can be computed from the coarsest approximations G 1 or G 2 , which yields a very efficient algorithm in practice.

Concretely, those games G i could be: (i) either untimed (Büchi) games that can be solved using classical algorithms. This is the most straightforward approach, however, to obtain such untimed games we will need to rely on the region construction, which will probably yield an undesired state explosion; (ii) or timed games, such as the one that can be solved by Uppaal TiGa (in the finite words setting). Relying on such tools will allow us, as in the case of model-checking, to benefit from their efficient implementation (in the case of Uppaal TiGa, this means relying on its on-the-fly zone-based algorithm for solving timed games). We will investigate the relative merits of these different techniques, and plan to implement them as an extension of our tool MightyL.