Kiraku Minami
email: kminami@kurims.kyoto-u.ac.jp

Trace Equivalence and Epistemic Logic to Express Security Properties ⋆

Keywords: Applied pi calculus, Trace equivalence, Epistemic logic

In process algebra, we can express security properties using an equivalence on processes. However, it is not clear which equivalence is the most suitable for the purpose. Indeed, several definitions of some properties are proposed. For example, the definition of privacy is not unique. This situation means that we are not certain how to express an intuitive security notion. Namely, there is a gap between an intuitive security notion and the formulation. Proper formalization is essential for verification, and our purpose is to bridge this gap. In the case of the applied pi calculus, an outputted message is not explicitly expressed. This feature suggests that trace equivalence appropriately expresses indistinguishability for attackers in the applied pi calculus. By chasing interchanging bound names and scope extrusions, we prove that trace equivalence is a congruence. Therefore, a security property expressed using trace equivalence is preserved by application of contexts. Moreover, we construct an epistemic logic for the applied pi calculus. We show that its logical equivalence agrees with trace equivalence. It means that trace equivalence is suitable in the presence of a non-adaptive attacker. Besides, we define several security properties to use our epistemic logic.

Introduction

Background

In modern society, information technology is indispensable to our daily lives, and many communication protocols are developed to transmit data securely. Verification of security properties of each protocol is essential, but it is not easy.

In the first place, how to formalize security notions is not clear. Various definitions of the same security property have been proposed, we will show an example later. One of our goals is to provide foundations to express these properties in a rigorous way. Besides, how to model communication and concurrency is also not clear; many such models have also been developed. In this work, we focus on process algebra because it allows us to handle parallel composition naturally.

In process calculi, common confidentiality properties such as secrecy are represented to use an equivalence on processes. Many equivalences exist (cf. [START_REF] Van Glabbeek | The linear time -branching time spectrum[END_REF]), but which is the most suitable for expressing confidentiality is not clear. For instance, Delaune et al. [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF] defined privacy in electronic voting in terms of the applied pi calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] as follows.

Definition 1 ( [13, Definition 9]). A voting protocol respects vote-privacy (or just privacy) if

S[V A { a /v}|V B { b /v}] ≈ l S[V A { b /v}|V B { a /v}]
for all possible votes a and b.

V A and V B denote the voters containing the free variable v. S is an evaluation context. S denotes other voters and authorities. Intuitively, when the protocol respects privacy, this definition states that an attacker cannot distinguish two situations where votes are swapped. Note that indistinguishability is expressed to use labeled bisimilarity ≈ l in this definition. Is it the most suitable? This question is nontrivial. Indeed, Chadha et al. [START_REF] Chadha | Epistemic logic for the applied pi calculus[END_REF] gave another definition and claimed that trace equivalence is more suitable than bisimilarity to model privacy. We also claim that trace equivalence is more suitable to express security properties in the presence of non-adaptive attackers. Similar arguments are not abundant in previous work.

In the applied pi calculus, a process can send not only names but also terms, but we do not explicitly express sent messages. We indirectly represent them to use alias variables. This feature enables us to handle cryptographic protocols naturally and suggests that trace equivalence means indistinguishability for attackers. This is because attackers whom we consider can observe only labeled transitions. We recall the syntax and semantics of the applied pi calculus in §2.

Both bisimilarity and trace equivalence on labeled transition systems (LTSs) are well studied. However, trace equivalence in the applied pi calculus (and other variants of the pi calculus [START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Milner | A calculus of mobile processes[END_REF]) has not drawn much attention. This is perhaps because trace equivalence is the coarsest among commonly used equivalences. However, security properties sometimes require that different processes are regarded as the same. For example, consider secrecy. We want to make two processes that send different messages indistinguishable. In the case, trace equivalence is enough, but bisimilarity is not always optimal because it is too strong. Bisimilarity requires that possible actions for each process are the same. However, a non-adaptive attacker cannot detect a difference in feasibility. Here, "non-adaptive" means that the attacker cannot control participants. Thereby, a fine equivalence such as bisimilarity is not always adequate. Bisimilarity is probably suitable for more powerful attackers.

Epistemic logic is often used to express confidentiality directly (e.g. [START_REF] Chadha | Epistemic logic for the applied pi calculus[END_REF][START_REF] Mano | Role interchange for anonymity and privacy of voting[END_REF][START_REF] Tsukada | On compositional reasoning about anonymity and privacy in epistemic logic[END_REF]). For example, when a message M sent by an agent a is anonymous, we might say that an adversary cannot know who sent M . In epistemic logic, we can express it with a formula such as ¬KSend(a, M ). This logical formulation is close to our intuition. Nevertheless, research into an epistemic logic for the applied pi calculus is not abundant.

In this paper, we assume that attackers can observe only labeled transitions. Especially, they cannot observe what action participants' can do. This assumption is natural because attackers in this paper are non-adaptive. We also assume that an attacker can send messages to participants.

Contributions

We prove that trace equivalence for the applied pi calculus is a congruence in §3. Second, we give an epistemic logic that characterizes trace equivalence in §4. Besides, we define security properties such as role-interchangeability, secrecy [START_REF] Mano | Role interchange for anonymity and privacy of voting[END_REF][START_REF] Tsukada | On compositional reasoning about anonymity and privacy in epistemic logic[END_REF], and openness, using our epistemic logic. Moreover, we show that parallel composition does not generally preserve secrecy and openness. Whereas, trace equivalence characterizes total secrecy, so application of contexts preserves it. We omit many proofs. See [START_REF] Minami | Trace equivalence and epistemic logic to express security properties[END_REF] for details.

Our results suggest that trace equivalence is more suitable to express (nonprobabilistic) security notions than bisimilarity.

The Applied Pi Calculus

The applied pi calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] is an extension of the pi-calculus [START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Milner | A calculus of mobile processes[END_REF]. We can handle cryptographic protocols naturally to use it.

Syntax

Let Σ be a signature equipped with an equational theory. Terms are made from names, variables, and function symbols. A term is ground when it contains no variables. We recall the syntax of the applied pi-calculus. Here, M, N... range over terms, while n on names and x on variables.

P, Q

::= 0 | M ⟨N ⟩.P | M (x).P | νn.P | if M = N then P else Q | P + Q | P |Q | !P A, B ::= P | νn.A | νx.A | A|B | { M /x} P, Q, .
.. are plain processes. ν is a binding operator. | is a parallel composition operator. + is a nondeterministic choice operator. Plain processes are similar to pi-calculus processes, but they are not the same. A pi-calculus process can send only a name. On the other hand, an applied pi calculus process can send a term. Besides, a channel consists of a term. An object of an input prefix is a variable, so names do not change while the process runs.

A, B, ... are extended processes. We call { M /x} an active substitution. This notion is peculiar to the applied pi calculus. An active substitution { M /x} sub- stitutes M for x in a neighbor process. fn(A) and bn(A) denote the sets of free names and bound names of a process A, respectively. fv and bv are similar to them. If fn(A)∩bn(A) = ∅ and no bound names are restricted twice, we say that A is name-distinct. Variable-distinctness is defined similarly. n(M ) denotes the set of names that appear in a term M . v(M ) is similar to it.

The domain dom(A) of an extended process A is inductively defined below. If variables in neighbor concurrently running processes are in dom(A), the process A affects those variables. If fv(A) = dom(A), we say that A is closed.

dom(P ) = ∅, dom(νn.A) = dom(A), dom(νx.A) = dom(A) \ {x}, dom(A|B) = dom(A) ∪ dom(B), dom({ M /x}) = {x}

Semantics

A context is an expression containing one hole. An evaluation context is a context whose hole is neither under a replication, a conditional branch, nor an action prefix. Structural equivalence ≡ is the smallest equivalence relation on extended processes that is closed under application of evaluation contexts and α-conversion, such that:

A|0 ≡ A (A|B)|C ≡ A|(B|C) A|B ≡ B|A (νu.A)|B ≡ νu.(A|B) if u / ∈ fn(B) ∪ fv(B) νu.νv.A ≡ νv.νu.A !P ≡ P |!P P + Q ≡ Q + P νx.{ M /x} ≡ 0 A|{ M /x} ≡ A[ M /x]|{ M /x} { M /x} ≡ { N /x} if Σ ⊢ M = N
The second from the last represents how an active substitution { M /x} acts.

Definition 2. Internal reduction → is the smallest relation on extended processes closed under structural equivalence and application of evaluation contexts, such that:

if M = N then P else Q → P when Σ ⊢ M = N if M = N then P else Q → Q when Σ ̸ ⊢ M = N P + Q → P M ⟨N ⟩.P | M (x).Q → P | Q[ N /x],
where terms M and N in the second rule are ground.

The last line represents synchronous communication on a channel M . We emphasize that an environment cannot observe what is interchanged.

Next, we recall labeled semantics and requisite equivalence relations.

M (x).P

M (N )

-→ P [ N /x] x / ∈ fv(M ⟨N ⟩.P ) M ⟨N ⟩.P νx.M ⟨x⟩ -→ P |{ N /x} A α -→ A ′ u does not appear in α. νu.A α -→ νu.A ′ A α -→ A ′ bv(α) ∩ fv(B) = ∅ A|B α -→ A ′ |B A ≡ A ′ A ′ α -→ B ′ B ′ ≡ B A α -→ B
The second rule represents an output. Note that an active substitution { N /x} is generated. The term N does not appear in the action label νx.M ⟨x⟩.

A frame is an extended process generated from 0 and active substitutions to use restriction and parallel composition. fr(A) denotes a process obtained by replacing plain processes in A with 0, and we call it a frame of A. We can consider that fr(A) is a list of outputted messages.

µ is an action. We define =⇒ as the transitive reflexive closure of -→, and

α =⇒ as =⇒ α -→=⇒.
µ =⇒ is the former when µ is silent and is the latter otherwise.

Definition 3. (M = N )φ def ⇔ v(M ) ∪ v(N ) ⊆ dom(φ)
and M σ = N σ where φ ≡ ν n.σ and n ∩ n(M, N ) = ∅ for some names n and active substitutions σ.

(M = N )φ means that an attacker cannot distinguish M and N to use φ.

Definition 4. The static equivalence on closed frames is given by

φ ≈ s ψ def ⇔ dom(φ) = dom(ψ) and ∀M, N ; (M = N )φ ⇔ (M = N )ψ
for closed frames φ and ψ. The static equivalence on closed processes is given by

A ≈ s B def ⇔ fr(A) ≈ s fr(B)
for closed processes A and B.

Static equivalence means that an attacker has the same information about which terms are equal.

Definition 5. A trace tr is a finite derivation tr

= A 0 µ1 =⇒ ... µn =⇒ A n such that every A i is closed and fv(µ i ) ⊆ dom(A i-1
) for all i. If A n can perform no actions, the trace tr is said to be complete or maximal. Given a trace tr, let tr[i] be its i-th process A i , and tr[i, j] be the trace A i µi+1 =⇒ ... ⇔ n = m and µ i = µ ′ i and A i ≈ s B i f or all i. An attacker cannot distinguish statically equivalent traces. tr(A) is a set of traces of A. tr max (A) is a set of maximal traces of A.

Definition 7.

Let A and B be closed processes.

A ⊆ t B def ⇔ ∀tr ∈ tr(A) ∃tr ′ ∈ tr(B) s.t. tr ∼ t tr ′ , A ≈ t B def ⇔ A ⊆ t B and B ⊆ t A.
Let A and B be two processes. Let σ be a map that maps variables in (fv(A) \ dom(A)) ∪ (fv(B) \ dom(B)) to ground terms. When Aσ ≈ t Bσ holds for every such σ, we also denote it as A ≈ t B.

A ⊆ t B means that each trace of A is imitated by some trace of B. We later show that non-adaptive active attackers cannot distinguish trace equivalent processes.

Trace equivalence is undecidable. However, if processes contain no replications and the equational theory on Σ is a subterm convergent destructor rewriting system, trace equivalence is coNEXP complete [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols theory and practice[END_REF].

Congruency of Trace Equivalence

The theorem below is our main result. It holds that trace equivalence is a congruence even though trace equivalence for the pi-calculus is not a congruence. This is ascribed to the difference between the pi-calculus and the applied pi calculus, namely, to the fact that names and variables are distinguished in the applied pi calculus. This is why adding an input prefix does not break trace equivalence. Besides, a scheme of late instantiation for an input transition is used in pi-calculus [START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Milner | A calculus of mobile processes[END_REF], so parallel composition may break trace equivalence. On the other hand, a scheme of early instantiation is used in the applied pi calculus. This scheme enables us to decompose a trace of a parallel composed process into traces of component processes.

Example 1. We consider pi-calculus. We put

P = z(z ′ )|yy ′ .ww ′ , Q = z(z ′ ).yy ′ .ww ′ + yy ′ .z(z ′ ).ww ′ + yy ′ .ww ′ .z(z ′ ).
Then, x(z).P and x(z).Q are trace equivalent, but xy|x(z).P and xy|x(z).Q are not trace equivalent. On the other hand, x(z).P and x(z).Q are not trace equivalent in the applied pi calculus because instantiation is early.

Abadi et al. [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] defined partial normal forms to prove that labeled bisimilarity is closed by application of closing evaluation contexts. They gave an operational semantics on partial normal forms. They classified transitions between ordinal processes into six cases to use partial normal forms.

To prove the next theorem, we use partial normal forms and define concurrent normal forms of traces. Transitions in a concurrent normal trace have to be particular forms.

Abadi et al. [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] studied decomposition and composition of reductions on partial normal forms. We study decomposition and composition of concurrent normal traces.

Theorem 1. ≈ t is a congruence.

The proof is very long and complicated, so we only present an outline of our proof for the proposition below. Other cases are easy. The proof is given in [START_REF] Minami | Trace equivalence and epistemic logic to express security properties[END_REF].

Proposition 1. A ≈ t B ⇒ A|C ≈ t B|C.
Proof outline. First, we define concurrent normal forms. A concurrent normal form is a particular form of a trace of a parallel composed process. A concurrent normal trace captures changes of scopes of bound names. Each process in a concurrent normal trace is of the form ν r s.(ν x.(σ|P )ρ | ν y.(ρ|Q)σ), where σ and ρ are (active) substitutions. Terms sent by the left process are accumulated in σ. Bound names sent by the left process P are accumulated in s. Symmetric cases are similar.

Second, for any trace t of A|C, we prove that there exists a concurrent normal trace t ′ of A|C such that t ∼ t t ′ .

Third, given a concurrent normal trace tr of A|C, we prove that we can construct traces of A and C which each process in them is of the form ν s.(σ|P )ρ or ν r.(ρ|Q)σ.

Finally, we take a trace tr ′ of B which is statically equivalent to the extracted trace of A as the above, combine it with tr ′ , and prove that the result is statically equivalent to the given trace tr.

-→ νn.((νm.a(x).x⟨m⟩)[ n /z] | n(y).b⟨y⟩ | { n /z}) a(z) -→νn.((νm.z⟨m⟩)[ n /z] | n(y).b⟨y⟩ | { n /z}) -→νnm.((νv.{ m /v})[ n /z] | (b⟨v⟩ | { n /z})[ m /v]) νw.b⟨w⟩ -→ νnm.((νv.{ m /v})[ n /z, v /w] | { n /z, v /w}[ m /v])
Next, we decompose it into traces of component processes.

-→ νn.((νm.a(x).x⟨h(m)⟩)[ n /z] | n(y).b⟨y⟩ | { n /z}) a(z) -→νn.((νm.z⟨h(m)⟩)[ n /z] | n(y).b⟨y⟩ | { n /z}) -→νnm.((νv.{ h(m) /v})[ n /z] | (b⟨v⟩ | { n /z})[ h(m) /v]) νw.b⟨w⟩ -→ νnm.((νv.{ h(m) /v})[ n /z, v /w] | { n /z, v /w}[ h(m) /v])
Cheval et al. [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF] established congruence property of trace equivalence for image-finite processes. They proved that trace equivalence is equivalent to maytesting equivalence for image-finite processes. On the other hand, taking all processes into account, may-testing equivalence does not imply trace equivalence. They gave a concrete counterexample. Thus, we cannot use the same technique.

An Epistemic Logic for the Applied Pi Calculus

Syntax

We propose an epistemic logic for the applied pi calculus. It was inspired by [START_REF] Chadha | Epistemic logic for the applied pi calculus[END_REF], but our logic is a bit different. We give syntax of formulas.

δ ::=⊤|M 1 = M 2 |M ∈ dom|δ 1 ∨ δ 2 |¬δ φ ::=δ|φ 1 ∨ φ 2 |¬φ|⟨µ⟩ -φ|F φ|Kφ
where M 1 , M 2 and M are terms, and µ is an action. We call δ a static formula and φ a modal formula. A static formula δ mentions equality of terms. A modal formula φ mentions traces.

⟨µ⟩ -φ states that the previous action is µ, and φ holds just before observing µ. F φ states that φ holds some time or other. The operator K expresses an attacker's knowledge, i.e., Kφ means an attacker knows that φ holds.

Semantics

Our logic is an LTL-like logic with an epistemic operator. Let A be a namevariable-distinct process that fv(A) \ dom(A) = x, ρ be an assignment which maps x to ground terms, tr ∈ tr(Aρ), 0 ≤ i ≤ |tr|, and M 1 and M 2 be terms. Please remember that fr(A) is a frame of A.

We suppose that δ and φ contain no variables other than x ∪ dom(tr[i]). We omit semantics of logical operators. They are defined as expected.

A, ρ, tr, i |= M 1 = M 2 iff (M 1 ρ = M 2 ρ)fr(tr[i]) A, ρ, tr, i |= M ∈ dom iff M is a variable x, and x ∈ dom(tr[i]) A, ρ, tr, i |= ⟨µ⟩ -φ iff tr[i -1] µ =⇒ tr[i] in tr and A, ρ, tr, i -1 |= φ A, ρ, tr, i |= F φ iff ∃j ≥ i s.t. A, ρ, tr, j |= φ A, ρ, tr, i |= Kφ iff ∀ρ ′ ∀tr ′ ∈ tr(Aρ ′ ); tr[0, i] ∼ t tr ′ [0, i] ⇒ A, ρ ′ , tr ′ , i |= φ
We suppose that an attacker does not know what terms are assigned to free variables before the process runs. Hence, the definition of K contains a quantifier over assignments ∀ρ ′ . Recall that an attacker can observe only labeled transitions, so accessibility is defined based on static equivalence on traces.

We also define satisfiability of formulas containing free variables. We put y = dom(tr[i]). We suppose that φ contains no variables other than x, y, and z.

A, ρ, tr, i |= φ( x, y, z) iff ∀ M ; A, ρ, tr, i |= φ( x, y, M ),
where M is a sequence of ground terms.

From now, we suppose that all processes are name-variable-distinct. We often omit restriction of a domain of definition. D(ρ) is a domain of definition of ρ.

When a formula φ is satisfied over all possible runs of a process A, we say that A satisfies φ.

A ≡ L B def ⇔ A ⊑ L B and B ⊑ L A.

Correspondence with trace equivalence

We prove that trace equivalent processes satisfy the same formulas.

Theorem 2. 1. A ≈ t B ⇒ A ⊑ L B; 2. A ⊑ L B ⇒ A ⊆ t B Proof. Let x = (fv(A) \ dom(A)) ∪ (fv(B) \ dom(B)). 1)
⊑ L B ⇒ A ⊆ t B. Theorem 3. A ≈ t B ⇔ A ≡ L B.
This theorem suggests that trace equivalence is suitable to define security properties. We give Proposition 2 as an example in the next subsection.

Applications

In this subsection, we often use abbreviations. Notably, P expresses ¬K¬, and G expresses ¬F ¬. P φ means that an attacker does not know φ does not hold. In other words, the attacker thinks that the possibility that φ holds remains.

We define minimal secrecy. We regard it as generalized minimal anonymity [START_REF] Mano | Role interchange for anonymity and privacy of voting[END_REF].

Definition 10. A variable x is minimally secret with respect to δ in

A iff A |= G(δ(x) → P (¬δ(x))).
This definition means that attackers cannot know that δ(x) holds. This property is very weak. For instance, although x is minimally secret with respect to a nontrivial formula δ, x is not always minimally secret with respect to ¬δ. Hereafter, we often omit objects.

Example 3. We put δ(z)

: z ̸ = a ∧ z ̸ = b.
We consider a process if x = a then c else d. Then x is minimally secret with respect to δ, but not secret with respect to ¬δ. Moreover, ∨ does not preserve minimally secret. However, ∧ preserves it. Although x is minimally secret in A, x is not always secret in A|A. Besides, restriction does not always preserve minimal secrecy.

Example 4. We put δ(z) : z = a. We put

P = if x = a then (a⟨s⟩ + b⟨s⟩) else a⟨s⟩, Q = if x = b then b⟨s⟩ else c⟨s⟩.
Then x is minimally secret with respect to δ in P + Q, but not secret in

(P + Q)|(P + Q).
Example 5. We put δ(z) : z = a. Then, x is minimally secret with respect to δ in x + a, but not secret in νa.(x + a). Here, we omitted objects.

We define total secrecy. We can also regard it as generalized total anonymity [START_REF] Mano | Role interchange for anonymity and privacy of voting[END_REF]. Total secrecy states attackers can obtain no information about x.

Proposition 2. x is totally secret in

A(x, y) iff A(x, y) ≈ t A(x ′ , y).

Proof. ⇒) We suppose for the sake of contradiction that A(x, y) ̸ ≈ t A(x ′ , y).

There exist M 1 , M 2 and N that are ground such that

A(M 1 , N ) ̸ ≈ t A(M 2 , N ). We suppose that A(M 1 , N ) ̸ ⊆ t A(M 2 , N ).
Then, there exists tr ∈ tr(A(M 1 , N )) such that any trace of A(M 2 , N ) is not statically equivalent to tr.

We put δ(z, z) :

z ̸ = M 2 ∨ z ̸ = N . Then A(x, y), (x → M 1 , y → N ), tr, |tr| |= Kδ(x, y).
This contradicts total secrecy. ⇐) We arbitrarily take δ, ρ, tr and i, where δ meets the demand of Definition 11 and D(ρ) = {x} ∪ y.

We suppose that A(x, y), ρ, tr, i |= δ(x, y, w).

We take M such that fr(tr

[i]) |= ¬δ(M, ρ( y), w). Let ρ ′ be ρ ′ (y) = { M (y = x) ρ(y) (otherwise).

By assumption, A(ρ(x), ρ( y)) ≈ t A(M, ρ( y)).

Hence, there exists tr ′ ∈ tr(A(M, ρ( y))) such that tr ∼ t tr ′ . Then, A(x, y), ρ ′ , tr ′ , i |= ¬δ(M, ρ( y), w). Therefore, A(x, y), ρ, tr, i |= P (¬δ(x, ρ( y), w)). Then, A(x, y) |= G(δ(x, y, w) → P (¬δ(x, ρ( y), w))).

Theorem 4. If x is totally secret in A(x, y), then x is also totally secret in E[A(x, y)] for every context E[_] which does not contain x.

Our framework can handle role interchangeability [START_REF] Mano | Role interchange for anonymity and privacy of voting[END_REF]. When x i satisfies a property δ k and x l satisfies a property δ j , an attacker thinks that it is possible that x l satisfies a property δ k and x i satisfies a property δ j . Definition 12. We put fv(A) \ dom(A) = {x 1 , ..., x p }, J = {1, ..., q}, and I = {1, ..., p}.

(x i , δ k ) is role interchangeable regarding {δ j (z j , y j )} j∈J in A iff A(x 1 , ..., x p ) |= G(δ k (x i , y k ) → ∧ l∈I ∧ j∈J (δ j (x l , y j ) → P (δ k (x l , y k ) ∧ δ j (x i , y j ))))
where y j ∩ {x 1 , ..., x p } = ∅ for all j ∈ J.

Proposition 3.

∀ M ∀i ∀tr ∈ tr(A(M 1 , ..., M p ))

∃ N ∃tr ′ ∈ tr(A(M i , N 2 , ..., N i-1 , M 1 , N i+1 , ..., N p )) s.t. tr ∼ t tr ′ ⇔ (x 1 , δ k
) is role interchangeable with respect to {δ j } in A for all {δ j } and k.

Corollary 1. ∀l ∈ I \ {i}; A(x 1 , ..., x i , ..., x l , ..., x p ) ≈ t A(x 1 , ..., x l , ..., x i , ..., x p ) ⇒ (x i , δ k ) is role interchangeable with respect to {δ j } in A for all {δ j } and k.

The converse holds only when p = 2. We give a counterexample for p = 3. Example 6. We put A(x, y, z) = if x = y then x + z else if x = z then x + y else y + z.

Then, (x, δ k ) is role interchangeable regarding {δ j } in A for all {δ j } j∈J and k, but A(a, b, a) ̸ ≈ t A(b, a, a). Thus,A(x,y,z) ̸ ≈ t A(y,x,z).

We can also consider role permutativity. Mano [START_REF] Mano | Formal Specification and Verification of Anonymity and Privacy[END_REF] showed that it is strictly stronger than role interchangeability. Role permutativity states that even if p values are swapped, an attacker cannot notice it. Definition 13. We put fv(A) \ dom(A) = {x 1 , ..., x p }, J = {1, ..., q}, and

I = {1, ..., p}. {δ j } j∈J is role permutable in A iff ∀n ≤ p ∀ψ ∈ S p ; A(x 1 , ..., x p ) |= G( ∧ k≤n δ i k (x i k , y k ) → P ( ∧ k≤n δ i k (x i ψ(k) , y k )))
where y j ∩ {x 1 , ..., x p } = ∅ for all j and each i k differs. Proposition 4. ∀ψ ∈ S p ; A(x 1 , ..., x p ) ≈ t A(x ψ(1) , ..., x ψ(p) )

⇔ {δ j } j∈J is role permutable in A for all {δ j } j∈J .

We define openness. We regard it as generalized identity [START_REF] Tsukada | On compositional reasoning about anonymity and privacy in epistemic logic[END_REF]. Parallel composition does not preserve openness.

Definition 14. x is open in

A under ∆(x) iff ∀ρ ∀tr ∈ tr max (Aρ); A, ρ, tr, |tr| |= ∆(x) → K(∆(x) → (x = xρ)).
Example 7. We put ∆(z) : z = r ∨ z = s. We put

P = if x = r then a⟨n⟩ else b⟨n⟩, Q = if x = r then b⟨n⟩ else a⟨n⟩. Then x is open in P and Q under ∆(x), but x is not open in P |Q under ∆(x).

Problem 1.

Input: An extended process A, an assignment ρ, a trace tr ∈ tr(A), an integer 0 ≤ i ≤ |tr|, and a formula φ.

Question: Does A, ρ, tr, i |= φ hold?

Proposition 5. Even if the word problem in Σ is decidable, Problem 1 can be undecidable.

Abadi and Cortier [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] proved that static equivalence can be undecidable even if the word problem in Σ is decidable. Proposition 5 follows from it.

We change semantics. We repeat the definition of satisfaction.

A |= φ iff ∀ρ ∀tr ∈ tr(Aρ); A, ρ, tr, 0 |= φ Now, we restrict ρ to be an assignment which maps free variables to only names and restrict inputted messages in tr to be only variables. That is, we assume that an attacker cannot tamper with a message. In other words, the attacker can only transfer messages without any change. Notably, the attacker cannot make a tuple of messages.

Problem 2.

Input: An extended process A and a formula φ. Question: Does A |= φ hold?

A convergent subterm theory is an equational theory defined by finite equations whose each right-hand side is a proper subterm of the left-hand side. Proposition 6. If the equational theory on Σ is a convergent subterm theory and A contains no replications, Problem 2 is decidable.

= ∧ v∈{0,1} 2(K(Bvote(v)) → Avote(v)).
Avote(v) means that Alice voted v, and Bvote(v) is similar. Minimal secrecy of a vote never holds because an attacker trivially knows votes when all votes agree. We consider protocol instances in which m voters participate and n voting options exist. Let v i be a vote of i. We consider the property below:

∨ j,k v j ̸ = v k → ∧ i ∧ v G(K(v i = v) → v 1 = v∧...∧v i-1 = v∧v i+1 = v∧...∧v m = v)
The consequence in G(...) implies that v i ̸ = v due to the antecedent condition, so we can rewrite the property.

∨ j,k v j ̸ = v k → ∧ i ∧ v G(K(v i = v) → v i ̸ = v)
Moreover, we take the contraposition in G.

∨ j,k v j ̸ = v k → ∧ i ∧ v G(v i = v → P (v i ̸ = v))
This consequence is exactly minimal secrecy. Besides, minimal secrecy of voting implies privacy, so privacy and minimal secrecy of voting agree under the disagreement condition ∨ j,k v j ̸ = v k .

It was shown that V (0, 1) ≈ t V (1, 0) implies that V respects privacy, and the partial converse was given in [START_REF] Chadha | Epistemic logic for the applied pi calculus[END_REF]. We give several properties of minimal secrecy. Proposition 7. We assume that a voting process V is equivalent for aborts, and minimal secrecy of each vote in V (v 1 , ..., v m ) holds under the disagreement condition

∨ j,k v j ̸ = v k . 1. m = 2 ⇒ V (v 1 , v 2 ) ≈ t V (v 2 , v 1 ). 2. m = 3 and n = 2 ⇒ V (v 1 , v 2 , v 3 ) ≈ t V (v 2 , v 1 , v 3 ). 3. Otherwise, V (v 1 , ..., v i , ..., v j , ..., v m ) ≈ t V (v 1 , ..., v j , ..., v i , ..., v m ) does not always hold.

Related Work

Logics about behavior of labeled transition systems originate from Hennessy-Milner logic [START_REF] Hennessy | On observing nondeterminism and concurrency[END_REF] that is a modal logic characterizing observational congruence. That is, observational equivalent systems satisfy the same modal formulas when these systems are image-finite. Process algebra is a special LTS. The spi calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] is an extension of the pi-calculus. It enables us to handle symmetric key encryption based on the Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF]. In the spi calculus, two ciphertexts obtained by encrypting two different plaintexts are indistinguishable unless an observer gets a secret key. Abadi and Gordon formalized security properties to use testing equivalence.

We focused on the applied pi calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] because it is more powerful than the spi calculus. That is, we intend to handle more various security notions. In the calculus, a process can send not only names but also terms via alias variables. Due to this feature, we can handle not only secrecy but also stricter properties. The authors proved that observational equivalence and labeled bisimilarity correspond.

Chadha et al. [START_REF] Chadha | Epistemic logic for the applied pi calculus[END_REF] already developed an epistemic logic for the applied pi calculus. They defined formulas Has and evt. Has directly represents attackers' knowledge, and evt means that a particular event had occurred. Temporal modalities were also used, but they do neither mention the just previous nor next action. The epistemic operator K was defined based on static equivalence on traces. Authors suggested that trace equivalence is more suitable than labeled bisimilarity when we consider privacy. However, a correspondent relation between logic and behavior of processes was not provided. As a matter of fact, α-equivalent processes do not always satisfy the same formulas in their framework because secret values are expressed as bound names or through events. In our framework, trace equivalent processes satisfy the same formulas.

Horne [START_REF] Horne | A bisimilarity congruence for the applied pi-calculus sufficiently coarse to verify privacy properties[END_REF] introduced quasi-open bisimilarity, and he proved that it coincides open bisimilarity. Moreover, intuitionistic modal logic FM characterizes quasiopen bisimilarity. The law of excluded middle does not hold in the logic because processes containing a free variable are also considered. Knight et al. [START_REF] Knight | Combining epistemic logic and hennessymilner logic[END_REF] defined an epistemic logic for an LTS. This framework is based on Hennessy-Milner logic, and it handles multiple agents' knowledge. They also proved weak completeness. However, compositionality was not discussed.

Process algebra is one of nominal transition systems. Parrow et al. [START_REF] Parrow | Modal Logics for Nominal Transition Systems[END_REF] developed modal logic characterizing bisimilarity for a nominal transition system.

Toninho and Caires [START_REF] Toninho | A spatial-epistemic logic for reasoning about security protocols[END_REF] proposed a dynamic spatial epistemic logic, which reasons what information a process can obtain. The epistemic operator means not only an attacker's knowledge but also a participant's knowledge, so, for example, the logic can reason a correspondence assertion.

Tsukada et al. [START_REF] Tsukada | On compositional reasoning about anonymity and privacy in epistemic logic[END_REF] studied sequential and parallel compositionality of security notions to use an epistemic logic for a multiagent system. They proved that neither anonymity nor privacy is generally preserved by composition. They also gave a sufficient condition for preservation. However, this word "parallel" merely means that the same agent acts two actions in the paper. That is, concurrency was not considered.

Fiore and Abadi [START_REF] Fiore | Computing symbolic models for verifying cryptographic protocols[END_REF] developed symbolic models of processes. They gave a procedure to decide whether an environment can derive a message M . Their technique can be used for verification. However, equivalences on processes were not studied in the paper.

Clarkson and Schneider [START_REF] Clarkson | Hyperproperties[END_REF] generalized trace properties to hyperproperties, and Clarkson et al. [START_REF] Clarkson | Temporal logics for hyperproperties[END_REF] developed hyperLTL and hyperCTL* for hyperproperties. Hyperproperties can express security properties which cannot be expressed by trace properties. The authors regarded systems as sets of traces, so hyperproperties are properties about systems. Our security properties are also proper hyperproperties. The advantage of our work over these works is to relate trace equivalence to attackers' knowledge. In [START_REF] Clarkson | Temporal logics for hyperproperties[END_REF][START_REF] Clarkson | Hyperproperties[END_REF], the relation between the equivalence and knowledge is not clear.

Goubault-Larrecq et al. [START_REF] Goubault-Larrecq | A probabilistic applied picalculus[END_REF] proposed the probabilistic applied pi calculus. In this case, Theorem 1 no longer holds. It is known that trace distribution preorder [START_REF] Segala | A compositional trace-based semantics for probabilistic automata[END_REF] is not a congruence. On the other hand, it is shown in [START_REF] Bernardo | Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes[END_REF] that probabilistic trace equivalence for nondeterministic and probabilistic LTS is a congruence with respect to parallel composition. Probabilistic trace equivalence is coarser than trace distribution equivalence.

Canetti et al. [START_REF] Canetti | Task-structured probabilistic i/o automata[END_REF] defined implementation for task-PIOAs. According to their definition, T 1 implements T 2 iff the set of behaviors of T 1 composed with E is included in the set of behaviors of T 2 composed with E for every environment E. Here, behavior is the set of trace distributions. The implementation relation is preserved by parallel composition.

Giro and D'Argenio [START_REF] Giro | On the expressive power of schedulers in distributed probabilistic systems[END_REF] pointed out that ordinary schedulers may give rise to unnatural behavior. A scheduler may leak information if it can look at the whole of the system. To solve this problem, they provided several reasonable subclasses of schedulers. The problem of the scheduler in the formalization of security properties was also pointed out in [START_REF] Alvim | Safe equivalences for security properties[END_REF][START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], which proposed other approaches.

Eisentraut et al. [START_REF] Eisentraut | Probabilistic bisimulation for realistic schedulers[END_REF] also studied subclasses of schedulers for probabilistic automata. They defined late distribution bisimulation and proved that late dis-tribution bisimulation with respect to distributed schedulers is compositional. We may need to specify subclasses of schedulers to state a probabilistic variant of Theorem 1.

Knight et al. [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] developed spatial and epistemic process calculus. Their study is for concurrent constraint programming, so their processes can add constraints. They proved that observational equivalence is a congruence. Their processes do not have labeled actions, so observational equivalence means that equivalent processes provide the same results. On the other hand, in the applied pi calculus, trace equivalent processes provide equivalent traces and indistinguishable information.

In this paper, we characterized trace equivalence in terms of our epistemic logic. That is, we showed that a non-adaptive active intruder cannot distinguish trace equivalent processes. We also focused on how composition of systems affects security properties. We proved that any composition preserves total secrecy and role permutativity. This is because trace equivalence is a congruence.

Conclusion

Summary

In this paper, we provided an epistemic logic for the applied pi calculus. This logic is an LTL-like logic, so we can describe security notions. We formulated secrecy, role-interchangeability, and openness. These are generalized security properties regarding multiagent systems.

Moreover, we associated trace equivalence with total secrecy. Application of context does not preserve minimal secrecy, but total secrecy is preserved because trace equivalence is a congruence. We also give a necessary and sufficient condition for role-interchangeability.

We conclude that trace equivalence is suitable to express non-probabilistic indistinguishability in the view of security in the presence of a non-adaptive active adversary.

Future Work

First, our epistemic logic states an adversary's knowledge. We intend to construct a logic for a process's knowledge. It will bridge a gap between multiagent systems and process calculi.

Second, formalizations of other security properties such as non-malleability are also the next topics.

Finally, what logic is suitable for security in the presence of an adaptive attacker is still open.

Definition 6 . 1 =⇒m

 61 µj =⇒ A j where 0 ≤ i ≤ j ≤ n. The length of the trace tr is denoted by |tr| = n. Let tr be a trace A 0 µ1 =⇒ ... µn =⇒ A n and tr ′ be a trace B 0 µ ′ =⇒ B m . Static equivalence between tr and tr ′ is defined as below: tr ∼ t tr ′ def

Definition 8 .

 8 A |= φ def ⇔ ∀ρ ∀tr ∈ tr(Aρ); A, ρ, tr, 0 |= φ, where D(ρ) = fv(A) \ dom(A). Definition 9. A ⊑ L B def ⇔ ∀ρ ∀tr ∈ tr(Aρ) ∃tr ′ ∈ tr(Bρ) s.t. ∀i ∀φ; [A, ρ, tr, i |= φ ⇔ B, ρ, tr ′ , i |= φ], where D(ρ) = (fv(A) \ dom(A)) ∪ (fv(B) \ dom(B)).

Definition 11 .

 11 x is totally secret in A(x, y) iff ∀δ(z, z, w); A(x, y) |= G(δ(x, y, w) → P (¬δ(x, y, w)))where δ contains no variables other than ones in {z} ∪ z ∪ w and satisfies that ∀ N ∀ψ∃M : ground s.t. ψ |= ¬δ(M, N , w). Besides, | y| = | z| and w ∩ ({x} ∪ y) = ∅.

4. 5

 5 Comparison with the Work of Chadha et al. Chadha et al. developed the definition of privacy in e-voting as follows. They considered protocol instances in which two voters Alice and Bob participate, and voting options are 0 and 1. Definition 15 ( [7, Definition 9]). The voting process V respects privacy if V |= Aprivacy ∧ Bprivacy where -Aprivacy def = ∧ v∈{0,1} 2(K(Avote(v)) → Bvote(v)), and -Bprivacy def

  Since νm.a(x).x⟨m⟩ ≈ t νm.a(x).x⟨h(m)⟩ holds, we can take a trace of νm.a(x).x⟨h(m)⟩which is statically equivalent to the former.Finally, we compose tr 2 and tr 3 and obtain a desired trace tr 4 .

	tr 3 :νm.a(x).x⟨h(m)⟩
	a(n) -→(νm.z⟨h(m)⟩)[ n /z]
	νv.n⟨v⟩ -→ (νm.{ h(m) /v})[ n /z]
	tr 4 :νm.a(x).x⟨h(m)⟩ | νn.a⟨n⟩.n(y).b⟨y⟩
	νz.a⟨z⟩
	a(n) -→(νm.z⟨m⟩)[ n /z]	νz.a⟨z⟩ -→ νn.(n(y).b⟨y⟩ | { n /z})
	νv.n⟨v⟩ -→ (νm.{ m /v})[ n /z]	z(m) -→νn.(b⟨v⟩ | { n /z})[ m /v]
		νw.b⟨w⟩ -→ νn.{ n /z, v /w}[ m /v]

tr 1 :νm.a(x).x⟨m⟩ tr 2 :νn.a⟨n⟩.n(y).b⟨y⟩

Acknowledgments

The author thanks Prof. M. Hasegawa and Prof. N. Yoshida for discussions. He also thanks the anonymous reviewers for helpful comments and suggestions.

⋆ This work was partly supported by JST ERATO Grant Number JPMJER1603, Japan.


Sergio Feo-Arenis

Milan Vujinović

Bernd Westphal

On Implementable Timed Automata ⋆

Generating code from networks of timed automata is a wellresearched topic with many proposed approaches, which have in common that they not only generate code for the processes in the network, but necessarily generate additional code for a global scheduler which implements the timed automata semantics. For distributed systems without shared memory, this additional component is, in general, undesired. In this work, we present a new approach to the generation of correct code (without global scheduler) for distributed systems without shared memory yet with (almost) synchronous clocks if the source model does not depend on a global scheduler. We characterise a set of implementable timed automata models and provide a translation to a timed while language. We show that each computation of the generated program has a network computation path with the same observable behaviour.

Introduction

Automatic code generation from real-time system models promises to avoid human implementation errors and to be cost and time efficient, so there is a need to automatically derive (at least parts of) an implementation from a model. In this work, we consider a particular class of distributed real-time systems consisting of multiple components with (almost) synchronous clocks, yet without shared memory, a shared clock, or a global scheduler. Prominent examples of such systems are distributed data acquisition systems such as data aggregation in satellite constellations [START_REF] Gobriel | Ridesharing: Fault tolerant aggregation in sensor networks using corrective actions[END_REF][START_REF] Feo-Arenis | Parameterized verification of track topology aggregation protocols[END_REF], the wireless fire alarm system [START_REF] Feo-Arenis | Ready for testing: ensuring conformance to industrial standards through formal verification[END_REF], IoT sensors [START_REF] Tirado-Andrés | A methodology for choosing time synchronization strategies for wireless IoT networks[END_REF], or distributed database systems (e.g. [START_REF] Corbett | Spanner: Google's globally distributed database[END_REF]). For these systems, a common notion of time is important (to meet real-time requirements or for energy efficiency) and is maintained up to a certain precision by clock synchronisation protocols, e.g., [START_REF] Flammini | Clock synchronization of distributed, real-time, industrial data acquisition systems[END_REF][START_REF] Jubran | Formal approach to guard time optimization for TDMA[END_REF][START_REF] Jubran | Optimizing guard time for TDMA in a wireless sensor network -case study[END_REF]. Global scheduling is undesirable because schedulers are expensive in terms of network bandwidth and computational power and the number of components in the system may change dynamically, thus keeping track of all components requires large computational resources.

Timed automata, in particular in the flavour of Uppaal [7], are widely used to model real-time systems (see, for example, [START_REF] Fehnker | Automated analysis of AODV using UPPAAL[END_REF][START_REF] Wibling | Ad hoc routing protocol verification through broadcast abstraction[END_REF]) and to reason about the correctness of systems as the ones named above. Modelling assumptions of timed automata such as instantaneous updates of variables and zero-time message exchange are often convenient for the analysis of timed system models, yet they, in general, inhibit direct implementations of model behaviour on real-world platforms where, e.g., updating variables take time.

In this work, we aim for the generation of distributed code from networks of timed automata with exactly one program per network component (and no other programs, in particular no implicit global scheduler), where all execution times are considered and modelled (including the selection of subsequent edges), and that comes with a comprehensible notion of correctness. Our work can be seen as the first of two steps towards bridging the gap between timed automata models and code. We propose to firstly consider a simple, iterative programming language with an exact real-time semantics (cf. Section 4) as the target for code generation. In this step, which we consider to be the harder one of the two, we deal with the discrepancy between the atomicity of the timed automaton semantics and the non-atomic execution on real platforms. The second step will then be to deal with imprecise timing on real-world platforms.

Our approach is based on the following ideas. We define a short-hand notation (called implementable timed automata) for a sub-language of the well-known timed automata (cf. Section 3). We assume independency from a global scheduler [START_REF] Arenis | On global scheduling independency in networks of timed automata[END_REF] as a sufficient criterion for the existence of a distributed implementation. For the timing aspect, we propose not to use platform clocks directly in, e.g., edge guards (see related work below) but to turn model clocks into program variables and to assume a "sleep" operation with absolute deadlines on the target platform (cf. Section 4). In Section 5, we establish the strong and concrete notion of correctness that for each time-safe computation of a program obtained by our translation scheme there is a computation path in the network with the same observable behaviour. Section 6 shows that our short-hand notation is sufficiently expressive to support industrial case studies and discusses the remaining gap towards real-world programming languages like C, and Section 7 concludes.

Generating code for timed systems from timed automata models has been approached before [START_REF] Abdullah | Synthesis of Ada code from graph-based task models[END_REF][START_REF] Amnell | Code synthesis for timed automata[END_REF][START_REF] Hendriks | Translating Uppaal to not quite C[END_REF][START_REF] Kristensen | Automatic translation from Uppaal to C[END_REF][START_REF] Senthooran | On generating soft real-time programs for non-realtime environments[END_REF]. All these works also generate code for a scheduler (as an additional, explicit component) that corresponds to the implicit, global scheduler introduced by the timed automata semantics [START_REF] Arenis | On global scheduling independency in networks of timed automata[END_REF]. Thus, these approaches do not yield the distributed programs that we aim for. A different approach in the context of timed automata is to investigate discrete sampling of the behaviour [START_REF] Puri | Dynamical properties of timed automata[END_REF] and so-called robust semantics [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF]. A timed automaton model is then called implementable wrt. to certain robustness parameters. Bouyer et al. [START_REF] Bouyer | Timed automata can always be made implementable[END_REF] have shown that each timed automaton (not a network, as in our case) can be sampled and made implementable at the price of a potentially exponential increase in size. A different line of work is [START_REF] Abdellatif | Model-based implementation of real-time applications[END_REF][START_REF] Abdellatif | Rigorous implementation of real-time systems -from theory to application[END_REF][START_REF] Triki | Model-based implementation of parallel real-time systems[END_REF]. They use timed automata (in the form of RT-BIP components [6]) as abstract model of the scheduling of tasks. Considering execution times for tasks, a so-called physical model (in a slightly different formalism) is obtained for which an interpreter has been implemented (the real-time execution engine) that then realises a scheduling of the tasks. The computation time necessary to choose the subsequent task (including the evaluation of guards) is "hidden" in the execution engine (which at least warns if the available time is exceeded), and they state the unfortunate observation that time-safety does not imply time-robustness with their approach.

There is an enormous amount of work on so-called synchronous languages like Esterel [START_REF] Berry | The Esterel synchronous programming language: Design, semantics, implementation[END_REF], SIGNAL [8], Lustre [START_REF] Halbwachs | The synchronous data flow programming language LUSTRE[END_REF] and time triggered architectures such as Giotto/HTL [START_REF] Henzinger | Giotto: a time-triggered language for embedded programming[END_REF]. These approaches provide an abstract programming or modelling language such that for each program, a deployable implementation, in particular for signal processing applications, can be generated.

Preliminaries

As modelling formalism (and input to code generation), we consider timed automata as introduced in [7]. In the following, we recall the definition of timed automata for self-containedness. Our presentation follows [START_REF] Olderog | Real-time systems -formal specification and automatic verification[END_REF] and is standard with the single exception that we exclude strict inequalities in clock constraints.

A timed automaton A = (L, A, X, V, I, E, ℓ ini ) consists of a finite set of locations (including the initial location ℓ ini ), sets A, X, and V of channels, clocks, and (data) variables. A location invariant I : L → Φ(X) assigns a clock constraint over X from Φ(X) to a location. Finitely many edges in E are of the form (ℓ, α, ϕ, r, ℓ ′ ) ∈ L × A !? × Φ(X, V ) × R(X, V ) * × L where A !? consists of input and output actions on channels and the internal action τ , Φ(X, V ) are conjunctions of clock constraints from Φ(X) and data constraints from Φ(V ), and R(X, V ) * are finite sequences of updates, an update either resets a clock or updates a data variable. For clock constraints, we exclude strict inequalities as we do not yet support their semantics (of reaching the upper or lower bound arbitrarily close but not inclusive) in the code generation. In the following, we may write ℓ(e) etc. to denote the source location of edge e.

The operational semantics of a network N = A 1 . . . A n of timed automata as components -and with pairwise disjoint sets of clocks and variables -is the (labelled) transition system

T (N ) = (C, Λ, { λ -→| λ ∈ Λ}, C ini ) over con- figurations. A configuration c ∈ C = { ℓ, ν | ν |= I( ℓ)} consists of location vector ℓ (an n-tuple whose i-th component is a location of A i ) and a valuation ν : X(N ) ∪ V (N ) → R + 0 ∪ D of
C ini = { (ℓ ini,1 , . . . , ℓ ini,n ), 0 } ∩ C. There is a delay transition ℓ, ν t -→ ℓ, ν + t , t ∈ R + 0 , if and only if ν + t ′ |= I( ℓ) for all t ′ ∈ [0, t].
There is an internal transition ℓ, ν τ -→ ℓ ′ , ν ′ , if and only if there is an edge e = (ℓ, τ, ϕ, r, ℓ ′ ) enabled in ℓ, ν and ν ′ is the result of applying e's update vector to ν. An edge is enabled in ℓ, ν if and only if its source location occurs in the location vector, its guard is satisfied by ν, and ν ′ satisfies the destination location's invariant. There is a rendezvous transition ℓ, ν τ -→ ℓ ′ , ν ′ , if and only if there are edges e 0 = (ℓ 0 , a!, ϕ 0 , r 0 , ℓ ′ 0 ) and e 1 = (ℓ 1 , a?, ϕ 1 , r 1 , ℓ ′ 1 ) in two different automata enabled in ℓ, ν and ν ′ is the result of first applying e 0 's and then e 1 's update vector to ν.

A transition sequence of N is any finite or infinite, initial and consecutive sequence of the form ℓ 0 , ν 0 λ1

-→ ℓ 1 , ν 1 λ2 -→ • • • . N is called deadlock-free if no transition sequence of N ends in a configuration c such that there are no c ′ , c ′′ such that c t -→ c ′ λ -→ c ′′ with t ∈ R + 0 , λ / ∈ R + 0 . A computation path of N is a time stamped transition sequence ℓ 0 , ν 0 , t 0 λ1 -→ ℓ 1 , ν 1 , t 1 λ2 -→ • • • s.t. t 0 = 0, t i+1 = t i + λ i+1 if λ i+1 ∈ R + 0 and t i+1 = t i if λ i+1 = τ .
Next, Deadline, Boundary. Given an edge e with source location ℓ and clock constraint ϕ clk , and a configuration c = ℓ, ν , we define next(c,

ϕ clk ) = min{d ∈ R + 0 | ν+d |= I(ℓ)∧ϕ clk } and deadline(c, ϕ clk ) = max{d ∈ R + 0 | ν+next(c, ϕ clk )+ d |= I(ℓ)∧ϕ clk } if minimum/
= x ≤ q, then ∂ϕ clk = x ≥ q.
3 Implementable Timed Automata

In the following, we introduce implementable timed automata that can be seen as a definition of a sub-language of timed automata as recalled in Section 2. As briefly discussed in the introduction, a major obstacle with implementing timed automata models is the assumption that actions are instantaneous. The goal of considering the sub-language defined below is to make the execution time of resets and the duration of message transmissions explicit. Other works like, e.g., [START_REF] Fahrenberg | Higher-dimensional timed automata[END_REF], propose higher-dimensional timed automata where actions take time. We propose to make action times explicit within the timed automata formalism. Definition 1. An implementable timed automaton I = (L, ℓ ini , A, X, V, I, E) consists of locations, initial location, channels, clocks, variables like timed automata, a location invariant I : L → Φ(X) s.t. each I(ℓ) has a boundary ∂I(ℓ), and a finite set

E = E τ ∪ E ! ∪ E ? of edges consisting of -internal edges (ℓ, ϕ, r dat , r clk , ℓ ′ ) ∈ E τ ⊆ L × Φ(X, V ) × R(V ) × R(X) × L, -send edges (ℓ, ϕ, a!, r clk , ℓ ′ ) ∈ E ! ⊆ L × Φ(X, V ) × A ! × R(X) × L, -receive edges (ℓ, ϕ clk , {(a 1 ?, ℓ ′ 1 ), . . . , (a n ?, ℓ ′ n )}, r clk , ℓ ′ ) n ≥ 0, in E ? ⊆ L × Φ(X) × 2 A ? ×L × R(X) × L. ♦
Implementable timed automata distinguish internal, send, and receive edges by action and update in contrast to timed automata. An internal edge models (only) updates of data variables or sleeping idle (which takes time on the platform), a send edge models (only) the sending of a message (which takes time), and a receive edge (only) models the ability to receive a message with a timeout. All kinds of edges may reset clocks. Figure 1 shows an example implementable timed automaton using double-outline edges to distinguish the graphical representation from timed automata. The edge from ℓ 0 to ℓ 1 , for example, models that ℓ6 ℓ0

x ≤ s0

+ g + m ℓ1 x ≤ s1 ℓ2 x ≤ s1 + g + m ℓ3 x ≤ s2 ℓ4 x ≤ s2 + g + m ℓ5 x ≥ s0 + g LZ[id]! ACK? x ≥ s0 + g + m + nl1 x ≥ s1 + g LZ[id]! ACK? x ≥ s1 + g + m + nl3 x ≥ s2 + g LZ[id]! ACK? x ≥ s2 + g + m + nl5 x := 0 x ≥ c -nl0 x ≤ s3 x ≤ c
Fig. 1: The LZ-protocol of sensors [START_REF] Feo-Arenis | Ready for testing: ensuring conformance to industrial standards through formal verification[END_REF] as implementable timed automaton.

ℓ I(ℓ) ℓ ′ I(ℓ ′ ) ϕ τ rdat ; rclk ℓ I(ℓ) ℓ × I(ℓ) ℓ ′ I(ℓ ′ ) ϕ τ rdat ∂I(ℓ) τ rclk (a) Internal edge (ℓ, ϕ, r dat , r clk , ℓ ′ ). ℓ I(ℓ) ℓ ′ I(ℓ ′ ) ϕ a! rclk ℓ I(ℓ) ℓ × I(ℓ) ℓ ′ I(ℓ ′ ) ϕ a! ∂I(ℓ) τ rclk (b) Send edge (ℓ, ϕ, a!, r clk , ℓ ′ ). ℓ I(ℓ) ℓ ′  I(ℓ ′ 1 ) ϕclk a1? ℓ ′ I(ℓ ′ ) rclk ℓ ′ n I(ℓ ′ n ) ϕclk an? ℓ I(ℓ) ℓ ×  I(ℓ) ℓ ′  I(ℓ ′ 1 ) ϕclk a1? ∂I(ℓ) τ rclk ℓ ′ I(ℓ ′ ) τ ∂I(ℓ) rclk ℓ × n I(ℓ) ℓ ′ n I(ℓ ′ n ) ∂I(ℓ) τ rclk ϕclk an? (c) Receive edge (ℓ, ϕ clk , {(a1?, ℓ ′ 1 ), . . . , (an?, ℓ ′ n )}, r clk , ℓ ′ ).
Fig. 2: Edges of the timed automaton of an implementable timed automaton.

message 'LZ[id]' may be transmitted between time s 0 + g (including guard time g and operating time) and s 0 + g + m, i.e., the maximal transmission duration here is m. The time n l1 would be the operating time budgeted for location ℓ 1 .

The semantics of the implementable network N consisting of implementable timed automata I 1 , . . . , I n is the labelled transition system T (A I1 . . . A In ). The timed automata A Ii are obtained from I i by applying the translation scheme in Figure 2 edge-wise. The construction introduces fresh ℓ × -locations. Intuitively, a discrete transition to an ℓ × -location marks the completion of a data update or message transmission in I that started at the next time of the considered configuration. After completion of the update or transmission, implementable timed automata always wait up to the deadline. If the update or transmission has a certain time budget, then we need to expect that the time budget may be completely used in some cases. Using the time budget, possibly with a subsequent wait, yields a certain independence from platform speed: if one platform is fast enough to execute the update or transmission in the time budget, then all faster platforms are. Note that the duration of an action may be zero in implementable timed automata (exactly as in timed automata), yet then there will be no timesafe execution of any corresponding program on a real-world platform.

ℓ1,0 x ≤ s1,0 + w1 ℓ1,1 x ≤ s1,1 + m ℓ1,1 x ≥ s1,0 rdat,1 a! ℓ2,0 y ≤ s2,0 + w2 ℓ2,1 y ≤ s2,2 ℓ2,1 y ≥ s2,0 rdat,2 y ≥ s2,1 a? Fig. 3: Artificial example of a non-implementable network if s 2,0 +w 2 > s 1,0 +w 1 .
In [START_REF] Arenis | On global scheduling independency in networks of timed automata[END_REF], the concept of not to depend on a global scheduler is introduced. Intuitively, independency requires that sending edges are never blocked because no matching receive edge is enabled or because another send edge in a different component is enabled. That is, the schedule of the network behaviour ensures that at each point in time at most one automaton is ready to send, and that each automaton that is ready to send finds an automaton that is ready for the matching receive. Similar restrictions have been imposed on timed automaton models in [START_REF] Berendsen | Compositional abstraction in real-time model checking[END_REF] to verify the ZeroConf protocol. Whether a network depends on a global scheduler is decidable; for details, we refer the reader to [START_REF] Arenis | On global scheduling independency in networks of timed automata[END_REF].

Figure 3 shows an artificial network of implementable timed automata whose independency from a global scheduler depends on the parameters s 1,0 + w 1 and s 2,0 + w 2 . If the location ℓ 1,1 is reached, then the standard semantics of timed automata would (using the implicit global scheduler) block the sending edge until ℓ 2,1 is reached. Yet in a distributed system, the sender should not be assumed to know the current location of the receiver. By choosing the parameters accordingly (i.e., by protocol design), we can ensure that the receiver is always ready before the sender so that the sender is never blocked. In this case, we can offer a distributed implementation.

In the following sections, we only consider networks of implementable timed automata that are deadlock-free, closed component (no shared clocks or variables, no committed locations (cf. [7])), and do not depend on a global scheduler.

Timed While Programs

In this section, we introduce a timed programming language that provides the necessary expressions and statements to implement networks of implementable timed automata as detailed in Section 5. The semantics is defined as a structural operational semantics (SOS) [START_REF] Plotkin | A structural approach to operational semantics[END_REF] that is tailored towards proving the correctness of the implementations obtained by our translation scheme from Section 5. We use a dedicated time component in configurations of a program to track the execution times of statements and support a snapshot operator to measure the time that passed since the execution of a particular statement. Due to lack of space, we introduce expressions on a strict as-needed basis, including message, location, edge, and time expressions. In a general purpose programming language, the former kinds of expressions can usually be realised using integers (or enumerations), and time expressions can be realised using platform-specific representations of the current system time.

Syntax. Expressions of our programming language are defined wrt. given network variables V and X. We assume that each constraint from Φ(X, V ) or expression The set of statements, statement sequences, and timed programs are given by the grammar in Table 1. The term nextedge I ([mexpr ]) represents an implementation of the edge selection in an implementable timed automaton that can optionally be called with a message expression. We denote the empty statement sequence by ǫ and introduce ⊳ as an artificial snapshot operator on statements (see below). The particular syntax with snapshot and non-snapshot statements allows us to simplify the semantics definition below. We use StmSeq to denote the set of all statement sequences.

S ::= v ← expr | t ← texpr | m ← mexpr | l ← lexpr | sleepto(texpr ) | send (mexpr ) | m ← receive(expr ) | e,
Component Configurations and Interpretation of Expressions. A component configuration is a tuple π = S, (β, γ, w, u), σ consisting of a statement sequence S ∈ StmSeq, the operating time of the current statement β ∈ R + 0 (i.e., the time passed since starting to work on the current statement), the time to completion of the current statement γ ∈ R + 0 ∪ {∞} (i.e., the time it will take to complete the work on the current statement), the snapshot time w ∈ R + 0 (i.e., the time since the last snapshot), the platform clock value 3 u ∈ R + 0 , and a type-consistent (R1) v ← expr ; S, (β, 0, w, u), σ S, (0, γ ′ , w ′ , u), σ[v := σ(expr )] (R5) sleepto(texpr ); S, (σ(texpr ), 0, w, u), σ S, (0, γ ′ , w ′ , u), σ (R6) send (mexpr ); S, (β, 0, w, u), σ S, (0, γ ′ , w ′ , u), σ (R7)

m ← receive(expr ); S, (β, γ, w, u), σ S, (0, γ ′ , w ′ , u), σ[m := a] , a ∈ A, if β ≤ σ(expr ), a = ⊥, if β ≥ σ(expr ),
(R8) e, v1, v2 ← nextedge I ([mexpr ]); S, (β, 0, w, u), σ S, (0, γ ′ , w ′ , u), σ[e, v1, v2

:= nextedge I ([mexpr ]) (σ)] (R9a) if • • • e = eexpr i : Si • • • fi; S, (β, 0, w, u), σ Si; S, (0, γ ′ , w ′ , u), σ , σ(e) = σ(eexpr i ) (R9b) if e = eexpr 1 : S1 . . . e = eexpr n : Sn fi; S, (β, 0, w, u), σ S, (0, γ ′ , w ′ , u), σ , ∀ 0 ≤ i ≤ n • σ(e) = σ(eexpr i ) (R10a)
while expr do S od; S, (β, 0, w, u), σ S; while expr do S od; S, (0, γ ′ , w ′ , u), σ , σ(expr ) = true (R10b) while expr do S od; S, (β, 0, w, u), σ S, (0, γ ′ , w ′ , u), σ , σ(expr ) = false Table 2: Discrete reductions of the timed programming language. Rules (R2), (R3), and (R4) for time, message, and location assignment are similar to (R1).

valuation σ of the program variables. We will use operating time and time to completion to define computations of timed while programs (with discrete transitions when the time to completion is 0), and we will use the snapshot time w as an auxiliary variable in the construction of predicates by which we relate program and network computations. The valuation σ maps basic type variables from V b to values from a domain that includes all values of data variables from D as used in the implementable timed automaton and all values needed to evaluate clock constraints (see below), i.e. σ(V b ) ⊆ D b . Time variables from V t are mapped to non-negative real numbers, i.e., σ(V t ) ⊆ R + 0 , message variables from V m are mapped to channels, i.e., σ(V m ) ⊆ A ∪ {⊥} or the dedicated value ⊥ representing 'no message', location variables from V l are mapped to locations, i.e., σ(V l ) ⊆ L, and edge variables from V e are mapped to edges, i.e., σ(V e ) ⊆ E.

For the interpretation of expressions in a component configuration we assume that, if the valuation σ of the program variables corresponds to the valuation of data variables ν, then the interpretation expr (π) of basic type expression expr corresponds to the value of expr under ν. Other variables obtain their values from σ, too, i.e. t (π) = σ(t), m (π) = σ(m), l (π) = σ(l), and e (π) = σ(e); constant symbols are interpreted by their corresponding value, i.e. a (π) = a, ℓ (π) = ℓ, and e (π) = e, and we have t + expr (π) = t (π) + expr (π).

mentable timed automata to programs on realistic platforms, we need to handle possible overflows in the finitely represented current platform time.

There are two non-standard cases. The -symbol denotes the platform clock value of π, i.e..

(π) = u, and we assume that nextloc I ([mexpr ]) (π) yields the destination location of the edge that is currently processed (as given by e), possibly depending on a message name given by mexpr . If e (π) denotes an internal action or send edge e, this is just the destination location ℓ ′ (e), for receive edges it is ℓ ′ (e) if mexpr evaluates to the special value ⊥, and an ℓ i from a (a i ?, ℓ i ) pair in the edge otherwise. If the receive edge is non-deterministic, we assume that the semantics of nextloc I resolves the non-determinism.

Program Computations. Table 2 gives an SOS-style semantics with discrete reduction steps of a statement sequence (or component). Note that the rules in Table 2 (with the exception of receive) apply when the time to completion is 0, that is, at the point in time where the current statement completes. Each rule then yields a configuration with the operating time γ ′ for the new current statement. The new snapshot time w ′ is 0 if the first statement in S is a snapshot statement S⊳, and w otherwise. Rule (R7) updates m to a, which is a channel or, in case of timeout, the 'no message' indicator '⊥'. Rule (R8) is special in that it is supposed to represent the transition relation of an implementable timed automaton. Depending on the program valuation σ, (R8) is supposed to yield a triple of the next edge to work on, this edge's next and deadline. For simplicity, we assume that the interpretation of nextedge I ([mexpr ]) is deterministic for a given valuation of program variables.

A configuration of program

P = S 1 • • • S n is an n-tuple Π = ( S 1 , (β 1 , γ 1 , w 1 , u 1 ), σ 1 , . . . , S n , (β n , γ n , w n , u n ), σ n )
of component configurations; C(P ) denotes the set of all configurations of P .

The operational semantics of a program P is the labelled transition system on system configurations defined as follows. There is a delay transition

( S 1 , (β 1 , γ 1 , w 1 , u 1 ), σ 1 , . . . ) δ -→ ( S 1 , (β 1 + δ, γ 1 -δ, w 1 + δ, u 1 + δ), σ 1 , . . . ) (by delay δ ∈ R + 0 ) if, for all i, 1 ≤ i ≤ n, δ ≤ γ i , i.e.
if no current statement completes strictly before δ. There is an internal transition

(. . . , S i , (β i , 0, w i , u i ), σ i , . . . ) τ -→ (. . . , S ′ i , (0, γ ′ i , w ′ i , u i ), σ ′ i , . . . ) if for some i, 1 ≤ i ≤ n, a discrete reduction rule from Table 2 applies, i.e. if S i , (β i , 0, w i , u i ), σ i ⊢ S ′ i , (0, γ ′ i , w ′ i , u i ), σ ′ i .
There is a synchronisation transition (. . . , S i , (β i , 0, w i , u i ), σ i , . . . S j , (β j , γ j , w j , u j ), σ j , . . . )

mexpr (σi) --------→ (. . . , S ′ i , (0, γ ′ i , w ′ i , u i ), σ i , . . . S ′ j , (0, γ ′ j , w ′ j , u j ), σ ′ j , . . . ) ti-1 ti ne ti-1,0 ti+1 de ti,0 ti+2 n e ′ (a) (b) (c)
if S i , (β i , 0, w i , u i ), σ i ⊢ S ′ i , (0, γ ′ i , w ′ i , u i ), σ i by (R6)
, and S j , (β j , γ j , w j , u j ), σ j ⊢ S ′ j , (0, γ ′ j , w ′ j , u j ), σ ′ j by (R7), and β j ≥ β i , i.e. if component j has been listening at least as long as component i has been sending.

Note that this definition of synchronisation allows multiple components to send at the same time (which may cause message collision on a shared medium) and that, similar to the rendezvous communication of timed automata, out of multiple receivers, only one takes the message. In our application domain these cases do not happen because we assume that implementable networks do not depend on a global scheduler. That is, the program of an implementable network never exhibits any of these two behaviours.

A program configuration is called initial if and only if the k-th component configuration, 1 ≤ k ≤ n, is at S k , with any β k , γ k = 0, w k = 0, u k = 0, and any σ k with σ k (V b ) = 0. We use C ini (P ) to denote the set of initial configurations of program P . A computation of P is an initial and consecutive sequence of program configurations ζ = Π 0 , Π 1 , . . . , i.e. Π 0 ∈ C ini (P ) and for all i ∈ N 0 exists λ ∈ R + 0 ∪ {τ } such that Π i λ -→ Π i+1 as defined above. We need not consider terminating computations of programs here because we assume networks of implementable timed automata without deadlocks.

Correct Implementation of Implementable Networks

The program of the network of implementable timed automata N = I 1 . . . I n is P (N ) = S(I 1 ) . . . S(I n ) (cf. Table 3c). The edges' work is implemented in the corresponding Line 2 of the statement sequences in Tables 3a and3b. The remaining Lines 3 to 8 include the evaluation of guards to choose the edge to be executed next. The result of choosing the edge is stored in program variable e which (by the while loop and the if-statement) moves to Line 1 of the implementation of that edge. The program's timing behaviour is controlled by variable t and is thus decoupled from clocks in the timed automata model. After Line 8, the value of t denotes the absolute time where the execution of the next edge is due. That is, clocks in the program are not directly compared to the platform time (which would raise issues with the precision of platform clocks) but are used to determine points in time that the target platform is supposed to sleep to. By doing so, we also lower the risk of accumulating imprecisions in the sleep operation of the target platform when sleeping for many relative durations. The idea of scheduling work and operating time is illustrated by the timing diagram in Figure 4. Row (a) shows a naïve schedule for comparison: From time t i-1 , decide on the next edge to execute and determine this edge's next time at t i (light grey phase: operating time, must complete within the next edge's next time n e ), then sleep up to the next time (dashed grey line), then execute the edge(s) actions (dark grey phase: work time, must complete within the edge's deadline d e ), then sleep up to the edge's deadline at t i+1 , and start over. The program obtained by our translation scheme implements the schedule shown in Row (b). The program begins with determining the next edge right after the work phase and then has only one sleep phase up to, e.g., t i+2 where the next work phase begins. In this manner, we require only one interaction with the execution platform that implements the sleep phases. Row (c) illustrates a possible extension of our approach where operating time is needed right before the work phase, e.g., to prepare the platform's transceiver for sending a message.

We call the program P (N ) a correct implementation of network N if and only if for each observable behaviour of a time-safe execution of P (N ) there is a corresponding computation path of N . In the following, we provide our notion of time-safety and then elaborate on the above mentioned correspondence between program and network computations.

Intuitively, a computation of P (N ) is not time-safe if either the execution of an edge's statement sequence takes longer than the admitted deadline or if the next time of the subsequent edge is missed, e.g., by an execution platform that is too slow. Note that in a given program computation, the performance of the platform is visible in the operation time β and time to completion γ.

We write Π k :L e n to denote that the program counter of component k is at Line n of the statement sequence of edge e. We use σ| X∪V to denote the (network) configuration encoded by the values of the corresponding program variables. We assume4 that for each program variable v, the old value, i.e., the value before the last assignment in the computation is available as @v.

Definition 2. A computation Π 0 , Π 1 , . . . of P (N ) is time-safe if and only if, for each component k, 0 ≤ k ≤ n and all i ∈ N 0 , 1. Π k i :L e 2 ∧ γ i,k = 0 =⇒ w k ≤ deadline( σ i,k (l), σ i,k | X∪V , σ i,k (e)
), i.e., if the i-th configuration completes (γ i,k = 0) Line 2 of an edge's statement sequence, not more time than admitted by its deadline has been used (w k ), 2.

Π k i :L e 1 ∧ γ i,k = 0 =⇒ w k = σ i,k (@d) + next( σ i,k (l), σ i,k | X∪V , σ i,k (e)
), i.e., the sleepto statement in Line 1 completes exactly after the deadline of the previously worked on edge plus the current edge's next time. ♦ Note that, by Definition 2, operating times may be larger than the subsequent edge's next time in a time-safe computation (if the execution of the current edge completes before its deadline). Stronger notions of time-safety are possible.

For correctness of P (N ), recall that we introduced Timed While Programs to consider the computation time that is needed to compute the transition relation of an implementable network on the fly. In addition, program computations have a finer granularity than network computations: In network computations, the current location and the valuation of clocks and variables are updated atomically in a transition. In the program P (N ), these updates are spread over three lines.

We show that, for each time-safe computation ζ of program P (N ), there is a computation of network N that is related to ζ in a well-defined way. The relation between program and network configurations decouples both computations in the sense that at some times (given by the respective timestamp) the, e.g., clock values in the program configuration are "behind" network clocks (i.e., correspond to an earlier network configuration), at some times they are "ahead", and there are points where they coincide.

Figure 5 illustrates the relation for one edge e. The top row of Figure 5 gives a timing diagram of the execution of the program for edge e of one component. The rows below show the values over time for each program variable v up to e, n, and d. For example, the value of l will denote the source location ℓ of e until Line 3 is completed, and then denotes the destination location ℓ ′ . Similarly, v ′ and x ′ denote the effects of the update vector of e on data variables and clocks. Note that, during the execution of Line 3, we may observe combinations of values Fig. 5: Relating program and network computations for one component. for v and l that are never observed in a network computation due to the atomic semantics of networks. The two bottom lines of Figure 5 show related network configurations aligned with their corresponding program lines. Note that the execution of each line except for Line 1 may be related to two network configurations depending on whether the program timestamp is before or after the current edge's deadline. Figure 6 illustrates the three possible cases: The execution of program Line 2 (work time, dark gray) is related to network configurations with the source location ℓ of the current edge. Right after the work time, the network location ℓ × is related and at the current edge's deadline the destination location ℓ ′ is related. In the related network computation, the transition from ℓ × to ℓ ′ always takes place at the current edge's deadline. This point in time may, in the program computation, be right after work time (Figure 6a, no delay in ℓ × ), in the operating time (Figure 6b), or in the sleep time (Figure 6c).

ℓ ℓ × ℓ ′ ℓ ′ (a) At deadline. ℓ ℓ × ℓ × ℓ ′ ℓ ′ (b) During operating time. ℓ ℓ × ℓ × ℓ ′ ℓ ′ (
The relation between program and network configurations as illustrated in Figure 5 can be formalised by predicates over program and network configurations, one predicate per edge and program line. 5 The following lemma states the described existence of a network computation for each time-safe program computation. The relation gives a precise, component-wise and phase-wise relation of program computations to network computations. In other words, we obtain a precise accounting of which phases of a time-safe program computation cor-respond to a network computation and how. We can argue component-wise by the closed component-assumption from Section 3. Lemma 1. For each time-safe computation ζ = Π 0 , Π 1 , . . . of P (N ), there exists a computation path ξ = c 0,0 , . . . , c 0,m0 , c 1,0 , . . . of N s.t. each network configuration c i,j is properly related to program configuration Π i . ♦

Proof (sketch). The proof is a technical check of the predicates mentioned above during an inductive construction of computation path ξ. For the base case, we show that the initialisation statements in Lines 1 to 4 of Table 3c reach the Line 2 of a send or receive edge (cf. Table 3a and3b) and establish a related network configuration. For the induction step, we need to consider delays and discrete steps of the program. From time-safety of ζ we can conclude to possible delays in N for the related configurations with a case-split wrt. the deadline (cf. Figure 6). When the program time is at the current edge's deadline, the network may delay up to the deadline in an intermediate location ℓ × , take a transition to the successor location ℓ ′ , and possibly delay further. For discrete program steps, we can verify that N has enabled discrete transitions that reach a network configuration that is related to the next program line. Here, we use our assumptions from the program semantics that update vectors have the same effect in the program and the network. And we use the convenient property of our program semantics that the effects of statements only become visible with the discrete transitions. For synchronisation transitions of the program, we use the assumption that the considered network of implementable timed automata does not depend on a global scheduler, in particular that send actions are never blocked, or, in other words, that whenever a component has a send edge locally enabled, then there is a receiving edge enabled on the same channel.

⊓ ⊔

Our main result in Theorem 1 is obtained from Lemma 1 by a projection onto observable behaviour (cf. Definition 3). Intuitively, the theorem states that at each point in time with a discrete transition to Line 2, the program configuration exactly encodes a configuration of network P (N ) right before taking an internal, send, or receive edge.

Definition 3. Let ξ k = ℓ k 0,0 , ν k 0,0 λ0,1 --→ . . . λ0,m 0 ----→ ℓ k 1,0 , ν k 1,0 .
. . be the projection of a computation path ξ of the implementable network N onto component k, 1 ≤ k ≤ n, labelled such that each configuration ℓ k i,0 , ν k i,0 is initial or reached by a discrete transition to a source location of an internal, send, or receive edge.

The sequence

ξ k obs = ℓ k 0,i0 , ν k 0,i0 + d 0 , ℓ k 1,i1 , ν k 1,i1 + d 1 , .
. . , d j ≥ 0, where (j, i j ) is the largest index such that between c := ℓ k j,0 , ν k j,0 and ℓ k j,ij , ν k j,ij + d j exactly next(c) time units have passed, is called the observable behaviour of component k in ξ. ♦ Theorem 1. Let N be an implementable network and ζ k = π 0,0 , . . . , π 0,n0 , π 1,0 , . . . the projection onto the k-th component of a time-safe computation ζ of P (N ) labelled such that π i,ni , π i+1,0 are exactly those transitions in ζ from a Line 1 to the subsequent Line 2. Then ( σ i,0 (l), σ i,0 | X∪V , u i,0 ) i∈N0 is an observable behaviour of component k on some computation path of N . ♦ Fig. 7: Timed automaton of the implementable timed automaton (after applying the scheme from Figure 2) for the LZ-protocol of sensors [START_REF] Feo-Arenis | Ready for testing: ensuring conformance to industrial standards through formal verification[END_REF].

Evaluation and Discussion

The work presented here was motivated by a project to support the development of a new communication protocol for a distributed wireless fire alarm system [START_REF] Feo-Arenis | Ready for testing: ensuring conformance to industrial standards through formal verification[END_REF], without shared memory, only assuming clock synchronisation and message exchange. We provided modelling and analysis of the protocol a priori, that is, before the first line of code had been written. In the project, the engineers manually implemented the model and appreciated how the model indicates exactly which action is due in which situation. Later, we were able to study the handwritten code and observed (with little surprise) striking regularities and similarities to the model. So we conjectured that there exists a significant sub-language of timed automata that is implementable. In our previous work [START_REF] Arenis | On global scheduling independency in networks of timed automata[END_REF], we identified independency from a global scheduler as a useful precondition for the existence of a distributed implementation (cf. Section 2). For this work, we have modelled the LZ-protocol of sensors in the wireless fire alarm system from [START_REF] Feo-Arenis | Ready for testing: ensuring conformance to industrial standards through formal verification[END_REF] as an implementable timed automaton (cf. Figure 1; Figure 7 shows the timed automaton obtained by applying the scheme from Figure 2). Hence our modelling language supports real-world, industry case-studies. Implementable timed automata also subsume some models of time-triggered, periodic tasks that we would model by internal edges only.

From the program obtained by the translation scheme given in Table 3, we have derived an implementation of the protocol in C. Clock, data, location, edge, and message variables become enumerations or integers, time variables use the POSIX data-structure timespec. The implementation runs timely for multiple days. Although our approach with sleeping to absolute times reduces the risk of drift, there is jitter on real-world platforms. The impact of timing imprecision needs to be investigated per application and platform when refining the program of a network to code, e.g., following [START_REF] Bouyer | Timed automata can always be made implementable[END_REF]. In our case study, jitter is much smaller than the model's time unit. Another strong assumption that we use is synchrony of the platform clocks and synchronised starting times of programs which can in general not be achieved on real-world platforms. In the wireless fire alarm system, component clocks are synchronised in an initialisation phase and kept (sufficiently) synchronised using system time information in messages. Robustness against limited clock drift is obtained by including so-called guard times [START_REF] Jubran | Formal approach to guard time optimization for TDMA[END_REF][START_REF] Jubran | Optimizing guard time for TDMA in a wireless sensor network -case study[END_REF] in the protocol design. In the model, this is constant g: Components are ready to receive g time units before message transmission starts in another component.

Note that Theorem 1 only applies to time-safe computations. Whether an implementation is time-safe needs to be analysed separately, e.g., by conducting worst-case execution time (WCET) analyses of the work code and the code that implements the timed automata semantics. The C code for the LZ-model mentioned above actually implements a sleepto function that issues a warning if the target time has already passed (thus indicating non-time-safety). The translation scheme could easily be extended by a statement between Lines 2 and 3 that checks whether the deadline was kept and issues a warning if not. Then, Theorem 1 would strengthen to the statement that all computations of P (I) either correspond to observable behaviour of I or issue a warning. Note that, in contrast to [START_REF] Abdellatif | Model-based implementation of real-time applications[END_REF][START_REF] Abdellatif | Rigorous implementation of real-time systems -from theory to application[END_REF][START_REF] Triki | Model-based implementation of parallel real-time systems[END_REF], our approach has the practically important property that time-safety implies time-robustness, i.e., if a program is time-safe on one platform then it is time-safe on any 'faster' platform. Furthermore, we have assumed a deterministic choice of the next edge to be executed for simplicity and brevity of the presentation. Non-deterministic models can be supported by providing a non-deterministic semantics to the nextedge I function in the programming language and the correctness proof.

Conclusion

We have presented a shorthand notation that defines a subset of timed automata that we call implementable. For networks of implementable timed automata that do not depend on a global scheduler, we have given a translation scheme to a simple, exact-time programming language. We obtain a distributed implementation with one program for each network component, the programs are supposed to be executed concurrently, possibly on different computers. We propose to not substitute (imprecise) platform clocks for (model) clocks in guards and invariants, but to rely on a sleep function with absolute deadlines. The generated programs do not include any "hidden" execution times, but all updates, actions, and the time needed to select subsequent edges are taken into account. For the generated programs, we have established a notion of correctness that closely relates program computations to computation paths of the network. The close relation lowers the mental burden for developers that is induced by other approaches that switch to a slightly different, e.g., robust semantics for the implementation.

Our work decomposes the translation from timed automata models to code into a first step that deals with the discrepancy between atomicity of the timed automaton semantics and the non-atomic execution on real platforms. The second step, to relate the exact-time program to real platforms with imprecise timing is the subject of future work.

  clocks and variables. The location vector has invariant I( ℓ) = n i=1 I(ℓ i ), and we assume a satisfaction relation between valuations and clock and data constraints as usual. Labels are Λ = {τ } ∪ R + 0 , and the set of initial configurations is

  v1, v2 ← nextedge I ([mexpr ]) | if e = eexpr 1 : S1 . . . e = eexpr n : Snfi | while expr do S od S ::= ǫ | S | S⊳ | S; S | S⊳; S (ǫ; S ≡ S; ǫ ≡ S), P ::= S1 • • • Sn.

Fig. 4 :

 4 Fig. 4: Scheduling of work and operating time.

  c) During sleep time.

Fig. 6 :

 6 Fig. 6: Cases of changing from intermediate location to destination location.

  maximum exist and ∞ otherwise. That is, next gives the smallest delay after which e is enabled from c and deadline gives the largest delay for which e is enabled after next. The boundary of a location invariant ϕ clk is a clock constraint ∂ϕ clk s.t. ν + d |= ∂ϕ clk if and only if d = next(c, ϕ clk ) + deadline(c, ϕ clk ). A simple sufficient criterion to ensure existence of boundaries is to use location invariants of the form ϕ clk

Table 1 :

 1 Statements S, statement sequences S, and programs P . from Ψ (V ) over V and X has a corresponding (basic type) program expression and thus that each variable v ∈ V and each clock x ∈ X have corresponding (basic type) program variables v v , v x ∈ V b . In addition, we assume typed variables for locations, edges, and messages, and for times (on the target platform). We additionally consider location variables V l to store the current location, edge variables V e to store the edge currently worked on, message variables V m to store the outcome of a receive operation, and time variables V

t to store platform time. Message expressions are of the form mexpr ::= m | a, m ∈ V m , a ∈ A, location expressions are of the form lexpr ::= l | ℓ | nextloc I (mexpr ), l ∈ V l , ℓ ∈ L, and edge expressions are of the form eexpr ::= e | e, e ∈ V e , e ∈ E. A time expression has the form texpr ::= | t | t + expr , where is the current platform time and t ∈ V t . Note that time variables are different from clock variables. The values of clock variable v x are used to compute a new next time, which is then stored in a time variable, which can be compared to the platform time. Clock variables can be represented by platform integers (given their range is sufficient for the model) while time variables will be represented by platform specific data types like timespec with C [22] and POSIX. In this way, model clocks are only indirectly connected (and compared) to the platform clock.

  Implementation S(e, I) of internal or send edge e in I. Line 2 is the update vector r dat if e ∈ Eτ (internal edge) and the send action send (a) if e ∈ E ! (send edge).

	1: sleepto(t)⊳;	// sleep to current next at ti, then snapshot
	2: ( r dat | send (a) );	// from ti to ti,0, work on τ -or a!-edge
	3: l ← ℓ ′ 0 ;	// now fictionally at ti+1 in destination location
	4: x ← (x + n + d)[ r clk ]; // fictionally delay to ti+1, reset clocks
	5: t ← t + d;	// new sleep goal (1/2, see below): to ti+1 (old deadline)
	6: e, n, d ← nextedge I (); // choose next edge e based on current component con-
	7:	//	figuration, get next and deadline of e
	8: t ← t + n	// new sleep goal (2/2): and then to ti+2 (new next)
	(a) 2: m ← receive(d);	// from ti to ti,0, work on receive edge, i.e. read message
	3: l ← nextlocI(m);	// at ti,0, if no m-match: treat like timeout
	6: e, n, d ← nextedge I (m); // choose next edge e based on current component confi-
	7:

// guration and message (!), get next and deadline of e (b) Implementation S(e, I) of receive edge e in I; Lines 1, 4-5, and 8 are as in Figure 3a. 1: t ← ; // get beginning of time; assume basic type variables are 0 2: l ← ℓini ; // initialise location 3: e, n, d ← nextedge I (); // choose next edge e based on component configuration 4: t ← t + n; // new sleep goal: beginning of time plus next of e 5: while true do if e = e0 : S(e0, I) • • • e = en : S(en, I) fi od (c) Implementation S(I) of implementable timed automaton I.

Table 3 :

 3 Implementation scheme for implementable timed automaton.

⋆ Partly supported by the German Research Council (DFG) under grant WE 6198/1-1.

Using a real, unbounded value for the platform clock avoids the issue of overflows in executions of programs as defined here. When refining the programs of imple-

Without loss of generality, since the program could be augmented by an auxiliary variable @v for each variable v that provides the old value of v.

Details on these predicates and a detailed proof of Lemma 1 are provided in a corresponding technical report.