Julien Deantoni

Charles André

Régis Gascon

CCSL denotational semantics

Keywords: CCSL, UML, time constraints, semantics, denotational CCSL, UML, contraintes temporelles, sémantique, dénotationnelle

The Clock Constraint Specification Language (ccsl) has been informally introduced in the specifications of the uml Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE). In a previous report entitled "Syntax and Semantics of the Clock Constraint Specification Language", we equipped a kernel of ccsl with an operational semantics. In the present report we pursue this clarification effort by giving a mathematical characterization to each ccsl constructs.

Introduction

Modeling of distributed systems, as well as electronic systems with multi-cores or multi-clock domains, needs multiple time bases. The uml profile for Modeling and Analysis of Real-Time and Embedded systems [START_REF] Omg | UML Profile for MARTE, v1.0. Object Management Group[END_REF] (marte) addresses this modeling issue through its rich model of Time. marte also introduces the concept of clock constraints and proposes the non-normative language ccsl (short for Clock Constraint Specification Language) for specifying such constraints.

The marte time model has been first presented at the 10 th international conference on Model Driven Engineering Languages and Systems [START_REF] André | Modeling time(s)[END_REF]. This paper introduced the concepts of time bases, clocks and clock constraints. ccsl appeared only in a few illustrative examples. On the other hand, the omg specification of marte contains neither a precise syntax nor a formal semantics for ccsl; only an informal (English) semantics is given. This lack of formal description of ccsl has been partially filled in our research report entitled "Syntax and Semantics of the Clock Constraint Specification Language" [START_REF] André | Syntax and semantics of the clock constraint specification language (CCSL)[END_REF], which described a kernel of ccsl and provided a structural operational semantics for this kernel. The present report contibutes further to the semantics of ccsl by giving full mathematical characterization of the clock relations and clock expressions of ccsl.

ccsl has also been used in verification of time requirements [START_REF] Mallet | Marte CCSL to execute East-ADL timing requirements[END_REF][START_REF] André | Specification and verification of time requirements with CCSL and esterel[END_REF]. The contribution of the present report is to define a denotational semantics for ccsl. This semantics introduce formally the notion of birth and death of both clock constraints and clocks. The goal of this formalization is to pave the road of using ccsl with different modes, where each mode is a node of a an automaton.

The report consists of three main sections. The first section introduces the multiform logical time, the clocks, and the clock constraints. A clock constraint is a clock relation that applies to two clock expressions. In this section, all the clock relations from the kernel ccsl are mathematically defined. The primitive clock expressions of the kernel ccsl are characterized in the same way.

The second section first explains how libraries can be constructed over the ccsl kernel. The third section describes the perspectives opened by such a formal modeling approach.

2 Clock Constraint Specification Language

Multiform logical time

marte Time model deals with both discrete and dense times. In marte, a clock gives access to a time structure made of time bases, which are themselves ordered sets of instants. A clock can be either dense or discrete. This report focuses on the structural relations between clocks and these relations do not differentiate between dense and discrete clocks. However, some relations only apply to discrete clocks and others apply to both discrete and dense clocks. Logical clocks refer to discrete-time logical clocks and represent logical time.

Leslie Lamport [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] introduced logical clocks in the late 70's. The logical clocks associate numbers (logical timestamps) with events in a distributed system, such that there exists a consistent total ordering of all the events of the system. These clocks can be implemented by counters with no actual timing mechanisms. In the 80's, the synchronous languages [START_REF] Benveniste | The synchronous approach to reactive and real-time systems[END_REF] introduced their own concept of logical time. This logical time shares with Lamport's time the fact that they need not actually refer to physical time. Logical time only relies on (partial or total) ordering of instants. In what follows, we consider logical time in the sense of synchronous languages. In the synchronous language Signal [8], a signal s is an infinite totally ordered sequence (s t ) t∈N of typed elements. Index t denotes a logical instant. At each logical instant of its clock, a signal is present and carries a unique value. Signal is a multi-clock (or polychronous) language: it does not assume the existence of a global clock. Instead, it allows multiple logical clocks. Signal composition is ruled by operators which are either mono-clock operators (composing signals defined on a same clock) or multi-clock operators (allowing composition of signals having different clocks).

Indeed, a logical clock can be associated with any event. This point of view has been adopted in the marte time model [START_REF] Omg | UML Profile for MARTE, v1.0. Object Management Group[END_REF]Chap. 10]. A logical clock "ticks" with each new occurrence of its associated event. Synchronous languages like Esterel exploit this property. In an Esterel program, time may be counted in seconds, meters, laps. . . (see the Berry's RUNNER program [START_REF] Berry | The Esterel Language Primer, version v5_91[END_REF] which describes the training of a runner). This variety of events supporting time leads to the concept of multiform time. More technical examples can be found in automotive applications. For instance, the electronic ignition is driven by the angular position of the crankshaft rather than by a chronometric time (see our study of a knock controller in a 4-stroke engine [START_REF] André | A multiform time approach to real-time system modeling: Application to an automotive system[END_REF]).

In this report, we consider both dense and logical clocks and their relationships through clock constraints.

Because the notion of instant and the ordering of such instants are the core of the proposition, we first introduce the relations we defined on the instants.

Instants and Time Structure

Instants are the basic elements which are manipulated all along this report. An instant can be seen as an event occurrence, occurring at a specific (logical) time. Expliciting the fact that an instant as a specific logical time implies that instants can be partially ordered. To do so, we use specific instant relations. An instant relation between two instants reflects a specific ordering between the considered instants. We defined five kinds of instant relations, derived from two main relations.

Causal and chronological relations over a set of instant are defined in a time structure. A time structure T is a triple I, ≺, ≡ made of a set of instants I and two main relations on instants verying the conditions below.

• The precedence relation ≺ is a strict order relation on I (irreflexive, asymmetric and transitive)1 .

• The coincidence relation ≡ is an equivalence relation (reflexive, symmetric and transitive).

It reflects the fact that two instants have the exactly same logical time.

• The precedence and coincidence relations verify the following properties: for every i 1 , i 2 , i 3 ∈ I

-if i 1 ≺ i 2 and i 2 ≡ i 3 then i 1 ≺ i 3 , -if i 1 ≺ i 2 and i 1 ≡ i 3 then i 3 ≺ i 2 .
From these two relations, one can define additional relations associated to any time structure:

• The causality relation is defined as the union of the precedence relation and the coincidence relation.

∀i 1 , i 2 ∈ I, i 1 i 2 ⇔ (i 1 ≺ i 2 or i 1 ≡ i 2 ).
Note that is not really a partial order. By definition, this relation is reflexive and transitive, but it is not anti-symmetric. If i 1 i 2 and i 2 i 1 we can deduce that i 1 ≡ i 2 but coincidence does not imply equality.

• The exclusion relation # is defined as the union of the precedence relation and its converse relation. Formally, we have

∀i 1 , i 2 ∈ I, i 1 # i 2 ⇔ (i 1 ≺ i 2 or i 2 ≺ i 1 ).
This impose that instants i 1 and i 2 must not be coincident.

• Finally, the independence relation corresponds to the absence of other relations.

∀i 1 , i 2 ∈ I, i 1 i 2 ⇔ neither (i 1 ≺ i 2 ) nor (i 2 ≺ i 1 ) nor (i 1 ≡ i 2 ).
This relation can be used to express concurrency between two events.

The graphical representation of these different instant relations is given in Table 1.

instant

Clocks

We adopt a simplified model compared to the one defined in marte. However, this model is still linked to marte and has already been used in our papers (see for instance [START_REF] Peraldi-Frati | Scheduling multi clock real time systems: From requirements to implementation[END_REF]). This model considers that a clock is an ordered set of instants. A clock has a lifetime delimited by a birth instant and a death instant.

Formally, a Clock c is a 5-tuple I c , ≺ c , c ↑ , c ↓ , ≡ c ↓ where I c is a possibly infinite set of instants, c ↑ ∈ I c is the birth instant of c, and c ↓ ∈ I c is the death instant of c, ≡ c ↓ is a coincidence relation and ≺ c is an order relation on I c ⊎ {c ↑ , c ↓ } satisfying the following conditions:

• The restriction of ≺ c on I c is a strict order relation.

• All instants of I c are strictly ordered (≺ c is total):

∀i, j ∈ I c , (i = j) ⇒ (i ≺ c j) or (j ≺ c i).
• The birth strictly precedes all the other instants of the clock:

∀i ∈ I c ⊎ {c ↓ }, c ↑ ≺ c i.
• Every instant precedes the death but the last one that may coincide with it:

∀i ∈ I c ⊎ {c ↑ }, ((i ≺ c c ↓ ) ∨ (i ≡ c ↓ c ↓ ))
The set of instants I c represents the occurrences or ticks of the clock c. This is why birth and death does not belong to this set. A clock can have a finite or infinite number of instants. If I c is infinite then the death instant is not necessary.

A discrete-time clock c is a clock with a discrete set of instants I c . In that case, I c can be indexed by natural numbers in a fashion that respects the ordering ≺ c : we define idx c :

I c → N ⋆ (N ⋆ = N \ {0}) such that ∀i ∈ I c , idx(i) = k iff i is the k th instant in I c wrt. ≺ c
. By convention we will consider that the first instant of c is indexed by 1.

For any discrete time clock c

I c , ≺ c , c ↑ , c ↓ , ≡ c ↓ , c[k] denotes the k th instant in I c (i.e., idx c (c[k]) = k).
For any instant i ∈ I c of a discrete time clock c, °i is the unique immediate predecessor of i in I c ⊎ {c ↑ } . We assume that the predecessor of c [START_REF] Omg | UML Profile for MARTE, v1.0. Object Management Group[END_REF] is the birth c ↑ . Similarly we denote the unique immediate successor of i in I c as i°, if any.

The number of instants preceding a specific instant i of a clock c is retrieved by χ(c)@i. It only makes sense on discrete clock since it always return ∞ on dense clock. Note that the use of this function needs i to be strictly ordered on the set of instants it refers (i.e.,I c in the previous example). From the previous definition we give the following lemmas:

I, ≺, ≡ |= χ(c) ⇔ 0) (i ∈ I) ∧ (I c ∈ I) ∧ (∃j, k ∈ I c ⊎ {c ↑ }) ∧ (j ≺ k) ∧ (j ≺ i) ∧ (i ≺ k) ∧ 1) c ∈ C ∧ χ(c)@i = k ⇔ c[k] i ≺ c[k + 1] ∧ 2) c ∈ C, ∀k ∈ 1; |I c | ⇔ χ(c)@c[k] = k -1 ∧ 3) χ(c)@c ↑ = 0 ∧ 4) χ(c)@c ↓ = |I c | (1)
The reader can notice that the χ function is defined only if i is ordered with the set of instant of c (cf. equation 1.0).

Clock Constraints Specification

We have introduced the concept of clock constraints in the marte specification (chapter 9) and also a dedicated language for expressing such constraints: ccsl [START_REF] Omg | UML Profile for MARTE, v1.0. Object Management Group[END_REF]Annex C.3]. This language is non normative (the marte profile implementors are not obliged to support it). The semantics of ccsl given in the marte specification is informal. A first formal semantics, based on mathematical expressions has been proposed in a paper [START_REF] Mallet | On the semantics of UML/marte clock constraints[END_REF] and a research report [START_REF] André | Clock constraint specification language in UML/-MARTE CCSL[END_REF], which is an extended version of the paper. A precise definition of the syntax of a kernel of ccsl along with a structural operational semantics is now available [START_REF] André | Syntax and semantics of the clock constraint specification language (CCSL)[END_REF]. This semantics is the golden reference for the ccsl constraint solver implemented in TimeSquare [14]2 , the software environment that supports ccsl and the marte time profile.

Clock constraints are classified into two main categories:

1. clock relations that constrain the order of the instant of two or more existing clocks;

2. clock expressions that define a new clock from a set of parameters.

As for clocks, every relation and expression has a timelife defined by the instants of its birth and its death. We define in more details these elements in the following.

A ccsl specification S is a triple C, Expr , Rel such that C is a set of clocks, Expr is a set of clock definitions and Rel is a set of clock relations. Both Expr and Rel state constraints on the elements of C.

The models of ccsl specification are time structures. Let S = C, Expr , Rel be a ccsl specification and T = I, ≺, ≡ a time structure. Informally, T satisfies the specification S iff the following conditions holds:

• The set of instants I includes all the instants of the different clocks in C.

• The orders of the different clocks in C are preserved by ≺.

• The different constraints induced by the elements of Expr and Rel are satisfied.

The satisfaction of the different clock relations and definitions will be defined in the following sections and depends of the relations ≺ and ≡.

Definition of a specific subset of instants

Since relations and expressions are alive from their birth instant and possibly until their death instant, it is useful to define the set of instants of a clock between these two instants. An interval of clock c (i.e.,a subset of I c ) characterized by two instants α and β is denoted as I α..β c . It is defined by the following equation: The interval starts with the first instant of I c such that α precedes this instant. The interval ends at the first instant of I c which is strictly preceded by β; this instant is not in the interval. The latter constraint is expressed by ¬(β ≺ i) for all instants of I c in the interval. Note that since is a partial order, ¬(β ≺ i) is not equivalent to (i β).

I α..β c {i ∈ I c |(α i) ∧ ¬(β ≺ i)} (2) c α β c α β c ↓ c α β c ↓ (A) (B) (C)
When β is not given, the interval (denoted as I α.. a ) is defined as follows: These intervals are used in the following to represent the instants to be considered during the life of a specific relation or expression. Consequently, the set of instants of a clock c during the life of a relation r is noted I r c . Similarly the set of instants of a clock c during the life of an expression is noted I ce c where ce is the clock defined by the expression. More generally, we denote I x c the set of instants of c that is defined on an interval bounded by x ↑ and, either c ↓ or x ↓ . More formally, I x c is defined by the following equation:

I α.. c {i ∈ I c |(α i)} (3)
I x c {(∃x ↓ ∈ x ⇒ I x c = I x ↑ ..x ↓ c ) ∨ (∄x ↓ ∈ x ⇒ I x c = I x ↑ .. c )} (4)
Predicate dies_in Let dies_in be a predicate on clock × constraint such that

c dies_in (r) ⇔ (r ↑ c ↓ ) ∧ ∃r ↓ ∈ r ⇒ ¬(r ↓ ≺ c ↓ ) (5)

Clock relations

The clock relations presented in this subsection form the kernel all binary clock relations. Let a and b two clocks. Five primitive relations on clocks are defined. For each of them the definition is split into a first part named 'a)' defining the semantics of the relation and a second part 'b)' specifying the relations between deaths of clocks in the relations.

Subclocking: a r ⊂ b is a synchronous clock relation. a is said to be a sub-clock of b, and b a super-clock of a. The r represents the entity that gives the birth and the death of the relation (i.e.,the interval on which the relation applies). If r is not specified, the relation applies for the whole system life.

I, ≺, ≡ |= a r ⊂ b ⇔ (a) ∀i a ∈ I r a , ∃i b ∈ I r b , i a ≡ i b ∧ (b) b dies_in (r) ⇒ (a ↓ b ↓ ).
(i) ≺ i) ∧ ∀i, j ∈ I r b , (i ≺ j) ⇒ (h(i) ≺ h(j)) ∧ (b) (¬(b ↓ r ↑ ) ∧ a dies_in (r) ∧ h is bijective) ⇒ b dies_in (r). (7)
Equation 8-a imposes that each instant of I r b (slowest clock) is preceded by a distinct instant of I r a . Equation 8-b implies that b dies in r if a is dead and b is not late any more (and if b was not dead before entering the interval). The condition "h is bijective" is to ensure that one has the same number of a an b instants; even in the dense case.

→ I r a , ∀i ∈ I r b , (h(i) i) ∧ ∀i, j ∈ I r b , (i ≺ j) ⇒ (h(i) ≺ h(j)) ∧ (b) (¬(b ↓ r ↑ ) ∧ a dies_in (r) ∧ h is bijective) ⇒ b dies_in (r). (8)
The constraints are similar to precedence.

The reader can notice that there is no death propagation in this relation.

Equality: a r = b is a typical synchronous clock relation that means that each instant of a coincides with one instant of b. This relation holds when both a is a sub-clock of b, and b is a sub-clock of a.

I, ≺, ≡ |= a r = b ⇔ (a) ∀i ∈ I r a , ∃j ∈ I r b , i ≡ j ∧ ∀i ∈ I r b , ∃j ∈ I r a , i ≡ j ∧ (b) (a dies_in r) ∨ (b dies_in r) ⇒ (a ↓ ≡ b ↓ ). (10)
Note that 10-a expresses that a is subclock of b and vice versa. Equation 10-b states that the death of a and the death of b are coincident.

Clock expressions

A clock expression defines a new implicit clock. In order to assign this result to an explicit clock, we used clock definitions of the form c expr where expr is one of the expressions whose semantics is defined in this section. Consequently, the corresponding expression born and death respectively coincides with the born and the death of c. For all expressions, if other expressions or relations are used for their definition, their birth and their death respectively coincide with the birth and the death of c.

Index independent clock expressions

Clock union: a + b represents a clock that ticks whenever a or b ticks. This new clock is the minimal (w.r.t. ) super clock of both a and b.

I, ≺, ≡ |= c a + b ⇔ (a) ∀i a ∈ I c a , ∃i ∈ I c , (i ≡ i a )) ∧ ∀i b ∈ I c b , ∃i ∈ I c , (i ≡ i b )) (b) ∧ ∀i ∈ I c , (∃i a ∈ I c a , (i ≡ i a )) ∨ (∃i b ∈ I c b , (i ≡ i b )) (c) ∧ c ↓ max {a ↓ , b ↓ }. (11)
The function max is defined as follows: max {i, j} is equal to i if j i, to j if i ≺ j. If i and j are idependent both solution are valid. The function min is defined similarly.

Equation 11-a states that both a and b are subclocks of c and 11-b that every instants of c coincides either with a or b (minimal subclcok). Equation 11-c expresses that c dies iff both a and b are dead. The death of c coicindes with the death of the last clock. Note that a consequence of this definition is that in any time structure satisfying c a + b, the clocks a and b are totally ordered since the instants of c are.

Clock intersection: a * b defines a clock that ticks whenever both a or b tick.

I, ≺, ≡ |= c a * b ⇔ (a) ∀i ∈ I c , ∃i a ∈ I c a , ∃i b ∈ I c b , (i ≡ i a ) ∧ (i ≡ i b ) (b) ∀i a ∈ I c a , ∀i b ∈ I c b , (i a ≡ i b ) ⇒ (∃i ∈ I c , (i ≡ i a ) (c) ∧ c ↓ min {a ↓ , b ↓ }. ( 12
)
Equation 12-a state that c is a sub-clock of both a and b. Equation 12-b makes c maximal with respect to the subclocking relation. Equation 12-c states that c must die as soon as either a or b dies.

Figure 6 illustrates the two clock expressions just defined. note that in this case the death of c coincides with the death of a clock in the parameters but nothing prevents something else (i.e.,another constraint) to kill the clock before.

Index dependent clock expressions

Sup: a ∨ b defines a clock that is the fastest among all the clocks slower than a and b (equation 13). In other terms, the resulting clock always coincides with the slowest clock among a and b, in an opportunistic manner.

Let T = I, ≺, ≡ and T ′ = I ′ , ≺ ′ , ≡ ′ be two time structures. In the equation below, T ⊆ T ′ means that I ⊆ I ′ and the relations ≺ ′ and ≡ ′ respectively extend ≺ and ≡. Also, we note d ∈ T for a clock d iff I includes the instants of d and ≺ respects their ordering.

T |= c a ∨ b ⇔ (a) T |= a c ∧ T |= b c (b) ∧ ∀T ′ st. T ⊆ T ′ , ∀d ∈ T ′ , (T ′ |= a d) ∧ T ′ |= b d) ⇒ T ′ |= c ≺ d. (c) ∧|I c | = min(|I c a |, |I c b |) ∧ (|I c | = |I c a | ∧ a dies_in c) ⇒ c ↓ max (c[|I c a |], a ↓ ) ∨(|I c | = |I c b | ∧ b dies_in c) ⇒ c ↓ max (c[|I c b |], b ↓ ) (13)
T |= c a ∧ b ⇔ (a) T |= c a ∧ T |= c b (b) ∧ ∀T ′ st. T ⊆ T ′ , ∀d ∈ T ′ , (T ′ |= d a) ∧ (T ′ |= d b) ⇒ T ′ |= d ≺ c. (c) ∧ c ↓ max {a ↓ , b ↓ }. ( 14
)
The different parts of this equation are similar to the previous case but the death propagation where it is not necessary to delay the death depending on the clock c was following.

Figure 7 shows the sup and inf of two clocks. Strict sampling: a ⇓ b is a mixed clock expression (i.e.,based on both precedence and coincidence). It defines a subclock of b that ticks whenever clock a has ticked at least once since the previous tick of b. For this expression to make sense, b must be a discrete clock.

Figure 8 shows the corresponding instant ordering.

I, ≺, ≡ |= c a ⇓ b ⇔ (a) ∀i ∈ I c , ∃i a ∈ I c a , i b ∈ I c b , (°i ≺ i a ) ∧ (i a ≺ i) ∧ (i ≡ i b ) (b) ∧ c ↓ min {b ↓ , i b st. i b ∈ I c b ∧ (°i b ≺ a ↓ ) ∧ (a ↓ ≺ i b )}. ( 15
)
Equation 15-a says that c is a subclock of b and that there is always an occurrence of a between two occurrences of c (cf. Figure 8).

Non strict sampling: a b is also a mixed clock expression, similar to the previous one, just changing the precedence relations to non-strict ones. The clock b still must be a discrete clock. Figure 9 shows the corresponding instant ordering.

I, ≺, ≡ |= c a b ⇔ (a) ∀i ∈ I c , ∃i a ∈ I c a , i b ∈ I c b , (°i b ≺ i a ) ∧ (i a i b ) ∧ (i ≡ i b ) (b) ∧ c ↓ min {b ↓ , i b st. i b ∈ I c b ∧ (°i b ≺ a ↓ ) ∧ (a ↓ i b )}. ( 16
)
Figure 10 As of this tick, the resulting clock dies. To make sence, we require that b is a discrete clock. (For a sake of simplicity χ(a)@c ↑ = 0 and χ(b)@c ↑ = 0) ce clock, is defined on page 15.

I, ≺, ≡ |= c a b ⇔ (a) ∀i ∈ I c , ∃i a ∈ I c a , (i ≡ i a ) (b) ∧ ∀i a ∈ I c a , (∀i b ∈ I c b , ¬(i b i a )) ⇒ (∃i ∈ I c , (i ≡ i a ) (c) c ↓ min {a ↓ , i b st. i b ∈ I c b ∧ ∀j b ∈ I c b , (i b j b )}. (17

Clock expressions with non-clock parameters

In the previous expressions, all the parameters were clock. We consider here expressions with other kind of parameter type, for instance Integer or IntegerWords (see Annex B). In the following expressions non-clock parameters have the meaning of a schedule that are used to create a list of events or tasks and the times at which each one should happen or be done. More precisely, the schedule associated with an expression contains the future times at which the resulting clock should tick in coincidence with a parameter clock. evaluated

Awaiting: a ˆn, where n ∈ N ⋆ , is a synchronous clock expression. This expression waits for the n th strictly future tick of a. On this occurrence, the resulting clock ticks and dies. As one have to count the occurrences of a, the clock must be discrete. Defer: a (w) b is also a mixed clock expression that deals with multiple future scheduled ticks.

I, ≺, ≡ |= c aˆn ⇔ (a) (∃i a ∈ I c a , idx (i a ) = n) ⇒ (I c = {i c } ∧ (i c ≡ a[n]) ∧ c ↓ ≡ a[n]) (b) ∧ ( ∃i a ∈ I c a , idx (i a ) = n) ⇒ (I c = {} ∧ c ↓ a ↓ ) (18)
w is an IntegerWord defined, coinjointly with notations over w,in the annex B. Defer is a complex expression. A simplist explanation is to consider that each ticks of the clock a specifies that a ticks of the resulting clock will coincides after n ticks of b; where n is taken in w (cf. 19-a below).

For this expression to make sense, a and b must be discrete.

I, ≺, ≡ |= c a (w) b ⇔ (a) ∃h : I c → I b , ∀i ∈ I c , (i ≡ h(i)) ∧ ∀i a ∈ I a , ∃i c ∈ I c ∃X ⊆ I b , (|X| = w(idx (i a ) -1)) ∧ ∀i b ∈ I b , (i b ∈ X ⇔ i a ≺ i b i c ) (b) c ↓ ≡ min {b ↓ , c[min{|w|, |I a |}]}. (19)
Equation 19-b means that the death of c coincindes with the first of the following instant:

• the death of b (since c is subclock of b),

• the |w| th instant of c when w is finite (since there is no future scheduled occurence of c),

• the |I a | th of c (since no future scheduled occurence of c can be selected afterward).

Figure 13 shows clock expression 'defer' when n is a constant. In this case, the clock expression is also known as clock expression 'delayedFor'.

Clock expression concatenation

Will be defined in a future version

Conclusion

We presented in this document the denotational semantics of the ccsl language. Compared to older document, this report introduce an explicit notion of birth and death in the definition of a time system. The birth and death notions are implemented in TimeSquare [START_REF] Deantoni | TimeSquare: Treat your Models with Logical Time[END_REF] and used in the definition of the MoCCML operational semantics [START_REF] Deantoni | Operational Semantics of the Model of Concurrency and Communication Language[END_REF].

A Mathematical notions and notations

A.1 Binary relations

A binary relation R over X and Y is a subset of X × Y : R ⊂ X × Y (20)
X is called the domain of R; Y its codomain.

A.1.1 Relations over a set

If X = Y , R ⊂ X 2 is a binary relation over X (or endorelation over X). Some important classes of binary relations over X are:

R is reflexive :⇔ ∀x ∈ X, x R x (21) R is irreflexive :⇔ ∀x ∈ X, x R x (22) R is symmetric :⇔ ∀x, y ∈ X, x R y ⇒ y R x (23) R is antisymmetric :⇔ ∀x, y ∈ X, (x R y) ∧ (y R x) ⇒ x = y (24) R is asymmetric :⇔ ∀x, y ∈ X, (x R y) ⇒ ¬(y R x) (25) R is transitive :⇔ ∀x, y, z ∈ X, (x R y) ∧ (y R z) ⇒ (x R z) (26) R is total :⇔ ∀x, y ∈ X, (x R y) ∨ (y R x) (27)
R is an equivalence relation over X :⇔ R is reflexive, symmetric, and transitive (28)

R is a partial order relation over X :⇔ R is reflexive, antisymmetric, and transitive (29) R is a total order relation over X :⇔ R is a partial order which is total (30)

A total order is also known as a Linear order.

A.1.4 Strict partial order

In his paper entitled "Concurrency theory" [START_REF] Adam | Concurrency theory[END_REF] Petri defines a strict partial order.

A strict partial order: SPO(X, <) is defined as:

SPO(X, <) :⇔ 1) ∀x, y, (x < y) ⇒ (x ∈ X) ∧ (y ∈ X) ∧ 2) ∀x ∈ X, ¬(x < x) ∧ 3) ∀x, y, z ∈ X, (x < y) ∧ (y < z) ⇒ (x < z) (45)
in words < is an irreflexive, transitive relation in X; in shorthhand:

SPO(X, <) :⇔ 1) < ⊆ X × X ∧ 2) < ∩ Id = ∅ ∧ 3) < 2 ⊆ < (46)
In any strict partial order, we can define the disorder relation "neither x < y nor y < x".

x co y ⇔ (x, y ∈ X) ∧ ¬(x < y) ∧ ¬(y < x)

or for short co := < ∪ > It follows that co is (totally) reflexive and symmetric: Id ⊆ co and co = co -1 . A structure (X, co) with these properties is called a similarity.

We now assert that, in general, co is not transitive: co 2co = ∅.

Remark: a transitive similarity is an equivalence relation.

A.2 Functions

Functions are a special class of binary relations that are left-total and functional (Eq. 44).

Let A and B be sets.

A function from X to Y, denoted f : X → Y , is a relation from X to Y such that ∀x ∈ X, ∃!y ∈ Y, (x, y) ∈ f (48)
If (x, y) ∈ f , then we write f (x) = y.

Let f be a function from X to Y and let X ′ be a subset of X f (X ′ ) denotes a subset of Y , called the image of X ′ under f , such that

f (X ′ ) = {f (x) | x ∈ X ′ } (49)

A.2.1 Special classes of functions

Let f be a function f : X → Y .

f is surjective (onto) if f (X) = Y (50) f is injective (one-to-one) if ∀x, x ′ ∈ X, x = x ′ ⇒ f (x) = f (x ′ ) (51)
f is bijective (one-to-one and onto) if f is both surjective and injective (52)

A.3 Time related concepts

• The restriction of ≺ c on I c is a strict order relation.

• All instants of I c are strictly ordered (≺ c is total): ∀i, j ∈ I c , (i = j) ⇒ (i ≺ c j) or (j ≺ c i).

• The birth strictly precedes all the other instants of the clock:

∀i ∈ I c ⊎ {c ↓ }, c ↑ ≺ c i.
• Every instants precedes the death but the last one that may coincide with it:

∀i ∈ I c ⊎ {c ↑ }, ((i ≺ c c ↓ ) ∨ (i ≡ c ↓ c ↓ ))
.

A.3.2 Sets of instants

Let C be the set of clocks.

• Set of (actual) instants:

I = c∈C I c (54)
• Extended set of instants (includes virtual ones):

I + = I c ⊎ {c ↑ , c ↓ } (55)
where c ↓ is a virtual instant, greatest element of I + (i.e.,∀i ∈ I + , i c ↓ ). c ↓ stands for the (virtual) death instant of clocks c.

A.3.3 Relations on instants

Let ≺ (precedence) and ≡ (coincidence) be two binary relations over I + .

Precedence is a strict partial order over I + i.e., ∀x, y, z ∈ I+ : ¬(x ≺ x) (irreflexivity),

x ≺ y ⇒ ¬(y ≺ x) (asymmetry), and

x ≺ y ∧ y ≺ z ⇒ x ≺ z (transitivity) (56)

Inria

Coincidence is an equivalence relation over I + i.e., ∀x, y, z ∈ I+ :

(x ≡ x) (reflexivity),

x ≡ y ⇒ (y ≡ x) (symmetry), and

x ≡ y ∧ y ≡ z ⇒ x ≡ z (transitivity) (57)
From these relations we derive three new relations over I + :

Causality ≺ ∪ ≡ (58) Exclusion # ≺ ∪ ≺ -1 (59) Independence ∪ -1 (60)
The graphical representation of instant relations is given in

A.3.4 Intervals

Let α and β two instants of I + , and c a clock. We define special subsets of I c :

I α..β c {i ∈ I c |(α i) ∧ ¬(β i) ∧ ∃c † , ¬(β c † ) ⇒ (i c † ) } (62)
When β is not given, the interval (denoted as I α.. a ) is defined as follows:

I α.. c {i ∈ I c |(α i) ∧ ∃c † ⇒ (i c † ) } (

RR n°8628

Note that because the coincidence relation is not the identity relation, the supremum is not necessarily unique: all the instants of a coincidence set can meet the above conditions. A similar definition holds for I α.. c . I α..β c always exists thanks to the assumed existence of a greatest element ( †) in I + .

Fig 14 shows different cases. In the discrete time case, the supremum of a non empty interval is the last instant of the interval. In the dense time cas, the supremum is the first instant of the next interval (i.e.,an instant not in the interval). When the interval is shortened by a death, then the (virtual) death instant is the supremum of the interval. Of course, the instant may coincide with an instant of the interval.

= i • v | j • v (65)
Inria u is called the prefix of w, v is the period of w, and (v) ω = lim n v n denotes the infinite repetition of v. ε is the empty word. In order to avoid confusion between parentheses denoting periodic words and usual parentheses, the former are colored red. The associated ω symbol is also red.

A periodic word with an empty prefix is called a strictly periodic word (w = (v) ω ).

A periodic word has infinitely many representations:

Let b ∈ N ⋆ , u, v ∈ (N ⋆ ) * , u • b (v • b) ω = u (b • v) ω (

Figure 1 :

 1 Figure 1: Clock interval definitions

Fig. 2

 2 Fig. 2 illustrates various cases: without the clock death (Fig. 1.A) or with the clock death (Fig. 1.B and C).

Figure 2 :

 2 Figure 2: Clock interval when only α is given

Figure 3 :

 3 Figure 3: Example of subclocking.(For a sake of simplicity χ(a)@r ↑ = 0 and χ(b)@r ↑ = 0)

Figure 4 :

 4 Figure 4: Exemple of precedence.(For a sake of simplicity χ(a)@r ↑ = 0 and χ(b)@r ↑ = 0)

4 Figure 5 :

 45 Figure 5: Example of causality relation.(For a sake of simplicity χ(a)@r ↑ = 0 and χ(b)@r ↑ = 0)

Figure 6 :

 6 Figure 6: Exemples of clock expressions union and intersection.

Equation 13 -

 13 b means that a and b are faster than c. Equation 13-b states that there is no extension of T including a clock d being slower that a and be b and fsater than c. We need to introduce extensions of T to ensure that d can have distinct elements from the other clocks. Finally, 13-c express that c dies with the same number of ticks than the clock with the minimum number of ticks. Death of c occurs either at the death of this clock if c was following it or when it has the same number of ticks in the other case. Note that the death propagation makes sense only if a and b are discrete clocks.Inf: a ∧ b defines a clock that is the slowest among all the clocks faster than a and b (equation 14). The resulting clock always coincides with the fastest clock among a and b, in an Inria opportunistic manner.

Figure 7 :

 7 Figure 7: Exemples of clock expressions sup and inf.

Figure 8 :

 8 Figure 8: Strict sampling instant ordering.

Figure 9 :

 9 Figure 9: Non strict sampling instant ordering.

Figure 10 :Inria 2 . 7 . 3

 10273 Figure 10 highlights the different behaviors of the strict and non strict clock expression samplings.

)Figure 11 :

 11 Figure 11: Exemples of clock expression upto.(For a sake of simplicity χ(a)@c ↑ = 0 and χ(b)@c ↑ = 0)

  Equation 18-a defines the case where a[n] exists: in that case I c is a singleton whose element coincides with a[n], and the death of c also coincides with a[n]. If a[n] does not exist (18-b), I c is empty and c dies with a.figure12).

Figure 12 :

 12 Figure 12: Exemple of clock awaiting.(For a sake of simplicity χ(a)@c ↑ = 0)

Figure 13 :

 13 Figure 13: Exemple of clock expression 'defer'.

Inria

A. 3 . 1

 31 Clocks A clock c is a 5-tuple I c , ≺ c , c ↑ , c ↓ , ≡ c ↓ where I c is a possibly infinite set of instants, ≺ c is an order relation on I c ⊎ {c ↑ , c ↓ } c ↑ ∈ I c is the birth instant of c, and c ↓ ∈ I c is the death instant of c ≡ c ↓ is a coincidence relation satisfying the following conditions:

∧ 2 )

 2 63) Note that elements of I α..β c and I α.. c are all actual instants (i.e.,members of I). s is an upper bound for I α..β c i.e., ∀i ∈ I α..β c , i s ∧ 3) s is a least upper bound for I α..β c i.e., ∀s ′ upper bound of I α..β c , s s ′

Figure 14 :

 14 Figure 14: Supremum in different cases

66 )Notation B. 1 ( 1 2 . 2 2 . 5 2 . 6 2 . 7 3 17 A

 661122252627317 Length of a word). |w| denotes the length of the word w. Notation B.2. |w| b denotes the number of integers set to b ∈ N ⋆ in the word w. Notation B.3. w [k] denotes the k th integer of the word w. Notation B.4. w[k..l] denotes the (sub) word from w starting at the k th integer upto the l th integer included. Notation B.5. w[k..] denotes the (sub) word from w starting at the k th integer. Possibly infinite.Let k ∈ N ⋆ , b ∈ B, w a word w ↓ 0 0 b • w ↓ k = b + (w ↓ (k -1))Multiform logical time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Instants and Time Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Clocks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Clock Constraints Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Definition of a specific subset of instants . . . . . . . . . . . . . . . . . . . . . . . 7 Clock relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Clock expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Conclusion Mathematical notions and notations 19 A.1 Binary relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 A.2 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.3 Time related concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 B Integer Words 24 B.1 Finite/infinite words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Inria RESEARCH CENTRE SOPHIA ANTIPOLIS -MÉDITERRANÉE 2004 route des Lucioles -BP 93 06902 Sophia Antipolis Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr

Table 2

 2

	.

Table 2 :

 2 Instant relations

	Remark
	∀c ∈ C, ≺

c =≺ ∩ (I c × I c )

RR n°8628

Classical properties of binary relations are recalled in Appendix A.1. Inria

http:timesquare.inria.fr Inria

Inria

A.1.2 Operations on Binary Relations

If R is a binary relation over X and Y , then the following is a binary relation over Y and X: R -1 the converse of relation R over X and Y is such that R

If R is a binary relation over X, then each of the following relations is a binary relation over X: R = the reflexive closure of relation R over X is defined as

If R and S are binary relations over X and Y , then each of the following relations is a binary relation over Y and X:

If R is a binary relation over X and Y , and S a binary relation over Y and Z, then the following relation is a binary relation over X and Z: R • S ⊆ X × Z (composition) is defined as

A.1.3 Other types of Binary Relations

If R and S are binary relations over X and Y :

R is one-to-one :⇔ R is both injective and functional (39)

R is a correspondence :⇔ R is both left-total and surjective (42)

R is a function :⇔ R is both left-total and functional (43)

R is a bijection :⇔ R is a one-to-one correspondence (44) Inria