Runtime enforcement of timed properties revisited

Runtime enforcement is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties. This paper deals with runtime enforcement of timed properties by revisiting the foundations of runtime enforcement when time between events matters. We propose a new enforcement paradigm where enforcement mechanisms are time retardants: to produce a correct output sequence, additional delays are introduced between the events of the input sequence. We consider runtime enforcement of any regular timed property defined by a timed automaton. We prove the correctness of enforcement mechanisms and prove that they enjoy two usually expected features, revisited here in the context of timed properties. The first one is soundness meaning that the output sequences (eventually) satisfy the required property. The second one is transparency, meaning that input sequences are modified in a minimal way. We also introduce two new features, (i) physical constraints that describe how a time retardant is physically constrained when delaying a sequence of timed events, and (ii) optimality, meaning that output sequences are produced as soon as possible. To facilitate the adoption and implementation of enforcement mechanisms, we describe them at several complementary abstraction levels. Our enforcement mechanisms have been implemented and our experimental results demonstrate the feasibility of runtime enforcement in a timed context and the effectiveness of the mechanisms.

1. As our experiments in Sect. 4 show, the computation time of the monitor upon the reception of an event is relatively low. Moreover, given some average computation time per event and a property, one can determine easily whether the computation time is negligible or not.

2. Observe that the notions of transparency and optimality in a timed context are interpretations of the historical notion of transparency when dealing with enforcement mechanisms as time retardants: the output sequence is a minimally-delayed prefix of the input sequence.

3. As one can observe, these definitions of safety and co-safety TAs slightly differ from the usual ones by expressing constraints on the initial state. As a consequence of these constraints, consistently with Definition 2, the empty and universal properties are ruled out from the set of safety and co-safety properties, respectively.

4. The pyuppaal and DBM libraries are provided by Aalborg University. They can be downloaded at http://people.cs.aau.dk/~adavid/python/.

Authors and Affiliations

1. INRIA Rennes-Bretagne Atlantique, Rennes, France

   Srinivas Pinisetty, Thierry Jéron & Hervé Marchand

2. Laboratoire d’Informatique de Grenoble, Université Grenoble I, Grenoble, France

   Yliès Falcone

3. LaBRI, Université de Bordeaux-CNRS, Bordeaux, France

   Antoine Rollet

4. CRIM—Centre de recherche informatique de Montréal, Montréal, Canada

   Omer Nguena Timo

Corresponding author

Correspondence to Yliès Falcone.

Proofs

1.1 Proof of Proposition 3: item 1 (physical constraints)

We shall prove that, given a property \(\varphi ,\) the associated enforcement function \(E_\varphi :\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\) defined as per Definition 8 satisfies the physical constraints (Phy1) and (Phy2). That is, we shall prove that:

• Proof that the enforcement function satisfies (Phy1). Let us consider \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*},\,t,\,t^{\prime }\in {\mathbb {R}}_{\ge 0},\) such that \(t\le t^{\prime }.\) We will prove that there exists \(o \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\) s.t. \(E_\varphi (\sigma ,\,t^{\prime }) = E_\varphi (\sigma ,\,t)\cdot o.\) The fact that \(E_\varphi \) satisfies (Phy1) is a direct consequence of the following observations:

  • \(\forall \sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\,\forall t,\,t^{\prime }\in {\mathbb {R}}_{\ge 0}:\,t \le t^{\prime } \implies \!\!\! \mathrm {obs}(\sigma ,\,t) \preccurlyeq \mathrm {obs}(\sigma ,\,t^{\prime })\), i.e., \(\mathrm {obs}\) is monotonic in its second argument;

  • \(\forall w,\,w^{\prime }\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*:\,w\preccurlyeq w^{\prime }\!\implies \!{{\mathrm{store}}}(w) \preccurlyeq {{\mathrm{store}}}(w^{\prime }),\) i.e., \({{\mathrm{store}}}\) is monotonic;

  • \(\forall \sigma ,\,\sigma ^{\prime }\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\,\forall t\in {\mathbb {R}}_{\ge 0}:\, \sigma \preccurlyeq \sigma ^{\prime } \!\!\implies \!\!\mathrm {obs}(\sigma ,\,t) \preccurlyeq \mathrm {obs}(\sigma ^{\prime },\,t),\) i.e., \(\mathrm {obs}\) is monotonic in its first argument.

• Proof that the enforcement function satisfies (Phy2). From Definition 8, since \(E_\varphi (\sigma ,\,t) = \mathrm {obs}(\varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma ,\,t))),\,t),\) from the definition of \(\mathrm {obs}\) and the property of \(\mathrm {obs}\) that \(\forall \sigma :\,{{\mathrm{time}}}(\mathrm {obs}(\sigma ,\,t)) \le t,\) applied to \(\varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma ,\,t))),\) we can conclude that \({{\mathrm{time}}}(E_\varphi (\sigma ,\,t))\le t.\) Thus, \(E_\varphi \) satisfies (Phy2).

1.2 Proof of Proposition 3: item 2 (soundness and transparency)

We shall prove that, given a property \(\varphi ,\) the associated enforcement function \(E_\varphi :\,({\mathbb {R}}_{\ge 0}\times \Sigma )^*\times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) as per Definition 8 is sound and transparent as per Definition 7, i.e., \(E_\varphi \) satisfies the constraints (Snd) and (Tr).

Recall that \(E_\varphi :\,({\mathbb {R}}_{\ge 0}\times \Sigma )^*\times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) is defined as:

where:

• function \(\mathrm {obs}:\,({\mathbb {R}}_{\ge 0}\times \Sigma )^*\times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) is the observation function defined in Sect. 2,

• function \({{\mathrm{store}}}:\, ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\times ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) is defined as follows in Sect. 3.2.1:

  $$\begin{aligned} \begin{array}{rll} {{\mathrm{store}}}(\epsilon ) &{} = &{} (\epsilon ,\,\epsilon )\\ {{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) &{} = &{} {\left\{ \begin{array}{ll} \left( \sigma _{s}\cdot {{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}K,\,\epsilon \right) &{} \mathrm{if }\,K \ne \emptyset , \\ \left( \sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a)\right) &{} \mathrm{otherwise }, \end{array}\right. } \\ &{}&{} \mathrm{with } \\ &{}&{} \,\,\left( \sigma _{s},\,\sigma _{c}\right) = {{\mathrm{store}}}(\sigma ), \\ &{}&{} \,\,K=\kappa _{\varphi }\left( {{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a)\right) , \end{array} \end{aligned}$$

  with \( \kappa _{\varphi }(T,\,\sigma _{s},\,\sigma _{c}) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\{w \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \mid w \preccurlyeq _{d} \sigma _{c} \wedge |w| = |\sigma _{c}| \wedge \sigma _s\cdot w\models \varphi \wedge {{\mathrm{delay}}}(w(1)) \ge T - {{\mathrm{time}}}(\sigma _s)) \}.\)

From \(\mathbf {(Snd)}\) and \(\mathbf {(Tr)},\) we define the constraints that hold for a particular word \(\sigma \) and a particular time instant t (i.e., universal quantifications are removed). We denote these propositions by \(\mathbf {(Snd)}_{\sigma ,t}\) and \(\mathbf {(Tr)}_{\sigma ,t},\) respectively. Thus, we shall prove that \(E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ,t}\) and \(\mathbf {(Tr)}_{\sigma ,t}\) for any \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) and \(t\in {\mathbb {R}}_{\ge 0}.\) For this purpose, we perform an induction on the length of \(\sigma .\)

Induction basis. Let us suppose that \(|\sigma |=0,\) thus \(\sigma =\epsilon \) in \(({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}.\) First, we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\,\mathrm {obs}(\sigma ,\,t) = \epsilon .\) Second, we have \({{\mathrm{store}}}(\epsilon ) = (\epsilon ,\,\epsilon ).\) Consequently, we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t) = \epsilon .\) We now prove that, at any time \(t\in {\mathbb {R}}_{\ge 0},\,E_\varphi \) satisfies \(\mathbf {(Snd)}_{\epsilon ,t}\) and \(\mathbf {(Tr)}_{\epsilon ,t},\) successively.

• For \(\sigma =\epsilon ,\) we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t) = \epsilon .\) Thus, \(E_\varphi \) satisfies \(\mathbf {(Snd)}_{\epsilon ,t},\) for any time \(t\in {\mathbb {R}}_{\ge 0}.\)

• Since \(\mathrm {obs}(\epsilon ,\,t) = \epsilon \) and \(\epsilon \preccurlyeq _{d} \epsilon ,\) we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\,E_\varphi (\epsilon ,\,t) \preccurlyeq _{d} \epsilon .\) That is, \(E_\varphi \) satisfies \(\mathbf {(Tr)}_{\epsilon ,t},\) for any time \(t\in {\mathbb {R}}_{\ge 0}.\)

Induction step. Let us consider \(n\in \mathbb {N}\) and suppose that for any \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) with \(|\sigma |\le n,\) any \(t\in {\mathbb {R}}_{\ge 0},\,E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ,t}\) and \(\mathbf {(Tr)}_{\sigma ,t}.\)

Let us now prove that for any \(\sigma ^{\prime }\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) with \(|\sigma ^{\prime }| = n+1,\) for any \(t\in {\mathbb {R}}_{\ge 0},\,E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ^{\prime },t}\) and \(\mathbf {(Tr)}_{\sigma ^{\prime },t}.\) For this purpose, let us consider some input timed word \(\sigma ^{\prime }\) with \(|\sigma ^{\prime }|=n+1.\) Thus \(\sigma ^{\prime }=\sigma \cdot (\delta ,\,a)\) for some \(\sigma \) with \(|\sigma |=n,\,\delta \in {\mathbb {R}}_{\ge 0}\) and \(a \in \varSigma .\) Let us consider some time instant \(t\in {\mathbb {R}}_{\ge 0}.\)

We distinguish two cases according to whether the sum of delays of the timed word \(\sigma \cdot (\delta ,\,a)\) is greater than t or not, i.e., whether \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) > t\) or not.

• Case \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) > t.\) In this case, \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\sigma ,\,t).\) Consequently, \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t))),\,t) = E_\varphi (\sigma ,\,t).\) From the induction hypothesis, we directly deduce that \(E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ^{\prime },t}\) and \(\mathbf {(Tr)}_{\sigma ^{\prime },t}.\)

• Case \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) \le t.\) In this case \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) =\sigma \cdot (\delta ,\,a).\) We distinguish two cases, based on whether \(K = \emptyset ,\) or not.

  • Case \(K=\kappa _{\varphi }({{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a))=\emptyset .\) From the definition of \({{\mathrm{store}}},\) we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = (\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a)),\) and \(\varPi _{1}({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a))) = \sigma _{s}.\) We also have \(\varPi _{1}({{\mathrm{store}}}(\sigma )) = \sigma _{s}.\) From the definition of \(E_\varphi ,\) we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) =E_\varphi (\sigma ,\,t).\) From the induction hypothesis, we deduce that \(E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ^{\prime },t}\) and \(\mathbf {(Tr)}_{\sigma ^{\prime },t}.\)

  • Case \(K =\kappa _{\varphi }({{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a)) \ne \emptyset .\) From the definition of \({{\mathrm{store}}},\) we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = ((\sigma _s\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\, \epsilon ),\) and \(\varPi _{1}({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _s\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K).\) We distinguish two cases based on whether \({{\mathrm{time}}}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K) > t\) or not.

    • Case \({{\mathrm{time}}}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K) > t.\) We further distinguish two more cases based on whether \({{\mathrm{time}}}(\sigma _{s}) > t\) or not.

      • Case \({{\mathrm{time}}}(\sigma _{s}) > t.\) In this case, we have \(\mathrm {obs}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\,t) = \mathrm {obs}(\sigma _{s},\,t).\) Thus we have \(E_\varphi (\sigma \cdot (\delta ,\,a) ,\,t) = E_\varphi (\sigma ,\,t).\) So, from the induction hypothesis, we deduce that \(E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ^{\prime },t}\) and \(\mathbf {(Tr)}_{\sigma ^{\prime },t}.\)

      • Case \({{\mathrm{time}}}(\sigma _{s}) \le t.\) In this case we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \sigma _{s} \cdot O,\) where \(O \prec {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K.\) From the definition of K and \(\kappa _{\varphi }\) we know that \(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K \in \varphi .\) Since \(\forall t^{\prime } \ge {{\mathrm{time}}}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K)\) and \(E_\varphi (\sigma \cdot (\delta ,\,a)) = \sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\,E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ^{\prime },t},\) for any \(t\in {\mathbb {R}}_{\ge 0}.\) From the induction hypothesis, we know that \(\sigma _{s} \preccurlyeq _{d} \sigma .\) From the definition of K and \(\kappa _{\varphi },\) and using the induction hypothesis, we can conclude that \(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K \preccurlyeq _{d} \sigma \cdot (\delta ,\,a),\) and thus we also have \(\sigma _{s} \cdot O \preccurlyeq _{d} \sigma \cdot (\delta ,\,a).\) Thus \(E_\varphi \) satisfies \(\mathbf {(Tr)}_{\sigma ^{\prime },t}.\)

    • Case \({{\mathrm{time}}}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K) \le t.\) In this case, we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \sigma _{s} \cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}} K.\) From the definition of K and \(\kappa _{\varphi }\) we know that \(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K \in \varphi .\) Thus \(E_\varphi \) satisfies \(\mathbf {(Snd)}_{\sigma ^{\prime },t}.\) From the induction hypothesis, we know that \(\sigma _{s} \preccurlyeq _{d} \sigma .\) From the definition of K and \(\kappa _{\varphi },\) and using the induction hypothesis, we can conclude that \(\sigma _{s} \cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}} K \preccurlyeq _{d} \sigma \cdot (\delta ,\,a).\) Thus \(E_\varphi \) satisfies \(\mathbf {(Tr)}_{\sigma ^{\prime },t}.\)

1.3 Proof of Proposition 4

We shall prove that, given a property \(\varphi ,\) the associated enforcement function \(E_\varphi :\,({\mathbb {R}}_{\ge 0}\times \Sigma )^*\times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) as per Definition 8 satisfies the optimality constraint \(\mathbf {(Op)}\) (from Definition 4).

where the function \(E_\varphi \) is defined in Sect. 3.2.1 and recalled in the previous proof.

From \(\mathbf {(Op)}\), we define the constraint dedicated to a particular word \(\sigma \) and a particular time instant t (i.e., universal quantifications are removed). We denote this proposition by \(\mathbf {(Op)}_{\sigma ,t}.\) Thus, we shall prove that \(E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ,t}\) for any \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) and \(t\in {\mathbb {R}}_{\ge 0}.\) For this purpose, we perform an induction on the length of \(\sigma .\)

Induction basis. Let us suppose that \(|\sigma |=0,\) thus \(\sigma =\epsilon \) in \(({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}.\) First, we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\,\mathrm {obs}(\sigma ,\,t) = \epsilon .\) Second, we have \( {{\mathrm{store}}}(\epsilon ) = (\epsilon ,\,\epsilon ).\) Consequently, we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t) = \epsilon .\) For \(\sigma =\epsilon ,\) we have \(\forall t \in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t) = \epsilon .\) Thus, \(E_\varphi \) vacuously satisfies \(\mathbf {(Op)}_{\epsilon ,t},\) for any \(t\in {\mathbb {R}}_{\ge 0}.\)

Induction step. Let us consider \(n\in \mathbb {N}\) and suppose that for any \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) with \(|\sigma |\le n,\) any \(t\in {\mathbb {R}}_{\ge 0},\) \(E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ,t}.\)

Let us now prove that, for any \(\sigma ^{\prime }\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) with \(|\sigma ^{\prime }| = n+1,\) for any \(t\in {\mathbb {R}}_{\ge 0},\,E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ^{\prime },t}.\) For this purpose, let us consider some input timed word \(\sigma ^{\prime }\) with \(|\sigma ^{\prime }|=n+1.\) Thus \(\sigma ^{\prime }=\sigma \cdot (\delta ,\,a)\) for some \(\sigma \) with \(|\sigma |=n,\,\delta \in {\mathbb {R}}_{\ge 0}\) and \(a \in \varSigma .\) Let us consider some time instant \(t\in {\mathbb {R}}_{\ge 0}.\)

We distinguish two cases according to whether the sum of delays of the timed word \(\sigma \cdot (\delta ,\,a)\) is greater than t or not, i.e., whether \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) > t\) or not.

• Case \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) > t.\) In this case, \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\sigma ,\,t).\) Consequently, \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t))),\,t) = E_\varphi (\sigma ,\,t).\) From the induction hypothesis, we directly deduce that \(E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ^{\prime },t}.\)

• Case \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) \le t.\) We have \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) = \sigma \cdot (\delta ,\,a).\) We distinguish two cases, based on whether \(K = \emptyset ,\) or not, where \(K=\kappa _\varphi ({{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a)).\)

  • Case \(K=\emptyset .\) From the definition of \({{\mathrm{store}}},\) we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = (\sigma _{s},\, \sigma _{c}\cdot (\delta ,\,a)),\) and \(\varPi _{1}({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a))) = \sigma _{s}.\) We also have \(\varPi _{1}({{\mathrm{store}}}(\sigma )) = \sigma _{s}.\) From the definition of \(E_\varphi ,\) we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = E_\varphi (\sigma ,\,t).\) From the induction hypothesis, we deduce that \(E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ^{\prime },t}.\)

  • Case \(K \ne \emptyset .\) From the definition of \({{\mathrm{store}}},\) we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = ((\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K, \epsilon ),\) and \(\varPi _{1}({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K).\) We distinguish two cases based on whether \({{\mathrm{time}}}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K) > t\) or not.

    • Case \({{\mathrm{time}}}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K) > t.\) We further distinguish two more cases based on whether \({{\mathrm{time}}}(\sigma _{s}) > t\) or not.

      • Case \({{\mathrm{time}}}(\sigma _{s}) > t.\) We have \(\mathrm {obs}(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\,t) = \mathrm {obs}(\sigma _{s},\,t).\) Thus, we have \(E_\varphi (\sigma \cdot (\delta ,\,a) ,\,t) = E_\varphi (\sigma ,\,t).\) Hence, from the induction hypothesis, we deduce that \(E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ^{\prime },t}.\)

      • Case \({{\mathrm{time}}}(\sigma _{s}) \le t.\) We have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \sigma _{s} \cdot O ,\) where \(O \prec {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K.\) According to the definition of \({{\mathrm{store}}},\,\sigma _{s}\cdot O \not \models \varphi .\) Thus, \(E_\varphi \) vacuously satisfies \(\mathbf {(Op)}_{\sigma ^{\prime },t}.\)

    • Case \({{\mathrm{time}}}(\sigma _s\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K) \le t .\) We have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K.\) From the definition of K and \(\kappa _{\varphi },\) we know that \(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K \models \varphi .\) From the definition of \({{\mathrm{store}}},\) we know that \(\sigma _{s}\) is the maximal strict prefix of \(\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\) which satisfies \(\varphi .\) The last subsequence which again makes the output satisfy the property is \({{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K.\) From the definition of K and \(\kappa _{\varphi },\) we also know that the \({{\mathrm{delay}}}({{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K(1))\ge {{\mathrm{time}}}(\sigma )+\delta - {{\mathrm{time}}}(\sigma _{s}).\) Thus, we can conclude that \(E_\varphi \) satisfies \(\mathbf {(Op)}_{\sigma ^{\prime },t}.\)

1.4 Preliminaries to the proof of Proposition 5: characterizing the configurations of EMs

We first convey some remarks (Sect. 6), define some notions (Sect. 6) and lemmas (Sect. 6) related to the configurations of EMs.

1.4.1 Some remarks

Remark 12

In the following proofs, without loss of generality, we assume that at any time only one of the rules of the EM applies. This simplification does not come at the price of reducing the generality nor the validity of the proofs because (i) the store and dump rules of the EM assign different variables and do not rely on the same conditions, and (ii) the operations of EMs are assumed to be executed in zero time. The considered simplification however reduces the number of (equivalent cases) in the following proofs.

Remark 13

Between the occurrence of two (input or output) events the configuration of the EM evolves according to the idle rule (since it is the rule with lowest priority). To simplify notations we will use a rule to simplify the representation of \(\mathcal{E}_\mathrm {ioo}\in (({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \}) \times Op \times (({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \})\) stating that

for any \(\sigma ,\sigma ^{\prime }\in (({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \}) \times Op \times (({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \})\) and \(\delta _{1},\,\delta _2\in {\mathbb {R}}_{\ge 0}.\) Thus for \(\mathcal{E}_\mathrm {ioo}\) we will only consider sequences of \((({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \}) \times Op \times (({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \})\) where delays appearing in the \({{\mathrm{idle}}}\) operation are maximal (i.e., there is no sequence of two consecutive events with an \({{\mathrm{idle}}}\) operation).

1.4.2 Some notations

Since it is assumed that at most one rule of the EM applies at any time, let us define the functions \({{\mathrm{config_{in}}}},\,{{\mathrm{config_{out}}}}:\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\times {\mathbb {R}}_{\ge 0}\rightarrow C^{{\scriptscriptstyle \mathcal{E}}}\) that give respectively the input and output configurations of an EM reading an input sequence at some time instant. More formally, given some \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\,t\in {\mathbb {R}}_{\ge 0}:\)

• \({{\mathrm{config_{in}}}}(\sigma ,\,t) = c_{\sigma }^{t}\) such that \(c_{0}^{{\scriptscriptstyle \mathcal{E}}} \mathop {\hookrightarrow ^{*}}\limits ^{w(\sigma ,\,t)} c_{\sigma }^{t}\) where \(w(\sigma ,\,t) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}{{\mathrm{min}}}_{\preceq }\{ ioo \preceq \mathcal{E}_\mathrm {ioo}(\sigma ,\,t)\mid {{\mathrm{timeop}}}( ioo ) = t\};\)

• \({{\mathrm{config_{out}}}}(\sigma ,\,t) = c_{\sigma }^{t}\) such that \(c_{0}^{{\scriptscriptstyle \mathcal{E}}} \mathop {\hookrightarrow ^{*}}\limits ^{\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)} c_{\sigma }^{t}.\)

Observe that, when at some time instant, only the idle rule applies, \({{\mathrm{config_{in}}}}(\sigma ,\,t) = {{\mathrm{config_{out}}}}(\sigma ,\,t)\) holds.

Moreover, for any two \(t,\,t^{\prime }\in {\mathbb {R}}_{\ge 0}\) such that \(t^{\prime }\ge t,\) we note \(\mathcal{E}(\sigma ,\,t,\,t^{\prime })\) for \(\mathcal{E}(\sigma ,\,t^{\prime }) \setminus \mathcal{E}(\sigma ,\,t),\) i.e., the output sequence of an EM between t and \(t^{\prime }.\)

1.4.3 Some intermediate lemmas

Before tackling the proof of Proposition 5, we give a list of lemmas that describes the behavior of an EM, describing the configurations or the output at some particular time instant for some input and memory content.

Similarly to the first physical constraint, the following lemma states that the EM cannot change what it has output. More precisely, when the EM is seen as function \(\mathcal{E},\) the output is monotonic w.r.t. \(\preceq .\)

Lemma 1

(Monotonicity of the outputs of EMs) Function \(\mathcal{E}:\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\) is monotonic in its second parameter: \(\forall \sigma \in (\mathbb {R}\times \varSigma )^{*},\,\forall t,\,t^{\prime }\in {\mathbb {R}}_{\ge 0}:\,t\le t^{\prime } \implies \mathcal{E}(\sigma ,\,t) \preceq \mathcal{E}(\sigma ,\,t^{\prime }).\)

The lemma states that for any input sequence \(\sigma ,\) if we consider two time instants \(t,\,t^{\prime }\) such that \(t\le t^{\prime },\) then the output of the EM at time t is a prefix of the output at time \(t^{\prime }.\)

Proof (of Lemma 1)

The proof directly follows from the definitions of the function \(\mathcal{E}\) associated to an EM (see Sect. 3.4, p. 20) which directly depends on \(\mathcal{E}_\mathrm {ioo},\) which is itself monotonic over time (because of the definition of EMs). \(\square \)

As a consequence, one can naturally split the output of the EM over time, as it is stated by the following corollary.

Corollary 1

(Separation of the output of the EM over time)

The corollary states that for any sequence \(\sigma \) input to \(\mathcal{E},\) if we consider three time instants \(t_{1},\,t_{2},\,t_{3}\in {\mathbb {R}}_{\ge 0}\) such that \(t_{1}\le t_{2}\le t_{3},\) the output of \(\mathcal{E}\) between \(t_{1}\) and \(t_{3}\) is the concatenation of the output between \(t_{1}\) and \(t_{2}\) and the output between \(t_{2}\) and \(t_{3}.\)

Proof (of Corollary 1)

The corollary directly follows from Lemma 1. \(\square \)

The following lemma states that, at some time instant t, the output of the EM only depends on what has been observed until time t. In other words, the EM can work in an online fashion.

Lemma 2

(Dependency of the output on the observation only)

Proof (of Lemma 2)

The proof of the lemma directly follows from the definitions of \(\mathcal{E}_\mathrm {ioo}\) (Definition 10, p. 20) and \(\mathrm {obs}\) (in Sect. 2). Indeed, using \(\mathrm {obs}(\sigma ,\,t) = \mathrm {obs}(\mathrm {obs}(\sigma ,\,t),\,t),\) we deduce that \(\mathcal{E}_\mathrm {ioo}(\sigma ,\,t) = \mathcal{E}_\mathrm {ioo}(\mathrm {obs}(\sigma ,\,t),\,t),\) for any \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) and \(t\in {\mathbb {R}}_{\ge 0}.\) Using \(\mathcal{E}(\sigma ,\,t)= \varPi _{3}(\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)),\) we can deduce the expected result. \(\square \)

The following lemma indicates the value of the store variable inside the configurations at some special time instants (corresponding to the time necessary to read prefixes of the input sequence).

Lemma 3

(Values of \({{\mathrm{config_{in}}}}\) when reading events)

Proof (of Lemma 3)

The proof can be done using a straightforward induction on the length of the maximal considered prefix \(\sigma ^{\prime }\) of \(\sigma .\) Moreover, the proof uses the facts that between two prefixes of the input sequence, (i) no modification is brought to the store variable, and (ii) the store variable is reset upon the store of each event. \(\square \)

The following lemma states that only the memory content \(\sigma _{s}\) and the value of the dump variable influence the output of the EM. More specifically, if, after reading some sequence, an EM reaches some configuration, its future output is fully determined by the memory content \(\sigma _{s}\) (containing the corrected sequence) and the value of the dump variable (d), during the total time needed to output it.

Lemma 4

(Values of \({{\mathrm{config_{out}}}}\) when releasing events)

The lemma states that whatever is the output configuration \((\sigma _{s},\,\sigma _{c},\,s,\,d,\,m_{t},\,q)\) reached by reading some input sequence \(\sigma \) at some time instant \(t\ge {{\mathrm{time}}}(\sigma ),\) then for any prefix \(\sigma _{s}^{\prime }\) of \(\sigma _{s}\) the output configuration reached at time \(t + {{\mathrm{time}}}(\sigma _{s}^{\prime }) - d\) (we add the time needed to read \(\sigma _{s}^{\prime }\) minus the value of the dump clock) is such that \(\sigma _{s}^{\prime }\) has been released from the memory (the memory is \(\sigma _{s}\setminus \sigma _{s}^{\prime }\)) and the value of the dump variable has just been reset to \(0\).

Proof (of Lemma 4)

The proof is a straightforward induction on the length of \(\sigma _{s}^{\prime }.\) It uses the fact that the considered configurations occur at time instants greater than \({{\mathrm{time}}}(\sigma ),\) hence implying that no input event can be read any more. Consequently, following the definition of the EM (Definition 9, p. 18), on the configurations of the EM, only the idle and dump rules apply. Between \({{\mathrm{time}}}(\sigma _{s}^{\prime })\) and \({{\mathrm{time}}}(\sigma _{s}^{\prime }\cdot (\delta ,\,a))\) where \(\sigma _{s}^{\prime } \preceq \sigma _{s}^{\prime } \cdot (\delta ,\,a) \preceq \sigma _{s},\) the configuration of the EM evolves only using the idle rule (no other rule applies) until \({{\mathrm{config_{in}}}}(\sigma ,\,t+{{\mathrm{time}}}(\sigma _{s}^{\prime })) = (\sigma _{s}\setminus \sigma _{s}^{\prime },\,\sigma _{c},\,s^{\prime } + \delta ,\,\delta ,\,m_{t},\,q)\) with \(\sigma _{s} \setminus \sigma _{s}^{\prime }.\) The dump rule is then applied to get the following derivation \((\sigma _{s}\setminus \sigma _{s}^{\prime },\,\sigma _{c},\,s^{\prime } + \delta ,\,\delta ,\,m_{t},\,q) \mathop {\hookrightarrow }\limits ^{\epsilon / dump (\delta ,a)/\epsilon } (\sigma _{s}\setminus (\sigma _{s}^{\prime }\cdot (\delta ,\,a)),\,\sigma _{c},\,s^{\prime } + \delta ,\,0,\,m_{t},\,q).\) \(\square \)

The following lemma states that when an EM has nothing to read in input anymore, what is output is the observation of its memory content over time.

Lemma 5

The lemma states that, if after some time t, after reading an input sequence \(\sigma ,\) the EM is in an output configuration that contains \(\sigma _{s}\) as a memory content, then whatever is the prefix \(\sigma _{s}^{\prime }\) of \(\sigma _{s}\) we consider, the output of the EM between t and \(t+{{\mathrm{time}}}(\sigma _{s}^{\prime })\) is the observation of \(\sigma _{s}^{\prime }.\)

Proof (of Lemma 5)

The proof is performed by induction on the length of \(\sigma _{s}^{\prime }\) and uses Lemma 4.

• Case \(|\sigma _{s}^{\prime }| = 0.\) In this case, \(\sigma _{s}^{\prime } = \epsilon \) and since \({{\mathrm{time}}}(\epsilon ) = 0\) and \(\mathcal{E}(\sigma ,\,t,\,t-d)\) is not defined, the lemma vacuously holds.

• Induction case Let us suppose that the lemma holds for all prefixes \(\sigma _{s}^{\prime }\) of some maximum length \(n\in [0,\,|\sigma _{s}|-1].\) Let us consider \(\sigma ^{\prime }\) the prefix of \({\sigma _{s}}\) of length \(n+1.\) On the one hand, at time \(t+{{\mathrm{time}}}(\sigma ^{\prime }) - d,\) i.e., when \(t^{\prime }= {{\mathrm{time}}}(\sigma ^{\prime }) - d,\) according to Lemma 4, we have \({{\mathrm{config_{out}}}}(\sigma ,\,t+{{\mathrm{time}}}(\sigma ^{\prime }) - d)= ((\delta ,\,a),\,\sigma _{c},\, s,\,0,\,m_{t},\,q)\) for some \(s,\,m_{t}\in {\mathbb {R}}_{\ge 0}\) and \(\sigma _{c} \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*.\) On the other hand, let us consider some \(t^{\prime }\in [0,\,\delta ],\) we have:

  $$\begin{aligned} \mathcal{E}(\sigma ,\,t,\,t+{{\mathrm{time}}}(\sigma ^{\prime })+t^{\prime }-d)&= \mathcal{E}(\sigma ,\,t,\,t+{{\mathrm{time}}}(\sigma ^{\prime })-d) \cdot \mathcal{E}(\sigma ,\,t+{{\mathrm{time}}}(\sigma ^{\prime })\\&\quad -d,\,t+{{\mathrm{time}}}(\sigma ^{\prime }) + t^{\prime } -d). \end{aligned}$$

  Using the induction hypothesis, we find \(\mathcal{E}(\sigma ,\,t,\,t+{{\mathrm{time}}}(\sigma ^{\prime })-d) = \mathrm {obs}(\sigma ^{\prime },\,{{\mathrm{time}}}(\sigma ^{\prime })) =\sigma ^{\prime }.\) Using the semantics of the EM (dump and idle rules), we obtain \(\mathcal{E}(\sigma ,\,t+{{\mathrm{time}}}(\sigma ^{\prime }) + t^{\prime } -d) = \mathrm {obs}((\delta ,\,a),\, t^{\prime }+d).\) Thus, \(\mathcal{E}(\sigma ,\,t,\,t+{{\mathrm{time}}}(\sigma ^{\prime })+t^{\prime }-d) = \sigma ^{\prime } \cdot \mathrm {obs}((\delta ,\,a),\,t^{\prime }+d) = \mathrm {obs}(\sigma ^{\prime }\cdot (\delta ,\,a),\,t^{\prime }+d).\) \(\square \)

1.5 Proof of Proposition 5: relation between enforcement function and EM

Proof

We shall prove that, given a property \(\varphi ,\) the associated EM as per Definition 9 (p. 18) implements the associated enforcement function \(E_\varphi :\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\) as per Definition 8 (p. 12). That is:

The proof is done by induction on the length of the input timed word \(\sigma .\) \(\square \)

Induction basis. Let us suppose that \(|\sigma |=0,\) thus \(\sigma =\epsilon \) in \(({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}.\) On the one hand, we have \(\forall t\in {\mathbb {R}}_{\ge 0}:\,E_\varphi (\sigma ,\,t)=\epsilon .\) On the other hand, the word \(\mathcal{E}_\mathrm {ioo}(\epsilon ,\,t)\) over the input–operation–output alphabet is such that \(\forall t\in {\mathbb {R}}_{\ge 0}:\,\mathcal{E}_\mathrm {ioo}(\epsilon ,\,t)=\epsilon .\) Thus, according to the definition of the EM, \(\mathrm {store}\)-\(\overline{\varphi }\) and \(\mathrm {store}\)-\(\varphi \) rules cannot be applied. Consequently, the memory of the EM remains empty as in the initial configuration. It follows that the dump rule cannot be applied. We have then \(C_{0}^{{\scriptscriptstyle \mathcal{E}}} \mathop {\hookrightarrow }\limits ^{\epsilon /{{\mathrm{idle}}}(t)/\epsilon } (\epsilon ,\,\epsilon ,\,t,\,t,\, 0,\, q),\) and thus \(\mathcal{E}(\epsilon ,\,t)=\epsilon .\)

Induction step. Let us suppose that \(E_\varphi (\sigma ,\,t)=\mathcal{E}(\sigma ,\,t)\) for any timed word \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\) of some length \(n\in \mathbb {N},\) at any time \(t\in {\mathbb {R}}_{\ge 0}.\) Let us now consider some input timed word \(\sigma \cdot (\delta ,\,a)\) for some \(\sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\) with \(|\sigma |=n,\,\delta \in {\mathbb {R}}_{\ge 0},\) and \(a \in \varSigma .\) We want to prove that \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t)=\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t),\) at any \(t \in {\mathbb {R}}_{\ge 0}.\)

Let us consider some time instant \(t\in {\mathbb {R}}_{\ge 0}.\) We distinguish two cases according to whether \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) > t\) or not, that is whether \(\sigma \cdot (\delta ,\,a)\) is completely observed or not at time t.

• Case \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) > t.\) In this case, \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\sigma ,\,t),\) i.e., at time t, the observations of \(\sigma \) and \(\sigma \cdot (\delta ,\,a)\) are identical. On the one hand, we have: \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t))),\,t) =\mathrm {obs}(\varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma ,\,t))),\,t) = E_\varphi (\sigma ,\,t).\) On the other hand, regarding the EM, since \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\sigma ,\,t),\) using Lemma 2 (p. 35), we obtain \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t) = \mathcal{E}(\sigma ,\,t).\) Using the induction hypothesis, we can conclude that \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t)=\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t).\)

• Case \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) \le t.\) In this case, we have \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,t) = \sigma \cdot (\delta ,\,a)\) [i.e., \(\sigma \cdot (\delta ,\,a)\) has been observed entirely]. Using Lemma 3 (p. 36), we know that the configuration of the EM at time \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))\) is \({{\mathrm{config_{in}}}}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)))=(\sigma _{s},\, \sigma _{c},\,\delta ,\,d,\,m_{t},\,q_{\sigma })\) for some \(\sigma _{s},\, \sigma _{c}\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\,\delta ,\,d,\,m_{t}\in {\mathbb {R}}_{\ge 0},\,q_{\sigma }\in Q.\) Observe that \({{\mathrm{config_{in}}}}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = {{\mathrm{config_{in}}}}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)))\) because of (i) the definition of \({{\mathrm{config_{in}}}}\) using the definition of \(\mathcal{E}_\mathrm {ioo}\) and (ii) the event \((\delta ,\,a)\) has not been yet consumed through none of the store rules by the EM at time \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)).\) We distinguish two cases according to whether \(\sigma _{c}\cdot (\delta ,\,a)\) can be delayed into a word satisfying \(\varphi \) or not, i.e., whether \(K = \kappa _{\varphi }({{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a))=\emptyset ,\) or not.

  • Case \(K =\kappa _{\varphi }({{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a))=\emptyset .\) From the definition of \({{\mathrm{store}}}\) function, we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = (\sigma _{s},\, \sigma _{c}\cdot (\delta ,\,a)),\) and \(\varPi _{1}({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a))) = \sigma _{s}.\) We also have \(\varPi _{1}({{\mathrm{store}}}(\sigma )) = \sigma _{s}.\) From the definition of \(E_\varphi ,\) we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\, t) = E_\varphi (\sigma ,\,t).\) Now, regarding \(\mathcal{E},\) according to the definition of \(\mathrm {update},\) we have \(\mathrm {update}(q_{\sigma },\,\sigma _{c}\cdot (\delta ,\,a),\,m_{t}+\delta ) = (\sigma _{c},\,\mathtt {ff}).\) According to the definition of the transition relation, we have:

    $$\begin{aligned} \left( \sigma _{s},\,\sigma _{c},\,\delta ,\,d,\,m_{t},\,q_{\sigma }\right) \mathop {\hookrightarrow }\limits ^{(\delta ,a)/\mathrm {store}{\text {-}} \overline{\varphi }(\delta ,\,a)/\epsilon }\left( \sigma _{s},\, \sigma _{c}\cdot (\delta ,\,a),\,0,\,d,\,m_{t}+\delta ,\,q_{\sigma }\right) . \end{aligned}$$

    Thus \({{\mathrm{config_{out}}}}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) = (\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a),\,0,\,d,\,m_{t}+\delta ,\,q_{\sigma }).\) Let us consider \(t_{\epsilon }\in {\mathbb {R}}_{\ge 0}\) such that between \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))-t_{\epsilon }\) and \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\) the EM does not read any input nor produce any output, i.e., for all \(t\in [{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\, {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))],\,{{\mathrm{config}}}(t)\) is such that only the idle rule applies. Let us examine \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t).\) We have:

    $$\begin{aligned} \begin{array}{ll} \mathcal{E}(\sigma \cdot (\delta ,\,a),\,t) = &{}\mathcal{E}\left( \sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }\right) \\ &{}\cdot \mathcal{E}\left( \sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))\right) \\ &{}\cdot \mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t). \end{array} \end{aligned}$$

    Let us examine \(\mathcal{E}(\sigma ,\,t).\) We have:

    $$\begin{aligned} \begin{array}{ll} \mathcal{E}(\sigma ,\,t) &{}=\mathcal{E}\left( \sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }\right) \\ &{}\quad \cdot \mathcal{E}\left( \sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))\right) \\ &{}\quad \cdot \mathcal{E}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t). \end{array} \end{aligned}$$

    Observe that \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }) = \mathcal{E}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon })\) because \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }) = \sigma \) according to the definition of \(\mathrm {obs}.\) Moreover, \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = \epsilon \) since only the idle rule applies during the considered time interval. Furthermore, according to Lemma 5, since \({{\mathrm{config_{out}}}}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a),\,0,\,d,\,m_{t}+\delta ,\,q_{\sigma }),\) we get \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t) = \mathrm {obs}(\sigma _{s},\,t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d) = \mathrm {obs}(\sigma _{s},\,t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d).\) Moreover, we know that \({{\mathrm{config_{in}}}}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _{s},\, \sigma _{c},\,\delta ,\,d,\,m_{t},\,q_\sigma ).\) Since the EM is deterministic, and from Remark 12 (p. 34), we also get that \({{\mathrm{config_{out}}}}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _{s},\, \sigma _{c},\,\delta ,\,d,\,m_{t},\,q_\sigma ).\) Using Lemma  5 (p. 36) again, we get \(\mathcal{E}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t) = \mathrm {obs}(\sigma _{s},\,t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d).\) Consequently we can deduce that \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t) = \mathcal{E}(\sigma ,\,t) = E_\varphi (\sigma ,\,t) = E_\varphi (\sigma \cdot (\delta ,\,a)).\)

  • Case \(K =\kappa _{\varphi }({{\mathrm{time}}}(\sigma )+\delta ,\,\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a))\ne \emptyset .\) Regarding \(E_\varphi ,\) from the definition of \({{\mathrm{store}}}\) function, we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = ((\sigma _{s}\cdot {{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex}, time}K,\,\epsilon ),\) and \(\varPi _{1}({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _{s}\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K).\) Regarding the EM, according to the definition of \(\mathrm {update},\) we have \(\mathrm {update}(q_{\sigma },\, \sigma _{c}\cdot (\delta ,\,a),\,m_{t}+\delta ) = (\sigma ^{'}_{c},\,\mathtt {tt}).\) From the definition of the transition relation, we have:

    $$\begin{aligned} \left( \sigma _{s},\,\sigma _{c},\,\delta ,\,d,\,m_{t},\,q_\sigma \right) \mathop {\hookrightarrow }\limits ^{(\delta ,a)/\mathrm {store}{\text {-}}{\varphi }(\delta ,\,a)/\epsilon }\left( \sigma _{s}\cdot \sigma ^{'}_{c},\, \epsilon ,\,0,\,d,\,m^{'}_{t},\,q^{'}\right) , \end{aligned}$$

    where:

    • \(m^{'}_{t} = m^{'}_{t} + \delta - {{\mathrm{time}}}(\sigma ^{'}_{c}),\)

    • \(q^{'}\) is defined as \(q\mathop {\rightarrow }\limits ^{\sigma ^{'}_{c}}q^{'}.\)

    Thus \({{\mathrm{config_{out}}}}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) = (\sigma _{s}\cdot \sigma ^{'}_{c},\,\epsilon ,\,0,\,d,\,m^{'}_{t},\,q^{'}).\) Let us consider \(t_{\epsilon }\) such that during \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))-t_{\epsilon }\) and \({{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\) the EM does not read any input nor produce any output, i.e., for all \(t\in [{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\, {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))],\,{{\mathrm{config}}}(t)\) is such that only the idle rule applies. Let us examine \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t).\) We have:

    $$\begin{aligned} \begin{array}{ll} \mathcal{E}(\sigma \cdot (\delta ,\,a),\,t) = &{}\mathcal{E}\left( \sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }\right) \\ &{}\cdot \mathcal{E}\left( \sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))\right) \\ &{}\cdot \mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t). \end{array} \end{aligned}$$

    Let us examine \(\mathcal{E}(\sigma ,\,t).\) We have:

    $$\begin{aligned} \begin{array}{ll} \mathcal{E}(\sigma ,\,t) &{}=\mathcal{E}\left( \sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }\right) \\ &{}\quad \cdot \mathcal{E}\left( \sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))\right) \\ &{}\quad \cdot \mathcal{E}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t). \end{array} \end{aligned}$$

    Observe that \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }) = \mathcal{E}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon })\) because \(\mathrm {obs}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)) - t_{\epsilon }) = \sigma \) according to the definition of \(\mathrm {obs}.\) Moreover, \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))- t_{\epsilon },\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = \epsilon \) since only the idle rule applies during the considered time interval. Furthermore, according to Lemma 5, since \({{\mathrm{config_{out}}}}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))) = (\sigma _{s}\cdot \sigma ^{'}_{c},\,\epsilon ,\,0,\,d,\,m^{'}_{t},\,q^{'}), \) we get \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t) = \mathrm {obs}(\sigma _{s}\cdot \sigma ^{'}_{c},\,t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d).\) Now we further distinguish two more sub-cases, based on whether \({{\mathrm{time}}}(\sigma _{s}\cdot \sigma ^{'}_{c}) > t- {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d\) or not (whether all the elements in the memory can be released as output by time t or not).

    • Case \({{\mathrm{time}}}(\sigma _{s}\cdot \sigma ^{'}_{c}) > t- {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d.\) We further distinguish two more sub-cases based on whether \({{\mathrm{time}}}(\sigma _{s}) > t- {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d,\) or not.

      • Case \({{\mathrm{time}}}(\sigma _{s}) > t- {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d.\) In this case, we know that \(\mathrm {obs}(\sigma _{s}\cdot \sigma ^{'}_{c},\,t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d) = \mathrm {obs}(\sigma _{s},\, t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d).\) Hence, we can derive that \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,t) = \mathcal{E}(\sigma ,\,t).\) Also, from the induction hypothesis, we know that \(\mathcal{E}(\sigma ,\,t) = E_\varphi (\sigma ,\,t).\) Regarding \(E_\varphi ,\) we have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = \varPi _{1}({{\mathrm{store}}}(\sigma ))\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K.\) Moreover

        $$\begin{aligned} \begin{array}{rl} E_\varphi (\sigma \cdot (\delta ,\,a),\,t) &{}= \mathrm {obs}\left( \varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma ,\,t))),\,t\right) \\ &{}= \mathrm {obs}\left( \varPi _{1}({{\mathrm{store}}}(\sigma ))\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\,t\right) . \end{array} \end{aligned}$$

        We can have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \varPi _{1}({{\mathrm{store}}}(\sigma )) \cdot O\) where \(O \preccurlyeq {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K\) which is equal to \(E_\varphi (\sigma ,\,t)\cdot O,\) only if the delays computed by the \(\mathrm {update}\) function are different from the delays computed by \(E_\varphi .\) This would violate the induction hypothesis stating that \(\mathcal{E}(\sigma ,\,t) = E_\varphi (\sigma ,\,t).\) Hence, we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}(\ \varPi _{1}({{\mathrm{store}}}(\sigma )),\,t) = E_\varphi (\sigma ,\,t).\) Thus, \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathcal{E}(\sigma \cdot (\delta ,\,a),\,t).\)

      • Case \({{\mathrm{time}}}(\sigma _{s}) \le t- {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d.\) In this case, we can follow the same reasoning as in the previous case to obtain the expected result.

    • Case \({{\mathrm{time}}}(\sigma _{s}\cdot \sigma ^{'}_{c}) \le t- {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a))+d.\) In this case, similarly following Lemma 5 (p. 36), we have \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t) = \mathrm {obs}(\sigma _{s}\cdot \sigma ^{'}_{c},\,t - {{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)+d) = \sigma _{s}\cdot \sigma ^{'}_{c}.\) We can also derive that \(\mathcal{E}(\sigma ,\,{{\mathrm{time}}}(\sigma \cdot (\delta ,\,a)),\,t) = \sigma _{s}.\) Consequently, we have \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\, t) = \mathcal{E}(\sigma ,\,t) \cdot \sigma ^{'}_{c}.\) From the induction hypothesis, we know that \( E_\varphi (\sigma ,\,t) = \mathcal{E}(\sigma ,\,t),\) and we have \(\mathcal{E}(\sigma \cdot (\delta ,\,a),\, t) = E_\varphi (\sigma ,\,t)\cdot \sigma ^{'}_{c}.\) We have \({{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) = \varPi _{1}({{\mathrm{store}}}(\sigma )) \cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}} K,\) and thus \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathrm {obs}( \varPi _{1}({{\mathrm{store}}}( \sigma )) \cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}} K ,\,t).\) Hence, in this case, we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = {{\mathrm{store}}}(\sigma )\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K = E_\varphi (\sigma ,\,t)\cdot {{{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}}K,\) since the delays computed for the subsequence \(\sigma _{c}\cdot (\delta ,\,a)\) by \(E_\varphi \) and \(\mathcal{E}\) are equal. Finally, we have \(E_\varphi (\sigma \cdot (\delta ,\,a),\,t) = \mathcal{E}(\sigma \cdot (\delta ,\,a),\,t).\)

Implementation of store processes

We provide a brief description related to how the store process, which processes the input events (checking for the satisfaction of the property and computing delays) is implemented.

1.1 Implementation of \({\mathsf {StoreProcess_{safety}}}\)

We now describe the implementation of \({\mathsf {StoreProcess_{safety}}}\) used by an EM for safety properties. The \({\mathsf {StoreProcess_{safety}}}\) first parses the input model, and performs the necessary initialization. For each event of the trace in order, first the automaton representing the input trace is updated with the new event. Then the \(\mathrm {update_s}\) function is invoked, with the current state information and the event. The \(\mathrm {update_s}\) function returns \(\mathtt {ff}\) if an accepting state is not reachable upon the event \((\delta ,\,a)\) from the current state. In case if an accepting state is reachable, then the \(\mathrm {update_s}\) function returns the optimal delay with information about the state that is reachable. Before continuing with the next event, the \({\mathsf {StoreProcess}}\) updates the current state information. In the \({\mathsf {StoreProcess_{safety}}},\) the execution time of \(\mathrm {update_s}\) is measured. The \({\mathsf {StoreProcess_{safety}}}\) keeps track of the total time of \(\mathrm {update_s}\), by adding the \(\mathrm {update_s}\) time measured after each event to the total time, which is returned as a result of invoking the \({\mathsf {StoreProcess_{safety}}}.\)

1.2 Implementation of \({\mathsf {StoreProcess_{co-safety}}}\)

The \({\mathsf {StoreProcess_{co-safety}}}\) is implemented following the algorithm and steps described in [16]. Below we provide an abstract description of the code implementing the \(\mathrm {update_{cs}}\) function. The \(\mathrm {update_{cs}}\) function takes a timed word (the events read by the EM), and returns a new delay for each input event, if an accepting state is reachable for the given input timed word. First, all paths starting from the initial state for the given input sequence are computed. Then the set of all accepting paths is computed. In each path, if the location in the last state is accepting, then the path is accepting, and is a non-accepting path otherwise. If the set of accepting paths is empty, then \(\mathrm {update_{cs}}\) returns \(\mathtt {ff}.\) If there are accepting paths, for each state in the path, a corresponding delay is computed, and the paths whose sums of delays are minimal are filtered. Among these paths, one path is chosen according to the lexical order, and the delays corresponding to this path are returned as the result.

Reprints and permissions