Ramzi Ben Salah
email: ramzi.salah@imag.fr

Marius Bozga
email: marius.bozga@imag.fr

Oded Maler
email: oded.maler@imag.fr

Compositional Timing Analysis

Keywords: D.2.4 [Software Engineering]: Software/Program Verification, B.7.2 [Integrated Circuits]: Design Aids, F.1.1 [Computation by abstract devices]: Models of Computation Theory, Verification timed automata, abstraction, reachability analysis, compositional generation

We develop and implement a methodology for automatic abstraction of systems defined as networks of timed components modeled by timed automata. The abstraction technique yields an abstract model with much less clocks and states which over-approximate the timed behavior of the concrete system. Using this technique we can analyze timed system of size beyond the capabilities of contemporary analysis tools for timed automata.

INTRODUCTION

The only way to master the complexity of large systems is to apply a hierarchical/compositional design methodology. The basic principle of such a methodology is that a subsystem treated at one level of abstraction as a model M of some detail, is encapsulated as a component M ′ when a higher level is considered. The major difference between M and M ′ is that the latter abstracts away from the internal details appearing in M and focuses on the observable input-output (interface) behavior of the component which determine its high-level functionality. To take an illustrative example, consider the process of submitting a paper to a conference. Viewed from the perspective of the authors, the model M is a complex network or processes involving ideas, model formulation, proving theorems, implementation, experiments, literature survey and typesetting, admitting complex inter dependencies. On the other hand, from the perspective of the program chair all this internal details are irrelevant and the abstract model M ′ only specifies whether a substantial contribution has been submitted by the deadline, regardless of the respective timing of the sub processes.

For M ′ to be useful in the analysis at the higher level it should be significantly less complex than M and since there is no free lunch, the price of the abstraction is that M ′ is less precise than M in terms of the observable behaviors it admits. We work in the context of set-theoretic nondeterminism where the abstract model, by ignoring certain variables, allows more observable behaviors than a detailed model would. To be more concrete, think of M as an automaton whose state space consists of vectors of valuations to variables. Projecting away some variables will make the automaton more nondeterministic and will enlarge the set of observable sequences it can generate. In the verification context, this overapproximation of the semantics guarantees that correctness proofs obtained using the abstract model are valid for the concrete model. For the purpose of performance evaluation, which is one of the central issues in embedded systems, performance guarantees obtained using M ′ will hold for the detailed model M as well.

In this work we develop a novel methodology, supported by a tool chain, where M is a network of timed components, representing processes that respond to input events by emitting the corresponding output events within some time delay which is known to be bounded within a given interval. Such timed components may represent the execution times of software modules in a streaming application, communication delays in a network, the response times of servers or propagation delays in digital gates. Each component is modeled as a timed automaton with variables (a variant of the timed automaton of [START_REF] Alur | A Theory of Timed Automata[END_REF] adapted for the compositional context) and the whole network is equivalent to a global timed automaton with at least one state variable and one clock 1 per component. Although major analysis problems for timed automata are decidable, and despite of a lot investment and engineering innovation in timed automata tools over the last decade, the analysis of such networks remains infeasible beyond a modest amount of components. The essence of our work is the automatic generation of a smaller timed automaton M ′ with less states and less clocks which preserves the observed qualitative semantics of M and over-approximates its timed semantics. The reduced model M ′ can then replace M as a component in a higher level.

The core idea behind our technique is to use the clocks associated with the internal processes in M in order to analyze the possible time-dependent behaviors of the system. To do that we need to restrict the number of components in M to the capabilities of existing verification tools (5-20 components) and treat larger systems in a divide-and-conquer fashion by decomposing them into smaller chunks, applying the abstraction technique and composing the resulting abstract models. Before diving into the formal details of the chain of transformations leading from M to M ′ let us illustrate informally the nature of the abstraction via an example (see also [START_REF] Ben Salah | On Timed Components and their Abstraction SAVCBS[END_REF]).

(a) (e) (d) (b) (c) [l 1 , u 1 ] B 1 0 t 1 + l 2 l 1 u 1 t 1 t 1 + u 2 0 u 1 l 1 l 1 + l 2 u 1 + u 2 x B 2 [l 2 , u 2 ] z 1 z 2 s 0 s 0 s 1 s 1 s 2 s 2 s 3 s 3 x ↑ ĉ := 0 c 1 := 0 c 1 ∈ [l 1 , u 1 ] z 1 ↑ c 2 := 0 z 2 ↑ c 2 ∈ [l 2 , u 2 ] x ↑ ĉ := 0 ĉ ∈ [l 1 , u 1 ] z 1 ↑ ĉ ∈ [l 1 + l 2 , u1 + u 2 ] z 2 ↑
The network in Figure 1 has two components, B1 which responds to input x by emitting output z1 within a delay in the interval [l1, u1] and B2 which reacts to z1 within t ∈ [l2, u2] time. We assume that x occurs at time zero and that both z1 and z2 are considered observable. The range of possible behaviors is illustrated in Figure 1-(d) where z2 is constrained to occur between l2 and u2 time after z1. As a first step we augment the timed automaton representing the composition B1||B2 with an additional clock ĉ which measures the time elapsed since event x, see Figure 1-(b). This clock does not participate in the transition guards and hence does not influence the behavior of the automaton, it only adds time stamps to the runs. We then compute the interpreted timed automaton based on forward reachability 2 and obtain an equivalent automaton where transition guards are expressed as constraints over clocks {c1, c2, ĉ} in the form of zones. We then get rid of the internal clocks, after they have served us to restrict the behaviors of the automaton, and project the zones on ĉ to obtain the abstract automaton of Figure 1-(c). In this automaton z1 is constrained to occur in the absolute time interval [l1, u1] (which is exact) while z2 is allowed to take place in the interval [l1 + l2, u1 + u2] regardless of the occurrence time of z1 (which is an over-approximation, see Figure 1-(e)).

This example is too small to illustrate the role of timed reachability computation in restricting the range of behaviors of the automaton, it only give an intuition concerning the effect of clock 2 These notions will be explained in the sequel. projection. Another simplifying aspect was the fact that we handled only one input event. In this work we address the challenging problem of adapting this idea to infinite streams of input events that may occur at arbitrary time points. We let each input event generate its own clock, reset to zero upon arrival, and after the reachability analysis we get rid of the internal clocks and project the timing constraints on the input clocks. Doing so, we generate a reduced abstract model in which the timing of each output event is conditioned on the time elapsed since the input event that has triggered it. We restrict ourselves to acyclic networks of timed components in which every component admits a finite upper-bound on its reaction time. In such networks, each input event triggers a wave of activity along the network, a wave which progresses from inputs to outputs and leaves the network within a bounded amount of time. This fact, together with bounded frequency assumptions on the inputs, guarantees that the number of co-existing waves is always bounded and, consequently, so is the number of input clocks. Whenever the processing of an event terminates, its clock can be reused by subsequent events. Indeed, the adaptation of the IF toolbox [START_REF] Bozga | IF-2.0: A Validation Environment for Component-Based Real-Time Systems[END_REF] to handle those dynamic clocks with varying denotations was the major implementation challenge in this work which goes all the way from conception to realization.

The problem we address is central to the development of embedded systems and no wonder it has attracted many research groups representing different communities and approaches [START_REF] Perathoner | Influence of Different System Abstractions on the Performance Analysis of Distributed Real-Time Systems[END_REF][START_REF] Kunzli | Combining Simulation and Formal Methods for System-Level Performance Analysis DATE[END_REF], some of which we mention very briefly below. The work around the real-time calculus and similar formalisms [START_REF] Thiele | Performance Analysis of Embedded Systems, Embedded System Handbook[END_REF][START_REF] Wandeler | System Architecture Evaluation Using Modular Performance Analysis -A Case Study[END_REF][START_REF] Henia | System level performance analysis-the SymTA/S approach[END_REF] attempts to adapt analytic tools taken from domains such as queueing theory or max-plus algebra and adapt them to the more irregular setting of embedded systems admitting phenomena such as jitter, burst and discrete decisions of schedulers which are not easily modeled in the classical frameworks. The work and the tools developed in this framework share with ours the overall goal, namely give an abstract and approximate characterization of the timed "transfer function" of components as a transducer of timed streams, however the proposed techniques are radically different. Our approach does not start with clean algebraic framework which scale-up well but is very approximate to start with, but rather starts from the opposite: a state based model represented as a timed automaton which is much stronger in expressive power but is notorious for not scaling up beyond toy problems. 3 It is this clock-explosion challenge that we try to meet in this work. Compositional reasoning has been applied to timed automata in [START_REF] Tasiran | Verifying Abstractions of Timed Systems[END_REF] and is advocated for timing and performance issues in the context of interface automata [START_REF] De Alfaro | Timed Interfaces, EMSOFT'02[END_REF][START_REF] Henzinger | An Interface Algebra for Real-Time Components[END_REF] which offers a formal framework for checking whether the performance that a component provides matches the performance expected by other components. The major differences with respect to our work is that we attempt to generate the description of the abstract performance characterization of the component automatically from the more detailed model.

The rest of the paper is organized as follows. In Section 2 we present all the prerequisite material on timed automata. In Section 3 we add state variables and additional structure to the automata to facilitate compositional discourse. Section 4 is the core of the paper where we introduce all the steps in our abstraction techniques, namely, the introduction of dynamic events clocks, the reachability computation, the projection of internal clocks and variables and the minimization. In Section 5 we demonstrates the application of the tool chain to a case study consisting of a network of 36 components, modeling a sequential circuit used to illustrate the concept of wave pipelining. We apply our technique to find bounds on the input frequency which guarantee that no elementary component receives an input event before having digested the previous event.

TIMED AUTOMATA

In this section we define the variant of timed automata that we use. Notable deviations from the classics, made to fit our modeling and analysis needs, are that we make clock inactivity explicit 4and that we allow clock copying, not only resets to zero, during transitions. We start with preliminary definitions of clocks, zones, etc., then define timed automata and their semantics and conclude with forward reachability computation over zones, the method of choice in contemporary tools [START_REF] Henzinger | Symbolic Model-checking for Real-time Systems[END_REF][START_REF] Daws | The tool KRONOS[END_REF][START_REF] Larsen | UPPAAL in a Nutshell[END_REF][START_REF] Bozga | IF-2.0: A Validation Environment for Component-Based Real-Time Systems[END_REF], and its byproduct, the interpreted timed automaton which plays an important role in our analysis technique.

Preliminary Definitions

Let R ⊥ denote R+ ∪ {⊥} were ⊥ is a special symbol meaning inactive. We extend addition to R ⊥ by letting ⊥ + d = ⊥. Let C = {c1, ..., cn} be a finite set of variables called clocks ranging over R ⊥ . A clock valuation is a function v : C → R ⊥ and the set of possible valuations of C is R n ⊥ . A clock c is said to be active in valuation v iff v(c) = ⊥. Due to the distinction between active and inactive clocks, we have to deal with clock valuations of varying dimensionality. Given some

C ′ ⊆ C, we use V C ′ to denote the set of valuations in which v(c) = ⊥ iff c ∈ C ′ . Elements of V C ′ are then non-negative real vectors (points) of dimension |C ′ | ≤ n. The projection operation v ′ = v/ C ′ maps elements of VC to elements of V C ′ by letting v ′ (c) = v(c) if c ∈ C ′ and v ′ (c) = ⊥ otherwise.
In timed automata clock valuations change due to two types of activities: time progress which happens inside a discrete state and clock assignments which take place during discrete transitions. For d ≥ 0, we say that clock valuation v ′ is the result of applying dtime-progress to v, denoted by v ′ = v + d, if for every clock c, v ′ (c) = v(c) + d. Note that inactive clocks do not change their value. A clock assignment is a function γ : R n ⊥ → R n ⊥ indicating a transformation of clock values upon a transition. Assignments are restricted to compositions of one or more of the following basic assignments: ci := 0 (resetting to zero), ci := ⊥ (clock deactivation) and ci := cj (clock copying). We use v ′ = γ(v) to denote the fact that v ′ is the result of applying γ to v and use γ1 • γ2 for composition of assignments. The set of all assignments thus obtained is denoted by ΓC . We use the shorthand r C ′ to denote resetting all the clocks in some C ′ ⊆ C and kill C ′ for their deactivation.

Clocks constraints are used to express the influence of clock values on the behavior of the automaton. We use a family of constraints denoted by ΨC, defined by the following grammar:

ψ ::= true | ci ≺ k | ci -cj ≺ k | ψ ∧ ψ
where ci, cj ∈ C, k ∈ N and ≺∈ {<, ≤, =, ≥, >}. Constraints of the form x ≺ k and xy ≺ k are called atomic. The restriction of some ψ ∈ ΨC to a set of clocks C ′ ⊆ C, denoted by ψ/ C ′ , is the constraint obtained by deleting all atomic constraints that mention a clock outside C ′ .

We use v |= ψ to denote the fact that valuation v satisfies a clock constraint ψ. We will always assume (and guarantee) that constraints evaluated in a state of the automaton mention only clocks active in that state. The set Z ψ of valuations satisfying ψ is a subset of R m + where m ≤ n is the number of clocks active in the state. For any ψ, Z ψ is a convex polyhedron defined as the intersection of half-spaces which are either orthogonal (ci ≺ k) or diagonal (cicj ≺ k) with integer k. The set of all such polyhedra that we call timed zones will be denoted by ZC and its cardinality is finite in any bounded subset of R n .

Zones are closed under intersection and under the operations defined below. The timed convex hull of two zones is

Z1 ⊔ Z2 = min{Z ∈ ZC | (Z1 ⊆ Z) ∧ (Z2 ⊆ Z)}
which can be used as an over-approximation of Z1 ∪ Z2. The forward projection

Z ր = {v ∈ VC | ∃d ≥ 0, v -d ∈ Z} consists
of all clock valuations that can result from applying arbitrary time progress to elements of Z. The projection of

Z on C ′ ⊆ C is Z/ C ′ = {v/ C ′ | v ∈ Z}, and γ(Z) = {γ(v) | v ∈ Z} is the ap- plication of clock assignment γ to all elements of Z. In particular r C ′ (Z) is the resetting of the clocks in C ′ and kill C ′ (Z) is the de- activation of clocks in C ′ . Note that kill C ′ (Z) = Z/ C\C ′ . The difference between r C ′ (Z) and kill C ′ (Z) is that applying kill C ′
may reduce the dimensionality of the space on which the zone is defined while applying r C ′ may reduce the dimensionality of the set but not of the space on which it is defined,and after some time progress the set will regain its reduced dimensions. These operation are computed efficiently on a DBM representation of the zones. More details can be found, for example, in [START_REF] Yovine | Kronos: A Verification Tool for Real-time Systems[END_REF].

Timed Automata and their Analysis DEFINITION 1 (TIMED AUTOMATON). A timed automaton is a tuple

A = (Q, q0, C, I, ∆) where Q is a finite set of discrete states, q0 ∈ Q is the initial state, C is a finite set of clocks, I : Q → ΨC
associates a staying condition (invariant) with every state q such that the automaton may stay at q as long as the clock constraint I(q) is satisfied, ∆ ⊆ Q × ΨC × ΓC × Q is the transition relation consisting of elements of the form δ = (q, g, γ, q ′ ) where q, q ′ ∈ Q are, respectively, the source and the target of the transition, g ∈ ΨC is the transition guard restricting the execution of the transition to clock valuations that satisfy it and γ ∈ ΓC is a clock assignment occurring upon a transition.

Note that in this definition we do not have a specific alphabet of transition labels. We view each transition as a distinct type of event and postpone transition labeling to the next section where we discuss state variables and composition. Timed automata define infinite transition systems whose states are configurations of the form (q, v) ∈ Q×VC . The initial configuration is (q0, ⊥) with all clocks inactive and the transitions are either discrete transitions of the automaton or time-passage transitions, formalized via the notion of a step.

DEFINITION 2 (STEPS). A step of A is one of the following:

• A discrete step: (q, v) δ -→ (q ′ , v ′ ), for some δ = (q, g, γ, q ′ ) ∈ ∆ such that v |= g and v ′ = γ(v), • A time step: (q, v) d -→ (q, v + d) for some d ∈ R+ such that v + d |= I(q).
Note that the concatenation of two time steps of durations d1 and d2 is a time step of duration d1 + d2. A compound step is a discrete step followed by a time step (possibly of zero duration):

(q, v) δ,d -→ (q ′ , v ′ + d) ≡ (q, v) δ -→ (q ′ , v ′ ) d -→ (q ′ , v ′ + d)
A run of the automaton A starting from a configuration (q, v) is a sequence of compound steps.We use the notation (q, v) ξ -→ (q ′ , v ′ ) for runs. The untiming of ξ, denoted by µ(ξ), is the sequence of transitions taken, regardless of the time durations. The semantics of A, denoted by [[A]], is the set of runs it may generate from the initial state and its qualitative semantics is µ(

[[A]]) = {µ(ξ)|ξ ∈ [[A]]}.

From Timed Automata to Reachability Graphs

The verification of this infinite-state system is done symbolically by computing the reachability graph, also known as the simulation graph, whose nodes are symbolic states of the form (q, Z) ∈ Q × ZC which are closed under the following operations:

• The time successor of (q, Z) is (q, Z ′ ) where Z ′ is the set of clock valuations reachable from Z by letting time progress without violating the staying condition I(q):

post t (q, Z) = (q, (Z ր ∩ I(q))) = {(q, v + d) | (v ∈ Z) ∧ (d ≥ 0) ∧ ((v + d) |= I(q))}
• The δ-transition successor of (q, Z) via a transition δ = (q, g, γ, q ′ ) ∈ ∆ is the set of configurations reachable by taking this transition.

post δ (q, Z) = {(q ′ , v ′ ) | ∃v ∈ Z, v |= g ∧ v ′ = γ(v)} = (q ′ , (γ(Z ∩ g)))
• The δ-successor of (q, Z) is the set of configurations reachable from (q, Z) by a δ-transition followed by a time step:

succ δ (q, Z) = post t (post δ (q, Z)) = (q ′ , (γ(Z∩g) ր ∩I(q ′ )) PROPOSITION 1 (SUCCESSORS). A configuration (q ′ , v ′ ) be- longs to (q ′ , Z ′ ) = succ δ (q, Z) if and only if it is the endpoint of a compound step (q, v) δ,d
-→ (q ′ , v ′ ) for some (q, v) ∈ (q, Z) and some d ≥ 0. 5The analysis of timed automata is done via a forward reachability algorithm which starts with (q0, {⊥}) and computes successors until a fixed point is reached, a fact guaranteed by the finiteness of ZC in any bounded subset of R n ⊥ . As a byproduct, the algorithm produces the reachability graph which can be viewed as the finite state automaton defined below. DEFINITION 3 (REACHABILITY GRAPH). The reachability graph associated with a timed automaton A = (Q, q0, C, I, ∆) is a finite automaton G = (∆, S, s0, h) such that S is the smallest set of symbolic states containing the initial state s0 = (q0, {⊥}) and closed under {succ δ } δ∈∆ . The transition relation h ⊆ S × ∆ × S consists of all triples of the form ((q, Z), δ, (q ′ , Z ′ )) such that (q ′ , Z ′ ) = succ δ (q, Z).

The fundamental property of the reachability graph is that it preserves the qualitative semantics in the sense that it may generate a sequence of transitions w ∈ ∆ * iff w ∈ µ([[A]]). This implies that any (untimed) linear-time property verified on G holds also for A. Note that this is not true for the automaton obtained by taking A and removing its clocks. The reachability process excludes behaviors that cannot be realized due to timing constraints and only after that it is safe to remove the clocks. Our technique is inspired by this insight, and provides different levels of relaxation of the timing constraints after reachability. To this end we define the interpreted timed automaton which enjoys the properties of the reachability graph, but preserves also the quantitative timing information and is semantically equivalent to the timed automaton A from which it was derived.

DEFINITION 4 (INTERPRETED TIMED AUTOMATON).

Let A = (Q, q0, C, I, ∆) be a timed automaton and let G = (∆, S, s0, h) be its reachability graph. The interpreted timed automaton for A is A r = (S, s0, C, I r , ∆ r ) such that I r (q, Z) = Z and for every transition ((q, Z), δ, (q ′ , Z ′ )) ∈ h, corresponding to a transition δ = (q, g, γ, q ′ ) ∈ ∆ we define a transition ((q, Z), g ∩ Z, γ, (q ′ , Z ′ )) ∈ ∆ r .

Clearly, the semantics of A and of A r are identical and even if we later relax the timing constraints in A r and introduce more behaviors, we do not introduce any new qualitative behavior.

TIMED AUTOMATA WITH STATE VARI-ABLES

The timed automaton model presented so far was based on a flat state space, without mentioning state variables nor a Cartesian product structure. For the compositional treatment of networks of automata we need a richer formalism that will facilitate the discussion of composition, hiding of internal actions and the like. To this end we associate with the automata state variables so that each transition is associated in a change in the valuation of a variable and the semantics consists of the evolution of these valuations over time.

Variables, Valuations and Assignments

Let X = {x1, . . . , xm} be a finite set of variables ranging over a domain D. An X-valuation is a function v : X → D assigning to each xi a value v(xi). The set of X-valuations, which are just elements of D m , is denoted by

VX . Every X ′ ⊆ X defines a projection function /X ′ : VX → V X ′ such that v ′ = v /X ′ if v ′ (x) = v(x)
for every x ∈ X ′ . When states are associated with X-valuations, transitions correspond to changes in one or more state variables, formalized as assignments.

DEFINITION 5 (ASSIGNMENTS). Let v and v ′ be two valuations. The function fv : VX → VX is the constant function defined for every u ∈ VX as fv(u

) = v. The function f v,v ′ : VX → VX is such that for every u, u ′ ∈ VX , u ′ = f v,v ′ (u) when u ′ (x) =  v ′ (x) if v(x) = v ′ (x) u(x) if v(x) = v ′ (x)
In other words, f v,v ′ acts as the identity on all the variables on which v and v ′ agree and assigns to the other variables their value in v ′ . Needless to say,

v ′ = f v,v ′ (v).
In the sequel we restrict ourselves to the Boolean domain and use the notation x ↓ for x := 0 and x ↑ for x := 1.

For example if v = (0, 1, 1, 0) and v ′ = (1, 1, 0, 0), then f v ′ = {x1 ↑ , x2 ↑ , x3 ↓ , x4 ↓ }, and f v,v ′ = {x1 ↑ , x3 ↓ }.
We denote the set of X-assignments by FX . The projection f /V ′ of an assignment f on a subset X ′ of the variables is defined naturally via restriction. When valuations and assignments are associated with states and transitions we need to check, when composing automata, the compatibility between valuations over two non-disjoint sets of variables.

DEFINITION 6 (COMPATIBILITY). Let X 1 and X 2 be two sets of variables and let X = X 1 ∪ X 2 and X = X 1 ∩ X 2 . Two valuations v 1 ∈ V X 1 and v 2 ∈ V X 2 are said to be compatible if they agree on shared variables, that is, v 1 /X = v 2 /X . From two such compatible valuation one can naturally construct a joint valuation v 1 v 2 : X → VX which agrees with v 1 and v 2 on all variables. Likewise, two assignments

f 1 ∈ F X 1 and f 2 ∈ F X 2 are compatible if f 1 /X = f 2 /X
and one can construct from them a joint assignment f 1 f 2 : VX → VX .

Signals

As timed behaviors of a system defined over X we consider signals, functions from the time domain R+ to VX . 6DEFINITION 7 (X -VALUED SIGNALS). A signal over a set X of variables ranging over a discrete domain is a partial function ξ : R+ → VX defined over some interval [0, t), t ∈ R+ ∪ {∞}, which can be partitioned into a countable sequence of left-closed right-open intervals J = J1, J2, J3, . . . each of the form

J k = [t k-1 , t k ), such that ξ(t) = ξ(t ′ ) = ξ(J) if t and t ′ belong to the same interval J.
We denote the set of finite and infinite X-signals by S * (X) and S ω (X), and let S(X) = S * (X) ∪ S ω (X). The concatenation operation ξ1 • ξ2 is defined naturally for any ξ1 ∈ S * (X), ξ2 ∈ S(X), as it is defined for sequences. Signals can be represented in a state-based fashion, as a concatenation of constant signals where

v r 1 1 • v r 2 2 • v r 3 3 • •
• representing a signal which has value v1 for duration r1, then value v2 for duration r2, etc. or in an event-based fashion as a concatenation of time durations and assignments:

fv 1 • r1 • fv 1 ,v 2 • r2 • fv 2 ,v 3 • r3 • • • ,
which is the representation we will use. For example, signal which in state-based representation looks like

ξ = 1 0 0 ! 2 • 0 1 0 ! 5 • 0 0 0 ! 3 • 1 0 1 ! 7 • • • ,
will be written in an event-based form as:

ξ = {x1 ↑ , x2 ↓ , x3 ↓ } • 2 • {x1 ↓ , x2 ↑ } • 5 • {x2 ↓ } • 3 • {x1 ↑ , x3 ↑ } • 7 • • •
The projection ξ ′ = ξ /X ′ of an X-signal ξ on some X ′ ⊆ X is defined naturally by deleting variables outside X ′ from the assignments. This operation is a natural part of the process of hiding internal actions and may results in eliminating certain discrete steps and merging time steps. The projection of ξ on {x1, x3}, is represented as

ξ ′ = {x1 ↑ , x3 ↓ } • 2 • {x1 ↓ } • 5 • {} • 3 • {x1 ↑ , x3 ↑ } • 7 • • • ,
and since the assignment which involved only a change in x2 became silent we can merge two time steps into one and obtain

ξ ′ = {x1 ↑ , x3 ↓ } • 2 • {x1 ↓ } • 8 • {x1 ↑ , x3 ↑ } • 7 • • • The untiming of a signal is the sequence µ(ξ) = fv 1 • fv 1 ,v 2 • fv 2 ,v 3 • • • , that
is, the qualitative behavior described previously.

Timed Automata with Variables

We associate every timed automaton with a set X of variables, partitioned into disjoint subsets of input and state variables X = Xin ⊎ Xst. The difference between them is that those in Xin are controlled by the external environment of the automaton which follows their evolution passively, reacting to changes in their values.

On the other hand, variables in Xst are owned exclusively by the automaton which controls their values. A subset Xou ⊆ Xst of the state variables, called output variables, are observable to the outside and may serve as inputs for other components. The interface variables of the automaton are its input and output variables Xio = Xin ⊎ Xou.

The connection between states and valuations is defined via the function λ : Q → VX associating with every state an X-valuation v = λ(q). The projections of λ on the interface variables is denoted by λio. Two points are worth mentioning: 1) we allow multiple states to be mapped to the same valuation to accommodate for future use in the interpreted timed automaton which may have several symbolic states corresponding to the same discrete state; 2) We consider the values of input variables to be part of the state, hence every change in the input will cause a transition to a different state, and there will be only one input valuation associated with each state. This amounts to composing every automaton with an unconstrained generator of its inputs. At a first glance this looks like an unnecessary blow up of the state space, but, when analyzed, the automaton should be composed anyhow with a generator of its inputs, so this overhead is an illusion.

DEFINITION 8 (TIMED AUTOMATA OVER VARIABLES).

A timed automaton over a set X of variables is a triple AX = (A, X, λ) where A = (Q, q0, C, I, ∆) is a timed automaton, X is a set of variables, and λ : Q → VX maps states to X-valuations. This function induces a mapping between transition labels and Xassignments where every transition δ = (q, g, γ, q ′ ) such that λ(q) = v and λ(q

′ ) = v ′ is labeled by λ(δ) = f v,v ′ .
We impose some additional properties that hold, for example, for the automata introduced in [START_REF] Maler | Timing Analysis of Asynchronous Circuits using Timed Automata[END_REF] for modeling Boolean circuits with delays, on which our example in Section 5 is based, and other automata obtained by well-structured composition of timed components.

1. Every transition in ∆ changes the value of exactly one variable. Consequently we can partition ∆ into sets of input and state transitions ∆ = ∆in ⊎ ∆st.

2. The automata are input-enabled (or receptive) in the sense that every change of an input variable is possible in every state and all transitions in ∆in are guarded by true.

3. All transitions in ∆st are guarded by clock constraints of the form c ∈ [l, u] involving only a single clock.

The semantics of AX is defined in terms of steps and runs, inherited from the definition of A, and in terms of the signals carried by these runs. With each compound step (q, v)

δ,t -→ (q ′ , v ′ ) such that λ(q) = v and λ(q) = v ′ , we associate the X-signal f v,v ′ • t.

The signal carried by a run is the concatenation of the signals carried by its steps. We denote by [[A]] ⊆ S(X) the set of signals carried by all runs of A and use [[A]]in, [[A]]ou and [[A]]io for the sets of their projections on the respective sets of variables. In particular, [[A]]io ⊆ S(Xio) is the observable behavior of A. Likewise we will use µ([[A]]) and µ([[A]

]io) for the untiming of those signal languages.

Given two timed automata A and A ′ having the same set Xio of interface variables, we say that A ′ is an over approximation of A, denoted by

A ⊑ A ′ , if [[A]]io ⊆ [[A ′ ]
]io. This will always be the case when A ′ is obtained from A by relaxing some of the timing constraints, or by merging two or more discrete states.

Composition

We now define the composition of two automata with variable sets X 1 and X 2 such that X 1 st ∩X 2 st = ∅ where interaction between components is realized via the shared variables

X = X 1 ∩ X 2 = (X 1 in ∩ X 2 in ) ⊎ (X 1 ou ∩ X 2 in ) ⊎ (X 2 ou ∩ X 1 in ).
When one automaton takes a transition that changes the value of a shared variable, the other automaton must take a similar transition as well. If the variable is an input for both it remains an input of the composed system. On the other hand, a variable which is an output variable of one automaton and an input for the other, becomes a state variable of the composed system.

A composition is cyclic is there are loops of influence between components: (X

1 out ∩ X 2 in = ∅) ∧ (X 2 out ∩ X 1 in = ∅)
. Cyclic composition may introduce, in certain circumstances, unstable behaviors consisting of spontaneous oscillations between values without any external stimulus. Our implementation uses the algorithm of [START_REF] Malik | Analysis of cyclic combinational circuits[END_REF] to check stability of cyclic compositions, but to simplify the presentation we restrict ourselves to acyclic composition.

DEFINITION 9 (COMPOSITION: VARIABLE CLASSIFICATION).

The set of variables in a composition of two timed automata over variable sets

X 1 and X 2 , is X = X 1 ∪ X 2 , where Xst = X 1 st ⊎ X 2 st , Xin = (X 1 in -X 2 ou )∪(X 2 in -X 1 ou ), and Xou ⊆ X 1 ou ⊎X 2 ou .
Note that the definition of Xou is not unique, permitting any subset of X 1 ou ⊎ X 2 ou to reflect the liberty in deciding which variables in a component are to be exposed to the external world. We do not include this choice of Xou in the formal definition of the composition in order to keep it associative. When we apply it in practice we compose all the automata together and specify explicitly the set of output variables of the product. The following definition identifies global states of the product as pairs of states whose valuations are compatible.

DEFINITION 10 (CONSISTENT GLOBAL STATES).

Let A X 1 = (A 1 , X 1 , λ 1 ) and A X 2 = (A 2 , X 2 , λ 2 ) be two timed automata. We say that a pair of states (q 1 , q 2 ) ∈ Q 1 × Q 2 is consistent if λ 1 (q 1 ) /X = λ 2 (q 2 ) /X . We denote the set of consistent global states by

Q 1 × Q 2 .

DEFINITION 11 (COMPOSITION OF TIMED AUTOMATA). Let

A X 1 = (A 1 , X 1 , λ 1 ) with A 1 = (Q 1 , q 1 0 , C 1 , I 1 , ∆ 1 ) and A X 2 = (A 2 , X 2 , λ 2 ) with A 2 = (Q 2 , q 2 0 , C 2 , I 2 , ∆ 2
), be two timed automata with variables, such that (q 1 0 , q 2 0 ) is consistent.

Their composition is A X 1 A X 2 = AX = (A, X, λ) with A = (Q, q0, C, I, ∆) where X = X 1 ∪ X 2 , classified accord- ing to Definition 9, Q = Q 1 × Q 2 , q0 = (q 1 0 , q 2 0 ), C = C 1 ⊎ C 2 , I((q 1 , q 2 )) = I 1 (q 1 ) ∧ I 2 (q 2
)) for every (q 1 , q 2 ) and the transition relation consists of all transitions of the form δ = ((q 1 , q 2 ), g, γ, (q ′1 , q ′2 )) for which one of the following holds:

1. q ′2 = q 2 and there is a transition δ = (q 1 , g, γ, q ′1 ) ∈ ∆ 1 such that λ 1 (δ) = f and f /X is the identity function 2. q ′1 = q 1 and there is a transition δ = (q 2 , g, γ, q ′2 ) ∈ ∆ 2 such that λ 2 (δ) = f and f /X is the identity function 3. there are two transitions

δ 1 = (q 1 , g 1 , γ 1 , q ′1 ) ∈ ∆ 1 and δ2 = (q 2 , g 2 , γ 2 , q ′2 ) ∈ ∆ 2 such that λ 1 (δ 1 ) = f 1 , λ 2 (δ 2 ) = f 2 , f 1 /X = f 2 /X is not the identity function, g = g 1 ∧ g 2 and γ = γ 1 • γ 2
The mapping λ : Q → X is defined for every global state as λ((q 1 , q 2 )) = λ 1 (q 1 ) λ 2 (q 2 ).

The first two cases in the definition of ∆ correspond to local transitions of A 1 and A 2 that do not touch shared variables and to which we apply the interleaving semantics. The third case corresponds to two transitions, one in each automaton, whose respective assignments change the values of a shared variable in a consistent way. It is not hard to see that state consistency as well as properties 1-3 above are preserved under composition. We mention a special class of timed automata which is closed under acyclic composition.

DEFINITION 12 (INPUT-DEPENDENT TIMED AUTOMATA).

A timed automaton A is input dependent if every non-trivial cycle in its transition graph involves at least one transition which changes the value of some input variable.

PROPOSITION 2 (CLOSURE UNDER ACYCLIC COMPOSITION).

If both A X 1 and A X 2 are input-dependent, so is their acyclic composition

A = A X 1 A X 2 .
PROOF. Suppose, without loss of generality, that X 1 ou ∩ X 2 in = ∅. Suppose A does have a non-trivial cycle without change in its input. Then, at least one of its projections on A 1 or A 2 must be a non-trivial cycle. Such a cycle in A 1 will contradict the fact that A 1 is input-dependent. Otherwise, the projection on A 1 is a trivial cycle without a change in its output, and the induced cycle in A 2 contradicts the fact that A 2 is input-dependent.

An important property of input-dependent automata is that there is a constant k such that the number of output events is at most k times the number of input events.

THE ABSTRACTION TECHNIQUE

At this point we can describe our abstraction procedure, starting with the automaton AX modeling a network of timed components and applying the following sequence of steps

AX ⇒ A + Ĉ X ⇒ A r X ⇒ A Ĉ X ⇒ AX io ⇒ A m X io .
1. From AX we construct A + Ĉ X by adding auxiliary input clocks that do not participate in transition guards or invariants, but only observe the dynamics of the automaton and measure the time elapsed since each input event. An input clock is discarded after a finite amount of time when the chain of reactions triggered by its event terminates.

2. We apply the forward reachability algorithm to A + Ĉ X to obtain the interpreted timed automaton A r X having the same semantics as AX . It is however, annotated with additional (redundant) timing constraints involving clocks in Ĉ.

We relax the timing constraints of A r

X by projecting them on clocks in Ĉ to obtain A Ĉ X . To be more precise, each transition guard is projected on the clock associated with the input event that has triggered it.

We project A Ĉ

X on the interface variables to obtain AX io thus making some internal transitions silent.

5.

We then reduce the discrete state space of AX io by merging states which are equivalent in terms of the untimed behaviors they admit and after merging transitions guards we obtain the reduced automaton A m X io .

At the end of the process we have the following relationships between the observable semantics of these automata:

[[AX ]]io = [[A + Ĉ X ]]io = [[A r X ]]io ⊆ [[A Ĉ X ]]io = [[AX io ]] ⊆ [[A m X io ]]
and the following relation between the qualitative semantics

µ([[AX ]]io) = µ([[A + Ĉ X ]]io) = µ([[A r X ]]io) = µ([[A Ĉ X ]]io) = µ([[AX io ]]) = µ([[A m X io ]]
). In other words, we preserve the qualitative semantics of the automaton and relax, to some extent, its timing constraints.

Adding Input Clocks

The most original and hard to implement part of our procedure is the construction of A + Ĉ which requires monitoring the propagation of input events in an acyclic network of timed components. When an input event occurs it excites one or more of the components to which it is a direct input. Each of those components will react within some t ∈ [l, u] and emit an output event, which may trigger reactions in some further components, and so on. Due to acyclicity, a component which has reacted to an input event cannot be influenced anymore by that event. Consequently all input events leave the system within a finite amount of time, bounded by d • u * , where d is the depth of the network, the maximal number of serially-connected components, and u * is the maximal delay upper bound of the components.

For an input event to be alive in the system there must be at least one active clock triggered by it, and since each clock is reset by one event, the number of live events is bounded by the number of clocks in the system which is equal to the number of timed components. This is an upper bound and in practice the maximal number of live events can be much smaller due to logical interference or additional bounded-variability assumptions concerning the external environment. In the sequel we assume m to be the upper bound on the number of live input events for each input variable.

For every transition δ ∈ ∆ we let χ(δ) be the set of clocks reset to zero by the transition. We say that a transition is exciting if χ(δ) = ∅. An exciting transition is a transition which triggers processes that will eventually be concluded by transitions guarded by clocks in χ(δ). We will augment every discrete state of the automaton with additional machinery that keeps track of the events which are alive in this state, and relates pending changes of states (represented by active clocks) to these events. Let M = {0, . . . , m} where m is the maximal number of live events in the automaton. The additional structure consists of:

• An event-recording table (ℓ, θ) consisting of -A live-event counter ℓ : Xin → M indicating for each input variable x how many of its events are alive.

-An association function θ : C → (Xin × M ) ∪ {⊥} relating each active clock to the input event responsible for its activation. Event (x, i) is understood to be the i th -oldest x-event still alive in the system.

We denote the (finite) set of event-recording tables by E .

• A set of auxiliary input clocks:

Ĉ = {cx[i] | x ∈ Xin, i ∈ M } with the intended meaning that cx[i]
is the time elapsed since the occurrence of event (x, i). A valuation of these clocks is a function v : Ĉ → R ⊥ . We will refer to the original clocks of the components as internal clocks.

Computing ∆ + Ĉ Input: An extended state (q, ℓ, θ) ∈ Q + Ĉ and a transition δ = (q, g, γ, q ′ ) ∈ ∆ Output: A transition δ + Ĉ = ((q, ℓ, θ), g, γ, (q

′ , ℓ ′ , θ ′ )) ∈ ∆ + Ĉ γ ′ := γ; ℓ ′ := ℓ; θ ′ := θ if χ(δ) = ∅ if δ ∈ ∆in changing input variable x /* new event creation */ ℓ ′ (x) := ℓ ′ (x) + 1 e := (x, ℓ ′ (x)) γ ′ := γ ′ ∪ {cx[ℓ(x)] := 0} elsif δ ∈ ∆st
for i = 1 to ℓ ′ (x) if θ ′-1 (x, i) = ∅ for j = i to ℓ ′ (x) -1 γ ′ := γ ′ ∪ {cx[j] := cx[j + 1]} for each c ∈ θ ′-1 (x, j + 1) θ ′ (c) := (x, j) ℓ ′ (x) := ℓ ′ (x) -1
Table 1: The algorithm for computing ∆ + Ĉ .

We can now proceed to the construction of the automaton. Since this construction does not affect the mapping of states to variable valuations we define it in terms of A from which we construct

A + Ĉ = (Q + Ĉ , q + Ĉ 0 , C ∪ Ĉ, I + Ĉ , ∆ + Ĉ ) where Q + Ĉ = Q × E and q + Ĉ 0
= (q0, ℓ0, θ0) where ℓ0(x) = 0 for every x, all clocks in Ĉ are inactive and θ0(c) = ⊥ for every c ∈ C.

The transition relation ∆ + Ĉ consists of transitions of the form δ ′ = ((q, ℓ, θ), g, γ, (q ′ , ℓ ′ , θ ′ )) based on transitions of the form δ = (q, g, γ, q ′ ) ∈ ∆ where γ is a clock assignment on C ∪ Ĉ whose projection on C is γ. The updated event recoding table (ℓ ′ , θ ′ ) and the extended assignment γ are computed from (ℓ, θ), g and γ according to the algorithm in Table 1. This procedure has four major parts.

1. Initialization: γ ′ inherits the clock assignments for the internal clocks from γ and the initial event-recording table is the same as in the source state.

2. Treatment of excitation: when a transition triggers a new internal processes by resetting clocks, these clocks should be associated with the input event responsible for their excitation. There are two cases:

(a) New event generation: the transition is due to a new input event on x and in this case we increment the x event counter, initialize a new input clock and keep the responsible event in a temporary variable e.

(b) Event propagation: the exciting transition is not related to a new input event, and in this case the responsible input event is inherited from the clock c guarding the transition.

Then every clock reset by the transition is associated with the input event in e.

3. Association book keeping: when clocks become inactive or when they are shifted, their association is updated.

4. Event death detection: if no clock points via θ to event (x, i) the event is no longer alive and we discard clock cx[i]. To keep the number of clocks finite we "shift" clocks cx[i + 1], . . . , cx[ℓ(x)] to the left and modify the association function accordingly. We use kill(x, i) to denote this operation.

This procedure maintains the event-detection table well-formed:

1. Only active internal clocks are associated with input events:

θ(c) = ⊥ iff v(c) = ⊥.
2. These clocks are associated only with live events: θ(c) = (x, i) only if i ≤ ℓ(x).

3. Each live event has at least one internal clock associated with it: i ≤ ℓ(x) only if ∃c θ(c) = (x, i).

4. Only input clocks associated with live events are active:

v(cx[i]) = ⊥ iff i ≤ ℓ(x).

Reachability Computation and Projection

Automaton A + Ĉ is an ordinary timed automaton except for the fact that the denotation of its input clocks may vary from one state to another due to clock shifting. Its configurations are of the form ((q, ℓ, θ), (v, v)) where (v, v) is a joint valuation of C ∪ Ĉ. After reachability computation we obtain the interpreted timed automaton whose states are of the form ((q, ℓ, θ), Z)) where Z is a zone over C ∪ Ĉ. As described in Section 2, we intersect invariants and transition guards with these zones to obtain the interpreted timed automaton A r X = (A r , X, λ) with A r = (Q r , X, q r 0 , C ∪ Ĉ, I r , ∆ r ).

The automaton A Ĉ = (Q r , q r 0 , Ĉ, I Ĉ , ∆ Ĉ ) is constructed from A r by projecting the timing constraints on clocks Ĉ. For each state p = ((q, ℓ, θ), Z) ∈ Q r let Ĉ(p) be the set of input clocks active at p. The invariant of p in A Ĉ is I Ĉ (p) = I r (p)/ Ĉ(p) . For every transition δ = (p, g, γ, p ′ ) ∈ ∆ r we define a transition δ Ĉ = (p, g Ĉ , γ Ĉ , p ′ ) ∈ ∆ Ĉ by letting γ Ĉ = γ/ Ĉ and

g Ĉ =  γ/ Ĉ if δ ∈ ∆ r in γ/ θ(c) if δ ∈ ∆ r in and

is guarded by c

We project A Ĉ on the set of interface variables Xio = Xin ⊎ Xou to obtain AX io = (A Ĉ , Xio, λio). This operation renders some transition invisible in the sense of not affecting variables but, unfortunately, not all of those can be eliminated. Consider an input event (x, i) which is responsible for the excitation of an internal timed component. It may happen that the reaction of that component has no further consequence and hence event (x, i) dies and its clock should be removed. The change in clock denotation due to shifting should be visible in the reduced model in order to preserve its intended semantics.

Minimization

The next step is the reduction of the discrete state space by merging states which are equivalent in terms of the qualitative behaviors they admit. This work is inspired by the minimization with elimination of silent transitions for the untimed case [START_REF] Bouajjani | Safety for Branching Time Semantics[END_REF] and its extension to timed systems [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF]. From the previous step we have a timed automaton whose transitions are decorated by clock assignments on Ĉ and by assignments on Xio. We minimize the automaton with respect to the alphabet Σ = FX io × Γ( Ĉ). We use τ to denote the silent element (f, γ) where both f and γ are the identity functions and use symbols like a to denote the other elements of Σ which are visible. To simplify notation we describe the minimization with respect to a Σ-labeled timed automaton A = (Σ, Q, q0, Ĉ, I, ∆) with transitions of the form (q, a, g, γ, q ′ ). We use notation q a -→ q ′ to denote the existence of an a-labeled transition for q to q ′ . The minimization is a sequence of three steps

A ⇒ A o ⇒ A b ⇒ A m explained below.
1. To remove silent transitions we identify states that are the target of an observable transition and collapse into them all their τ -successors to construct a state whose invariant is the union of all the invariants of these states. Every sequence of silent transitions is thus replaced by a single time step.

2. We compute the bisimulation relation ∼ with respect to Σ on states of A o and let the states of A b be the equivalence classes of ∼. The invariant of each class is the convex hull of the invariants of its members. All transitions are kept.

3. For every pair of states we merge all the transitions between them having the same a-label into one transition whose guard is the convex hull of the guards of those transitions.

Eliminating Silent Transitions

A state q in A = (Σ, Q, q0, I, ∆) is an observable entry point if it is the initial state q0 or there is some observable a and state q ′ such that q ′ a -→ q. We denote these states by D(Q) . A state q ′ ∈ D(Q) is a silent-successor of q ∈ D(q) if there is a path q

τ -→ q1 τ -→ • • • q k τ -→ q ′ in
the automaton. We denote by q the set containing q and all its silent successors. Note that all states in q admit the same variable valuation over Xio.

DEFINITION 13 (AUTOMATON

A o ). The automaton A o = (Σ, Q o , q o 0 , Ĉ, I o , ∆ o ) is constructed from A = (Σ, Q, q0, Ĉ, I, ∆) as follows: • Q o = { q : q ∈ D(Q)}, q o 0 = q0 • I o ( q ) = S p∈ q I(p)
• ∆ o contains a transition ( q , a, g, γ, q ′ ) for every transition (q ′′ , a, g, γ, q ′ ) ∈ ∆ such that q ′′ ∈ q .

It is not hard to see that the invariants thus obtained are convex, because clocks in Ĉ are never reset by silent transitions. Hence [[A o ]] and [[A]] coincide. Note also that A o has the same property as the reachability graph in the sense that every sequence of transitions is realizable in the original automaton.

Merging Bisimilar States

Let A = (Σ, Q, Ĉ, q0, I, ∆) be a timed automaton without silent transitions. The qualitative bisimulation relation over Q is the largest equivalence relation satisfying

q ∼ q ′ ≡ ∀a ∈ Σ (q a -→ p ⇒ ∃p ′ (q ′ a -→ p ′ ∧ p ∼ p ′ )).
In other words q ∼ q ′ if the same qualitative observable behaviors can be generated from both. We let [q] denote the ∼ equivalence classes of q and denote the set of such classes by Q/ ∼. All elements of [q] admit the same variable labeling.

DEFINITION 14 (AUTOMATON

A b ). The automaton A b = (Σ, Q b , q b 0 , Ĉ, I b , ∆ b ) is constructed from A o = (Σ, Q o , q o 0 , Ĉ, I o , ∆ o ) as follows: • Q b = Q o / ∼, q b 0 = [q o 0 ] • I b ([q]) = F q ′ ∈[q] I o (q ′ )
• ∆ b contains a transition ([q], a, g, γ, [q ′ ]) for every transition (p, a, g, γ, p ′ ) such that p ∈ [q] and p

′ ∈ [q ′ ].
This transformation, by definition, preserves qualitative behavior, and may over-approximate the timed behavior due to the use of convex hull.

Merging Transitions

The last step is to merge transitions between every pair of states which agree on the transition label.

DEFINITION 15 (AUTOMATON

A m ). Automaton A m = (Σ, Q b , q b 0 , Ĉ, I b , ∆ m ) is obtained from A b = (Σ, Q b , q b 0 , Ĉ, I b , ∆ b
) by letting ∆ m consist of transitions of the form (q, a, g, γ, q ′ ) where

g = G {g ′ | (q, a, g ′ , γ, q ′ ) ∈ ∆ b }.
As in the previous step, qualitative semantics is preserved while the timed semantics may grow due to the use of convex hull. Let us remark that in many cases, S g ′ is already convex and the timed semantics is preserved by this step. We can guarantee preservation of timed semantics by this step if we restrict the merging of transitions and states to those whose corresponding unions are convex.

EXPERIMENTAL RESULTS

For lack of space we refer the reader to [START_REF] Salah | On Timing Analysis of Large Systems[END_REF] for some details on the implementation of the full tool chain starting from high-level description of the network of timed component down to the realization of all the steps described in the paper (35K lines of C++ code) inside the IF toolbox.

To demonstrate our approach and tool chain consider the circuit depicted in Figure 2, a part of a multiplier adapted from the tutorial [START_REF] Burleson | Wave-pipelining: A Tutorial and Survey of Recent |Research[END_REF] on wave pipelining, a technique for improving the throughput of sequential circuits beyond what is possible by a purely synchronous approach. Each tick of a periodic clock defines a temporal window in which each of the inputs may change its value. Jitter is modeled by the fact that each input may choose a different point in that window. Then the changes in the input propagate through 36 logic gates, each modeled by a timed automaton with one clock based on the modeling approach of [START_REF] Maler | Timing Analysis of Asynchronous Circuits using Timed Automata[END_REF] for modeling circuits with bi-bounded delays. In a purely-synchronous regime the frequency of input waves should be greater than the worst-case propagation time of the whole circuit. Wave pipelining allows one to use a higher frequency and let several waves be present simultaneously in different parts of the circuit. A crucial question in this methodology is to find the highest frequency in which waves do not interfere, that is, avoidance of situations where an elementary gate receives an input from wave i + 1 while it has not yet finished processing wave i. Questions of a similar nature exist at higher levels of abstraction where gates are replaced by software modules and We first explore the limits of a non-compositional approach applied directly to a product of 36 timed automata. The longest delay path in the circuit is 1086 and we first compose it with an input generator of period 1200 and jitter of 10 which generates only one wave through the circuit. In this setting, using our interleaving reduction [START_REF] Ben Salah | On Interleaving in Timed Automata[END_REF] we manage to complete the analysis within 7 minutes to obtain a reachability graph with more than 26K symbolic states and 50K transitions. When we slightly reduce the input period to 1000 to allow two simultaneous waves, the analysis gets stuck for hours and we need to resort to a compositional approach. As can be seen in the figure, the circuits admits 5 instances of the sub-circuit denoted by A, two of which are connected to the primary inputs. We compose this sub circuit, whose longest path is 362 with an input generator of period 247 and jitter 10 which may induce 2 simultaneous waves in the circuit. The reachability graph obtained has 213/321 states/transtions which are reduced by our technique to 34/58 from which we deduce an output jitter of 32. To obtain a model of the third instance of A which is exposed to the output of the first two, we compose A with an input generator of jitter 32 and repeat the process, this time going from 270/411 transitions/states in the reachability graph to an abstract model with 36/62 and output jitter of 54. To treat the last two instances of A we compose it with an input generator of jitter 54 and get exactly the same results as the previous step in terms of size or the graph and the reduced model. No interference is detected and we can deduce that the whole circuit is safe with an input frequency with period 247. When we repeat the same sequence of steps with a input of period 246, an interference is detected.

DISCUSSION

We have developed a new original technique for abstracting the behavior of timed components. The essence of this technique is to use the internal clocks to compute what the component can and cannot do and then get rid of these clocks by projecting on the observable input clocks that we introduce into the model. As a result we obtain a model which focuses on what the potential users of the component care about: the relation between the timing of input and output events. This model is faithful to the qualitative semantics of the component but may relax the temporal correlation between output events that depend on the same internal event. Such a reduced model can serve as a specification of the component in a component library and, as we have demonstrated in the case study, to allow us to analyze timed automata of unpreceded size and complexity.

Finding ways to evaluate the quality of the abstractions obtained by our technique is one of the items on our agenda. Over-approximation of a system by another can be obtained trivially and the quality of the abstract model should be be judged either by whether it is sufficiently detailed to prove some properties, or by quantitative means: how many spurious behaviors have been added. For the first criterion, it is hard to find large examples due to the intractability of timed automata analysis, and we intend to take some cases studied using analytical methods for performance analysis and see whether we can obtain tighter results. For the second approach, recent results on volume and entropy of timed languages [START_REF] Asarin | Volume and Entropy of Regular Timed Languages[END_REF] may provide a tool for measuring the degree of over-approximation.

Figure 1 :

 1 Figure 1: (a) A network of 2 components; (b) The automaton with an auxiliary clock; (c) The automaton after projection on the auxiliary clock; (d) The semantics of the network; (e) The approximate semantics after projection.

  guarded by clock c /* event propagation */ e := θ(c) for each c ′ ∈ χ(δ) θ ′ (c ′ ) := e for every non-resetting clock assignment in γ /* book keeping */ if of the form c := ⊥ θ ′ (c) := ⊥ elsif of the form c1 := c2 θ ′ (c1) := θ(c2) for each x ∈ Xin /* clock killing and shifting */

Figure 2 :

 2 Figure 2: A wave-pipelining circuit

We mention[START_REF] Jonsson | Cyclic Dependencies in Modular Performance Analysis EMSOFT[END_REF] as a recent attempt to reconcile these two approaches for cyclic components.

Unlike[START_REF] Daws | Reducing the Number of Clock Variables of Timed Automata[END_REF] where clock activity analysis was used to reduce dimensionality.

Note, however, that not all elements of (q, Z) are the start points of such compound steps because they do not necessarily satisfy g.

We use signals in this paper because our case study is a circuit for which signals are more appropriate. More theoretical background on the relation between signals and the alternative semantic domain for timed systems, time-event sequences consisting of events separated by time durations (which are also equivalent to the timed traces of[START_REF] Alur | A Theory of Timed Automata[END_REF]) can be found in[START_REF] Asarin | Timed Regular Expressions[END_REF].


Jérôme Margueron

E Khan

Suppression, persistence and reentrance of superfluidity in overflowing nuclear systems

Keywords: numbers: 67.85.Lm, 74.40.Kb, 21.60.Jz, 26.60.Gj

HAL is

Overflowing many-body fermionic systems exist in various situations going from the crust of neutron stars [1,[START_REF] Margueron | Neutron Stars Crust[END_REF] to ultra-cold atoms [START_REF] Stamper-Kurn | [END_REF]4]. Interestingly, these systems offer the possibility to study the coupling between two fluids with very different pairing properties [5,6]. In such systems, one fluid is localized inside an initial container, such as for instance a nuclear potential, and a second fluid is overflowing towards a larger container. Being in different environments, these two fluids can acquire different pairing gaps. In this paper, we address the question of the coupling between the two superfluids and their finite temperature properties.

At the transition between its outer and inner crust, neutron stars provide an example of such microscopic overflowing systems, commonly called neutron dripping [1]. In the outer crust, nuclei form a Coulomb lattice which gets more and more neutron rich as the density increases. When the maximum number of neutrons that a nucleus can sustain is reached, the overproduced neutrons drip out of nuclei. These neutrons populate the continuum states and shall be described within the band theory (see Refs. [START_REF] Ashcroft | Solid State Physics[END_REF][START_REF] Chamel | [END_REF] and references therein). In the present work, we shall consider the spherical Wigner-Seitz approximation to the band theory which limitations are discussed for instance in Ref. [START_REF] Chamel | [END_REF]. It should be noted that nuclei surrounded by an infinite neutron gas could exist as a stable configuration in neutron stars where they are bounded by gravitation, while isolated nuclei that exist for instance on earth are limited to the drip lines.

The first prediction of the suppression of pairing in overflowing Z = 50 nuclear systems was performed in Ref. [5]. It was proposed to attribute this suppression to the large coherence length of the weakly-superfluid neutrons gas: the neutron gas can penetrate the dense nuclear system and could impose its weak pairing field. It was however also noted in the same work that neutrons are dripping out of the double-magic nucleus 176 Sn. In a recent work, the pairing gap of the last occupied state was also predicted to be quenched in overflowing nuclear systems, metallic grains and cold-atoms [6]. It was concluded that the suppression of superfluidity is a generic fact of a fermionic superfluid overflowing from a narrow container into a much wider one. It shall be noted that in this work the nuclear model was mainly limited to ℓ=0 single particle states (s-states). The description of nuclear systems requires however the inclusion of ℓ > 0 single particle states for the bound and the mean-field resonance states. It is indeed well known that, close to the drip lines, resonance states play an important role for pairing properties and it is referred generally as continuum coupling [9,10]. It has recently regained some attention in nuclei close to the drip-line (see for instance Refs. [11,12] and references therein). The general question of continuum coupling in overflowing superfluid systems and various phenomenons such as persistence, suppression and reentrance of pairing remains to be studied. Pairing correlations in the ground state of weaklybound nuclei are commonly described by the Hartree-Fock-Bogoliubov (HFB) theory [START_REF] De Gennes | Superconductivity of metals and alloys[END_REF][START_REF] Ring | The Nuclear Many-Body Problem[END_REF]. In most of the HFB calculations the continuum is discretized by solving the HFB equations with box boundary conditions [START_REF] Dobaczewski | [END_REF]. In this paper a systematic analysis based on several overflowing isotopic chains is performed and it is shown that pairing quenching and continuum coupling are strongly related. A pairing reentrance phenomenon with increasing temperature is predicted for Z = 50 overflowing systems.

In the present work, an HFB approach in coordinate representation is employed. This model has already been applied to describe nuclei and Wigner-Seitz cells in a fully self-consistent framework (see Ref. [16] and references therein). The Skyrme SLy4 interaction [17] is used in the mean-field channel, and is completed by the ISS pairing force which is adjusted to the BCS pairing gap predicted by bare nucleon-nucleon potentials [16]. All the bound states are considered, the angular momentum goes up to J max = 27/2, and we take a large box radius R box =27.4 fm ensuring an adequate description of the continuum. An almost constant neutron density at the edge of the Wigner-Seitz cell is obtained using mixed Dirichlet-Von Neumann boundary conditions. The expected nuclei in neutron stars located at the transition between the outer crust and the inner crust have a proton number Z around 30 to 50, depending on the models [18]. We therefore selected 8 isotopes given in Table I formed HFB model based on the Gogny interaction [19]. For these selected isotopes, the neutron-drip number N drip , defined as the neutron number of the last nucleus before the two-neutrons separation energy S 2n (N ) = E(N ) -E(N -1) changes its sign [START_REF] Ring | The Nuclear Many-Body Problem[END_REF], is given in table I. The total neutron occupation number of resonance states N res for the drip-line nuclei is also given. The calculation of N res requires the identification of resonance states which, in our case, are defined as positive energy states with rms radii lower than half the size of the box. It is interesting to remark from Table I that the drip-line nuclei with a number of neutrons that coincides with the well-known magic numbers (82 and 126) have no states in the continuum. The shell occupation in this case is 0 or 1, as in magic nuclei. We therefore group Kr, Sr, Sn and Te isotopes in the same group A 2 . The persistence of magicity with the same magic numbers as in stable nuclei might be due to the sphericity of these nuclei. This is a well known stabilization effect of magicity in nuclear structure [START_REF] Ring | The Nuclear Many-Body Problem[END_REF]. In the case of Ni, Zr, Mo and Ru, the drip-line occurs in more complicated shell structure partially involving resonance states and these isotopes are grouped in A 1 .

The drip-line isotopes identified in Table I can be considered as the seed nuclei from which the overflow occurs. The dripping of neutrons shall therefore be influenced by the microscopic structure of these seed nuclei. Nuclei belonging to the group A 1 have a resonance occupation number N res which goes from 2.2 to 8.0 particles. This number reveals the large continuum coupling. The number of particles in the resonance states is zero for nuclei belonging to the group A 2 , since in the magic nuclei located at the drip-line, pairing correlations are quenched and continuum coupling therefore largely suppressed. From a microscopic analysis, the structure of drip-line nuclei is qualitatively different between the group A 1 and A 2 . In the following, we show how these differences impact the quenching of pairing correlations at overflowing. Figs. 1 and 2 display the average neutron pairing gaps versus the neutron number (top panel) and the difference between the neutron number and the neutron drip N -N drip (bottom panel). The average neutron pairing gap is obtained from the neutron pairing field given by the HFB solution and is defined as,

∆ ≡ d 3 r∆(r)κ(r) d 3 rκ(r) , (1)
where ∆(r) and κ(r) are the pairing field and pairing tensor obtained from the solution of the finite temperature HFB model [START_REF] Margueron | Neutron Stars Crust[END_REF][START_REF] Sandulescu | [END_REF]. Fig. 1 represents the neutron pairing gaps for the A 1 isotopes while in Fig. 2 are shown the neutron pairing gaps for the A 2 isotopes. In the case of nuclei from the A 1 group, the neutron pairing gap persists beyond the drip line (see bottom panel of Fig. 1). The continuum coupling preserves the pairing diffusivity around the Fermi energy: the occupancy of the scattering states beyond the drip-line does not suppress superfuidity. The presence of an overflowing neutron gas has therefore a limited effect on the pairing gap for the A 1 isotopes, showing the persistence of superfluidity. In the case of the A 2 isotopes, a suppression of the average pairing gap just beyond the drip line is observed (Fig. 2). The presence of a magic nucleus at the drip line have therefore a strong influence on the pairing gap at and beyond the drip line: the large spacing between the last occupied state and the first excited state (resonance state) suppresses superfluidity. superfluidity, even in overflowing nuclear systems. In Ref. [6], the quenching of pairing in overflowing systems has been predicted upon overflow of trapped fermions. It should be underlined that in the present work, the mean-field in nuclear systems have a centrifugal term which gives rise to the mean-field resonance states and continuum coupling, whereas the conclusions obtained in Ref. [6] are applicable only to overflowing systems involving ℓ = 0 single particle states. In more general systems, like in the crust of neutron stars, a more sophisticated theoretical model such as the present HFB one predicts a suppression of superfluidity only if the continuum coupling is quenched, by the shell structure for instance. It shall however be mentioned that for the description of pairing in nuclei close to the transition point the HFB model shall be complemented by particle-projection methods.

The persistence of superfluidity upon overflow of bound neutrons might not be the only consequence of continuum coupling: in the case where pairing is suppressed, the increase of temperature may generate the reentrance of superfluidity. The finite-temperature HFB model [START_REF] Margueron | Neutron Stars Crust[END_REF][START_REF] Sandulescu | [END_REF], is employed to study the reentrance of pairing in the thermal state of overflowing even-even nuclear systems. The temperature-averaged pairing gap for 160,176,180,200 Sn is shown in Fig. 3. In 160 Sn and 200 Sn it behaves as expected from HFB theory: the pairing gap vanishes at the critical temperature T c = 0.57∆(T ≈ 0) (see Ref. [29] and references therein). In the case of 176 Sn and 180 Sn, the reentrance of superfluidity is observed with increasing temperature. This reentrance is induced by the presence of resonances states in the spectrum of these nuclear systems: Being slightly too high in energy, these states are not occupied at zero temperature (see Table I), while at finite temperature, they can be partially occupied from the Fermi-Dirac distribution. At low temperature, the pairing correlations can therefore be switched on allowing the reapparition of the superfluid state. The reentrance critical temperature depends on the step in energy between the last occupied bound state and the first resonance one, which changes from one system to another, as observed in Fig. 3 for 176 Sn and 180 Sn. In the case of 200 Sn, this energy step is too large to give rise to the reentrance of superfluidity before the highest critical temperature is reached.

The 180 Sn overflowing system has an interesting phase diagram including three critical temperatures: with increasing temperature, two of them correspond to the vanishing of superfluidity (T c1 ∼ 11 keV and T c3 ∼ 1 MeV) and one to its reappearance (T c2 ∼ 300 keV). The lowest critical temperature T c1 is associated to the transition from the superfluid to the normal state in the overflowing neutron gas. The highest critical temperature T c3 is similar for 160,176,180 Sn, indicating that superfluidity has been restored in the seed nucleus of 176,180 Sn between T c2 and T c3 . This superfluidity is mainly built on resonances populated at finite temperature. More generally, pairing reentrance in hot systems is observed for isotopes belonging to the group A 2 where resonances are too high in energy to participate to pairing at zero temperature but close enough to the last occupied state to be reached at finite temperature.

Reentrance of superfluidity at finite temperature have been predicted in nuclear systems such as in oddnuclei [20], rotational motion of nuclei [21], and the deuteron pairing channel in asymmetric infinite matter [22]. It was aslo predicted in polarised 3,4 He [23][24][25] and in spin asymmetric cold atom gas [26,[START_REF] Levin | Ultracold Fermi Gases[END_REF]. In all these systems, pairing at zero temperature is generated by an attraction among Fermions of different spin or isospin. Superfluidity is therefore maximum in spin or isospin symmetric systems for which there is a matching of the Fermi levels of the constituent Cooper-pairs. Temperature T in keV Breaking the spin or isospin symmetry disfavor pairing while temperature in asymmetric systems acts in favor of restoring the broken symmetry and can eventually induce a reentrance of pairing. In the present case, the condition for pairing to be analyzed is related to the equal amount of occupied and unoccupied states. At shell closure, this symmetry is maximally broken. The reentrance phenomenon analyzed in this paper is based on the restoration of this condition for pairing at finite temperature where resonance states play a major role. Now we analyze the stability of the reentrance prediction and we focus on the prediction for 176 Sn. The dependence on the Skyrme interaction is first analyzed. Among various Skyrme interactions (SLy4, RATP, SKI5, SKM * , SGII, SIII), we selected the ones that predict 176 Sn at the drip-line (group A 2 ), that are: SLy4, RATP, SKI5 and SIII. We also found that SLy4 and RATP a f7/2 resonance state at low-energy (between 1 and 2 MeV), SIII a p3/2 state around 1 MeV while and the lower-energy resonance state with SKI5 is found above 4 MeV. We found that SLy4, RATP and SIII Skyrme interactions predict a reentrance phenomenon in 176 Sn, as illustrated on Fig. 4, while SKI5 does not. We also show on Fig. 4 that all the interactions having a low-energy resonance in the window 0 to 2 MeV above the Fermi energy (RATP, SIII and SLy4) behave similarly, confirming our previous conclusions that the reentrance phenomenon is related to the vicinity of resonance states. The dependence on the choice of the Skyrme interaction (RATP, SLy4 and SIII) is also shown. The size of the box have also been varied from 28 to 30 fm, and the effect is shown to be small on Fig. 4.

In summary, we have investigated the pairing properties of nuclear systems upon overflowing superfluid neutrons. Suppression, persistence and reentrance of superfluidity can occur in these finite systems. From a systematic HFB calculations on 8 isotopic chains, the pairing properties is shown to be strongly correlated to the continuum coupling, both at zero and finite temperature. At zero temperature, the coupling between the seed nucleus and the gas is weak, and a formal separation of their properties into a nucleus plus a gas provides a qualitative understanding of the suppression and the persistence of superfluidity. With increasing temperature in the normal state, the Fermi-Dirac distribution can populate the resonance states giving rise to the reentrance of superfluidity. The pairing correlations in the nuclear system are switched on again and consecutive critical temperatures are predicted.

The understanding of the suppression, persistence and reentrance of superfluidity in nuclear systems, deeply related to the continuum coupling, opens wide perspectives for discoveries in weakly bound nuclei, as well as it sheds new light on the transition between the inner and outer crusts in neutron stars. The role of resonances around the neutron drip not only changes the microscopic understanding of the neutron drip-out mechanism, but it also modifies the thermal properties of the crust through the strength of the pairing interaction [30]. The temperatures at work during cooling are typically of the order of 10 to 500 keV [1] and coincide with the critical temperatures of the reentrance phenomenon. As a consequence, the novel pairing reentrance phenomenon analyzed in this paper is expected to modify the thermodynamical and cooling properties in the crust of neutron stars. The links with other superfluid Fermi-systems shall be investigated in the near future. For instance in cold Fermionic atoms overflowing from an inner trap to a larger one [START_REF] Stamper-Kurn | [END_REF]4], it is known that stable path close to the centrifugal energy are the classical analog of the quantal resonances. It will therefore be interesting to investigate the role of these stable paths on the superfluid properties of overflowing cold Fermionic atoms.

FIG. 1 :

 1 FIG. 1: (color online) Neutron pairing gaps versus neutron density N (top panel) and versus N -N (drip) (bottom panel) for the isotopes in the group A1 (see the text for more details).

Figs. 1 FIG. 2 :

 12 FIG.2:(color online) Same as Fig.1for isotopes in the A2 group.

FIG. 3 :

 3 FIG.3:(Color online) Temperature averaged neutron pairing gap versus temperature for160,176,180,200 Sn. A superfluid reentrant effect is observed for 176 Sn and 180 Sn.

TABLE I :

 I and located around Z=28, 40 and 50. It is well adapted to perform a spherical HFB calculation since these nuclei are predicted spherical near the neutron drip-line from a de-Isotope Z N drip group Nres Isotope acronym, number of protons Z, number of neutrons of the last nucleus before the drip line N drip , for the selected set. Isotopes for which the drip-line nucleus is nonmagic (magic) belongs to the group A1 (A2, respectively). The total occupation number of resonance states for the dripline nuclei Nres is shown in the last column (see the text for more details).

	Ni	28	60	A1	3.0
	Kr	36	82	A2	0.0
	Sr	38	82	A2	0.0
	Zr	40	84	A1	2.2
	Mo	42	90	A1	8.0
	Ru	44	92	A1	3.0
	Sn	50	126	A2	0.0
	Te	52	126	A2	0.0

The authors thanks M. Baldo, P. Schuck, X. Viñas and M. Urban for the interesting discussions during the completion of this work. This project was partially supported by the ANR NExEN and SN2NS contracts, the Institut Universitaire de France and by COMPSTAR, an ESF Research Networking Program.