Runtime enforcement of timed properties revisited

Abstract

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 Introduction

Runtime verification [1–6] refers to the theories, techniques, and tools aiming at checking the conformance of the executions of systems under scrutiny w.r.t. some desired property. Runtime enforcement [7–10] extends runtime verification and refers to the theories, techniques, and tools aiming at ensuring the conformance of the executions of systems under scrutiny w.r.t. some desired property. The first step of monitoring approaches consists in instrumenting the underlying system so as to partially observe the events or the parts of its global state that may influence the property under scrutiny. A central concept is the verification or enforcement monitor (EM) that is generally synthesized from the property expressed in a high-level formalism. Then, the monitor can operate either online by receiving events in a lock-step manner with the execution of the system or offline by reading a log/sequence of system events/actions. When the monitor is only dedicated to verification, it is a decision procedure emitting verdicts stating the correctness of the (partial) observed trace generated from the system execution. When the monitor additionally has enforcement abilities, it corrects any incorrect execution to meet a desirable behavior (and leaves correct executions unchanged).

Three categories of runtime verification frameworks can be distinguished according to the formalism used to express the input property. In propositional approaches, properties refer to events taken from a finite set of propositional names. For instance, a propositional property may rule the ordering of function calls in a program. Monitoring such kind of properties has received a lot of attention. Parametric approaches have received a growing interest in the last 5 years. In this case, events in the property are augmented with formal parameters, instantiated at runtime. In timed approaches, the observed time between events may influence the truth-value of the property. It turns out that monitoring of timed properties (where time is continuous) is a much harder problem because of (at least) two reasons. First, modeling timed requirements requires a more complex formalism involving time as a continuous parameter. Second, when monitoring a timed property, the problem that arises is that the overhead induced by the monitor (i.e., the time spent executing the monitoring code) influences the truth-value of the monitored property. Consequently, without assumptions and limitations on the computation performed by monitors (see § Context and Objectives), not much information can be gained from the verdicts produced by the monitor. Few attempts have been made on monitoring systems w.r.t. timed properties (see Sect. 5 for a detailed comparison with related work). Roughly speaking, two lines of work can be distinguished: synthesis of automata-based decision procedures for timed formalisms (e.g., [1, 3–5]), and, tools for runtime verification of timed properties [11, 12].

In runtime enforcement, an EM is used to transform some (possibly) incorrect execution sequence into a correct sequence w.r.t. the property of interest. In the propositional case, the transformation performed by an EM should be sound and transparent. Soundness means that the resulting sequence obeys the property. Transparency historically means that, the monitor should modify the input sequence in a minimal way (meaning that the input sequence should not be modified if it already conforms to the property). According to how a monitor is allowed to modify the input sequence (i.e., the primitives afforded to the monitor), several models of EMs have been proposed [7–10]. In a nutshell, an EM can definitely block the input sequence (as done by security automata [7]), suppress an event from the input sequence (as done by suppression automata [8]), insert an event to the input sequence (as done by insertion automata [8]), or perform any of these primitives (as is the case with edit-automata [8] or so-called generalized EMs [10]). Moreover, according to how transparency is effectively formalized, several definitions of runtime enforcement have been proposed (see [9] for an overview). The notion of time has been considered in previous runtime enforcement approaches such as in [13] for discrete-time properties, and in [14] which considers elapsing of time as a series of uncontrollable events (“ticks”).

Context and objectives. The general context is depicted in Fig.  1. We focus on online enforcement of timed properties. More specifically, given a timed property $\varphi ,$ we synthesize an enforcement mechanism that operates at runtime. To be as general as possible, an enforcement mechanism is supposed to be placed between an event emitter and an event receiver. The emitter and receiver execute asynchronously. Note, this abstract architecture is generic and can be instantiated to many concrete ones where the emitter and receiver are considered to be e.g., a program or the environment. In all cases, we assume that delaying an event from the emitter does not effect its subsequent events. This assumption is reasonable in many practical application scenarios with architectures compatible with the one described above.

Fig. 1

Enforcement mechanism

An enforcement mechanism inputs a sequence of timed event $\sigma$ and transforms it into a sequence of timed events o. No constraint is required on $\sigma ,$ whereas the enforcement mechanism ensures that o is correct w.r.t. property $\varphi .$ Satisfaction of property $\varphi$ by the output sequence is considered at the output of the enforcement mechanism and not at the input of the event receiver: we assume a reliable, without delay, and safe communication between the emitter and receiver. As usual in runtime enforcement, we do not consider any security, communication, nor reliability issue with events. The considered enforcement mechanisms are time retardants, i.e., their main enforcement primitive consists in delaying the received events. Contrary to edit-automata, enforcement mechanisms, as considered in this paper, are not able to generate nor suppress events because of (i) inducing more costly computations in a timed context, and (ii) delaying events is already sufficient in many application domains. Since time between events matters, we assume the enforcement mechanism to be infinitely faster than the emitter and receiver. In other words, the computation time of the enforcement mechanism is negligible: at runtime, the computation performed by the enforcement mechanism is done in zero-time.¹ Moreover, we assume that delaying the events of the emitter does not influence its behavior.

To sum up, given some timed property $\varphi$ and an input timed word $\sigma ,$ we aim to study mechanisms that input $\sigma$ and output a sequence o that (i) satisfies $\varphi$ (soundness of the mechanism), (ii) has the same order of events as $\sigma$ with possibly increased delays (transparency of the mechanism), and (iii) is released as fast as possible (optimality of the mechanism).²

Motivations. To the best of our knowledge, no approach focusing on enforcement of timed properties has been proposed. Motivations for extending runtime enforcement to timed properties abound. First, timed properties are more precise to specify desired behaviors of systems since they allow to explicitly state how time should elapse between events. Thus, timed properties/specifications can be particularly useful in some application domains [15]. For instance, in the context of security monitoring, EMs can be used as firewalls to prevent denial of service attacks by ensuring a minimal delay between input events (carrying some request for a protected server). On a network, EMs can be used to synchronize streams of events together, or, ensuring that a stream of events conforms to the pre-conditions of some service.

The following requirements could specify the expected behavior of a server:

$R_{1}$ :

“There should be a delay of at least 5 time units between any two user requests (r)”.

$R_{2}$ :

“The user should perform a successful authentication, that is, he should send a request (r) and receive a grant (g) between 10 and 15 time units”.

$R_{3}$ :

“Resource grants (g) and releases (r) should alternate, starting with a grant, and every grant should be released within 15 to 20 time units”.

$R_{4}$ :

“Every 10 time units, there should be a request for a resource followed by a grant. The request should occur within 5 time units”.

$R_{1}$ (resp. $R_{2}$) can be formalized as a safety (resp. co-safety) property. Safety (resp. co-safety) properties express that “something bad should never happen” (resp. “something good should happen within a finite amount of time”). Moreover, in the space of regular properties (over timed words), many interesting properties of systems are neither safety nor co-safety properties that typically specify some form of transactional behavior. Such behaviors are illustrated by requirements $R_{3}$ and $R_{4}.$ In this paper, we propose to synthesize enforcement mechanisms for all regular timed properties.

Some motivating examples illustrating enforcement mechanisms. Let us consider again requirements $R_{1}$ and $R_{3}.$ In Sect.  2 we will describe how to formalize these requirements as properties defined by timed automata. Before going further into the formal definitions, we briefly describe how an enforcement mechanism corrects an input sequence to satisfy a property. To enforce the properties, the enforcement mechanism is placed at the input of the server and operates on command-messages that it receives (destinated to the server). The enforcement mechanism releases the (correct sequence of) command-messages into the server input. In the following discussion of the examples, t denotes the current instant of time, i.e., the total time since the beginning of the considered sequence.

Let us consider requirement $R_{1}.$ Let r and a be the possible actions where r denotes request of a resource. We now illustrate how an enforcement mechanism corrects the input sequence $\sigma =(1,\,a)\cdot (3,\,r)\cdot (1,\,r)$ (where each event is associated with a delay, indicating the time elapsed after the previous event or the system initialization for the first event). The monitor receives the first action a at $t=1.$ Since, the safety requirement is not violated, the monitor outputs it immediately (the mechanism is sound and optimal as it output a correct sequence which is delayed in a minimal way). The second action r is received by the monitor at $t=4,$ and the monitor outputs it immediately. The last action r, is received at $t=5.$ If the action is output immediately, then the safety requirement would be violated (since only 1 time unit has elapsed after the monitor output the previous r action), and thus the mechanism would not be sound anymore. Thus, to satisfy $R_{1},$ the monitor outputs the last r action at $t=9,$ introducing a delay of 4 time units (which is the minimal required delay as per optimality requires). The output of the monitor is $(1,\,a)\cdot (3,\,r)\cdot (5,\,r).$ Note that the order of actions is preserved, only the delays between them have been possibly augmented.

Let us now consider requirement $R_{3}.$ Recall that g and r are the actions denoting the grant and release of the resource, respectively. We illustrate how an EM corrects the input sequence $\sigma = (3,\,g)\cdot (10,\,r)\cdot (3,\,g)\cdot (5,\,g).$ The monitor receives the first action g at $t=3,$ the second action r at $t=13,$ etc. The monitor cannot output the first received action g because the event alone does not satisfy the requirement (and the monitor does not know yet the next events). If the next event is r, then it can output the events g followed by r, if it can choose good delays for both the events satisfying the timing constraints. At $t=13,$ the monitor can decide that the first two events can be released as output. Hence in output, the delay associated with the first g is 13 t.u. If the monitor should choose the same delay for the second action r, then the property cannot be satisfied. The monitor chooses a delay of 15 t.u. which is the minimal delay satisfying the constraint that is greater than the corresponding delay in the input sequence. When the monitor observes the second g at $t=16,$ it releases it as output, and again waits for the next event. Since the next input event observed at $t=21$ is not r, the sequence violates the property and cannot be corrected by the monitor. Hence, after $t=21,$ the output of the monitor remains $(13,\,g)\cdot (15,\,r).$

Contributions. We introduce runtime enforcement of timed properties. For this purpose, we adapt soundness and transparency to a timed context. We show how to synthesize runtime enforcement mechanisms for any regular property defined by a timed automaton. In contrast with previous runtime enforcement approaches [7, 8, 10], our mechanisms only have the primitive of being able to delay input events so that the output sequence conforms to the property. To ease the design and implementation of EMs, we describe them at several abstraction levels: the notion of enforcement function describes the behavior of an enforcement mechanism at an abstract level as an input–output relation between timed words. An EM implements an enforcement function and describes the behavior of an enforcement mechanism in an operational way as a rule-based transition system. Enforcement algorithms describe the implementation of EMs and serve to guide the concrete implementation of enforcement mechanisms. The difficulty that arises when considering regular properties is that the aforementioned enforcement mechanisms should consider input (corrected) sequences of events that alternate between satisfying and not satisfying the underlying property. Experiments have been performed on prototype monitors to show their effectiveness and the feasibility of our approach.

This paper combines and extends the results of the two papers [16, 17]. More specifically, this paper provides the following additional contributions:

• to propose a more complete and revised theoretical framework for runtime enforcement of timed properties: we have re-visited the notations, unified and simplified the main definitions;

• to propose a completely new implementation of our EMs that (i) offers better performance (compared to the ones in [16]), and (ii) are now loosely-coupled to UPPAAL;

• to synthesize and evaluate EMs for more properties on longer executions;

• to include correctness proofs of the proposed mechanisms.

Importantly, while our synthesis techniques yield sound, transparent, and optimal enforcement mechanisms for all regular properties, some input execution sequences, while being correct, are not producible by our enforcement mechanisms. Indeed, we exhibit a notion of what we refer to as non-enforceable properties, for which physical time constraints prevent the associated enforcement mechanisms from preserving correct sequences. Intuitively, such undesired situation occurs when enforcing for instance co-safety properties: while the enforcement mechanism reads a correct input sequence, at the moment when it receives the event that allows it to determine that the sequence is correct, it is not possible anymore to release the first read event because the delay of the first event is now greater than the maximal value allowed by the guard on the corresponding transition in the underlying timed automaton. As we shall see, requirement $R_{4}$ can be formalized as a so-called non-enforceable timed property (Remark 3).

Paper organization. Section 2 introduces preliminaries and notation and also explains how properties are defined as timed automata on some examples. Section 3 details the enforcement mechanisms (enforcement function, monitor, and algorithm). Our prototype implementations of monitors and experiments are presented in Sect. 4. Section 5 discusses related work. Finally, conclusions and open perspectives are drawn in Sect. 6. To facilitate the reading of this paper, after each proposition we propose a sketch of proof. Full versions of the proofs along with some further notation required for the proofs are available in Appendix 1.

2 Preliminaries and notation

2.1 Untimed notions

$\mathbb {N}$ denotes the set of non-negative integers. An alphabet is a set of elements. A (finite) word over an alphabet A is a finite sequence of elements of A. The length of a word $\sigma$ is denoted as $|\sigma |.$ The empty word over A is denoted by $\epsilon _{A}$ or $\epsilon$ when clear from the context. The set of all (respectively non-empty) finite words over A is denoted by $A^{*}$ (respectively $A^{+}$). A language over A is a set $\mathcal{L}\subseteq A^{*}.$ The concatenation of two words $\sigma$ and $\sigma ^{\prime }$ is denoted by $\sigma \cdot \sigma ^{\prime }.$ The empty word over A is neutral for concatenation of words of A: $\forall \sigma \in A^{*}:\,\sigma \cdot \epsilon _{A} \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\epsilon _{A} \cdot \sigma \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\sigma .$ A word $\sigma ^{\prime }$ is a prefix of a word $\sigma ,$ denoted as $\sigma ^{\prime } \preccurlyeq \sigma ,$ whenever there exists a word $\sigma ^{\prime \prime }$ such that $\sigma = \sigma ^{\prime }\cdot \sigma ^{\prime \prime },$ and $\sigma ^{\prime }$ is a strict prefix of $\sigma$ denoted as $\sigma ^{\prime } \prec \sigma$ whenever $\sigma ^{\prime } \preccurlyeq \sigma \wedge |\sigma ^{\prime }|<|\sigma |.$ For a word $\sigma$ and $1\le i \le |\sigma |,$ the i-th letter (resp. prefix of length i, suffix starting at position i) of $\sigma$ is denoted $\sigma (i)$ (respectively $\sigma _{[\cdots i]},$ $\sigma _{[i\cdots ]}$)—with the convention $\sigma _{[\cdots 0]}\mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\epsilon$. Given a word $\sigma$ and two integers $i,\,j,$ such that $i \le j$ and $|\sigma | \ge j,$ the sub-word from index i to j is defined as $\sigma _{[i\cdots j]} \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\sigma _{[\cdots j][i \cdots ]}.$ Given a word $\sigma ,$ the last letter, $\sigma (|\sigma |),$ is denoted ${{\mathrm{last}}}(\sigma ).$ The set ${{\mathrm{pref}}}(\sigma )$ denotes the set of prefixes of $\sigma$ and by extension, ${{\mathrm{pref}}}(\mathcal{L})\mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\{{{\mathrm{pref}}}(\sigma )\ |\ \sigma \in \mathcal{L}\}$ is the set of prefixes of words in $\mathcal{L}.$ A language $\mathcal{L}$ is said to be prefix-closed whenever ${{\mathrm{pref}}}(\mathcal{L})=\mathcal{L}$ and extension-closed whenever $\mathcal{L}=\mathcal{L}\cdot A^{*}.$ Given an n-tuple of symbols $e=(e_{1},\ldots , e_{n}),\,\varPi _{i}(e)$ is the projection of e on its ith element ($\varPi _{i}(e)\mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}e_{i}$). The projection function is extended to sequences of tuples in the standard way.

2.2 Timed languages and properties as timed automata

Let ${\mathbb {R}}_{\ge 0}$ denote the set of non-negative real numbers, and $\varSigma$ a finite alphabet of actions. A pair $(\delta ,\,a) \in ({\mathbb {R}}_{\ge 0}\times \varSigma )$ is called an event. We note ${{\mathrm{delay}}}(\delta ,\,a)\mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\delta$ and ${{\mathrm{act}}}(\delta ,\,a)=a$ the projections of events on delays and actions, respectively. A timed word over $\varSigma$ is a finite sequence of events ranging over $({\mathbb {R}}_{\ge 0}\times \Sigma )^*.$ A timed language is any set $\mathcal{L}\subseteq ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}.$ We consider a timed word $\sigma = (\delta _{1},\,a_{1})\cdot (\delta _{2},\,a_{2})\cdots (\delta _{n},\,a_{n}).$ For $i\in [2,\,n],\,\delta _{i}$ is the delay between $a_{i-1}$ and $a_{i},$ and, $\delta _{1}$ the time elapsed before the first action $a_{1}.$ Note that even though the alphabet $({\mathbb {R}}_{\ge 0}\times \varSigma )$ is infinite in this case, previous notions and notations defined above (related to length, concatenation, prefix, etc.) naturally extend to timed words. The untimed projection of $\sigma$ is $\varPi _{\varSigma }(\sigma ) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}a_{1}\cdot a_{2}\cdots a_{n}$ in $\varSigma ^{*}$ (i.e., delays are ignored). The duration of a timed word $\sigma ,$ denoted by ${{\mathrm{time}}}(\sigma )\mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\varSigma _{i=1}^{n}\delta _{i},$ is the sum of its delays.

Timed automata. A timed automaton [18] is a finite automaton extended with a finite set of real valued clocks. Let $X=\{x_{1},\ldots , x_{k}\}$ be a finite set of clocks. A clock valuation for X is a function $\nu$ from X to $\mathbb {R}_{\ge 0}.$ $\mathbb {R}^{X}_{\ge 0}$ denotes the valuations of clocks in X. For $\nu \in \mathbb {R}^{X}_{\ge 0}$ and $\delta \in {\mathbb {R}}_{\ge 0},\,\nu +\delta$ is the valuation assigning $\nu (x)+\delta$ to each clock x of X. Given a set of clocks $X^{\prime } \subseteq X,\,\nu [X^{\prime } \leftarrow 0]$ is the clock valuation $\nu$ where all clocks in $X^{\prime }$ are assigned to $0.$

$\mathcal{G}(X)$ denotes the set of clock constraints defined as Boolean combinations of simple constraints of the form $x \bowtie c$ with $x \in X,$ $c\in \mathbb {N}$ and $\bowtie \in \{<,\,\le ,\,=,\,\ge ,\,>\}.$ Given $g \in \mathcal{G}(X)$ and $\nu \in {\mathbb {R}}_{\ge 0}^{X},$ we write $\nu \models g$ when g holds according to $\nu .$

Definition 1

(Timed automata) A timed automaton (TA) is a tuple $\mathcal{A}\!=\!(L, l_{0},\,X,\varSigma ,\,\varDelta ,\,G),$ such that L is a finite set of locations with $l_{0} \in L$ the initial location, X is a finite set of clocks, $\varSigma$ is a finite set of actions, $\varDelta \subseteq L \times \mathcal {G}(X) \times \varSigma \times 2^{X} \times L$ is the transition relation. $G\subseteq L$ is a set of accepting locations.

The semantics of a TA is a timed transition system $[\![\mathcal{A}]\!]=(Q,\,q_{0},\,\varGamma ,\,\rightarrow ,\,F_{G})$ where $Q= L \times {\mathbb {R}}_{\ge 0}^{X}$ is the (infinite) set of states, $q_{0}=(l_{0},\,\nu _{0})$ is the initial state where $\nu _{0}$ is the valuation that maps every clock in X to $0,\,F_{G}= G \times {\mathbb {R}}_{\ge 0}^{X}$ is the set of accepting states, $\varGamma = {\mathbb {R}}_{\ge 0}\times \varSigma$ is the set of transition labels, i.e., pairs composed of a delay and an action. The transition relation $\rightarrow \subseteq Q\times \varGamma \times Q$ is a set of transitions of the form $(l,\,\nu )\!\!\xrightarrow {(\delta ,\,a)}\!\!(l^{\prime },\,\nu ^{\prime })$ with $\nu ^{\prime }=(\nu +\delta )[Y \leftarrow 0]$ whenever there exists $(l,\, g,\,a,\,Y,\,l^{\prime }) \in \varDelta$ such that $\nu +\delta \models g$ for $\delta \in {\mathbb {R}}_{\ge 0}.$

In the following, we consider a timed automaton $\mathcal{A}= (L,\,l_{0},\,X,\, \varSigma ,\,\varDelta ,\,G)$ with its semantics $[\![\mathcal{A}]\!].$ $\mathcal{A}$ is deterministic whenever for any two distinct transitions $(l,\,g_{1},\,a,\,Y_{1},\,l^{\prime }_{1})$ and $(l,\,g_{2},\,a,\,Y_{2},\,l^{\prime }_{2})$ in $\varDelta ,\,g_{1}\wedge g_{2}$ is unsatisfiable. $\mathcal{A}$ is complete whenever for any location $l\in L$ and any action $a\in \varSigma ,$ the disjunction of the guards of the transitions leaving l and labeled by a evaluates to true (i.e., it holds according to any valuation). In the remainder of this paper, we shall consider only deterministic timed automata, and, automata refer to timed automata.

Remark 1

(Completeness and determinism) In this paper, we restrict the presentation to deterministic TAs. However, results also hold for non-deterministic TAs, with slight adaptations required to the vocabulary and when synthesizing an EM. Regarding completeness, if no transition can be triggered upon the reception of an event, a TA implicitly moves to a non-accepting trap state (i.e., a state with no successor).

A run $\rho$ from $q\in Q$ is a sequence of moves in $[\![\mathcal{A}]\!]:\,\rho = q \xrightarrow {(\delta _{1},\,a_{1})} q_{1} \cdots q_{n-1}\xrightarrow {(\delta _{n},\,a_{n})} q_{n},$ for some $n\in \mathbb {N}.$ The set of runs from $q_{0}\in Q$ is denoted ${{\mathrm{Run}}}(\mathcal{A})$ and ${{\mathrm{Run}}}_{F_{G}}(\mathcal{A})$ denotes the subset of runs accepted by $\mathcal{A},$ i.e., when $q_{n}\in F_{G}.$ The trace of a run $\rho$ is the timed word $(\delta _{1},\,a_{1})\cdot (\delta _{2},\,a_{2})\cdots (\delta _{n},\,a_{n}).$ We note $\mathcal{L}({\mathcal{A}})$ the set of traces of ${{\mathrm{Run}}}(\mathcal{A}).$ We extend this notation to $\mathcal{L}_{F_G}(\mathcal{A})$ in a natural way.

Regular, safety, and co-safety timed properties. In the sequel, we shall be interested in the set of regular timed properties, i.e., the timed properties that can be defined by a TA. Within the set of regular timed properties, we are interested in safety and co-safety properties. Informally, safety (resp. co-safety) properties state that “nothing bad should ever happen” (resp. “something good should happen within a finite amount of time”). In this paper, the classes are characterized as follows:

Definition 2

(Regular, safety, and co-safety properties)

• Regular properties are the properties that can be defined by languages accepted by a TA.

• Safety properties (a subset of regular properties) are the non-empty prefix-closed timed languages (i.e., the languages $\mathcal{L}$ s.t. ${{\mathrm{pref}}}(\mathcal{L})=\mathcal{L}$), that can be defined by a TA.

• Co-safety properties (a subset of regular properties) are the non-universal extension-closed timed languages (i.e., the languages $\mathcal{L}$ s.t. $\mathcal{L}=\mathcal{L}\cdot A^{*}$), that can be defined by a TA.

Remark 2

Usually, safety properties are defined as prefix-closed languages, and co-safety as extension-closed languages. With the usual definitions, the two properties $\emptyset$ and $({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}$ (the empty and universal properties, respectively vacuously and universally satisfied) are both, at the same time safety and co-safety properties, and are the only ones in the intersection. In this paper, to simplify the presentation and to avoid pathological cases, we separate the two classes, by considering that $({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}$ is a safety (but not a co-safety) property, and $\emptyset$ is a co-safety (but not a safety) property.

Safety and co-safety timed automata. In the sequel, we shall only consider the properties that can be defined by a deterministic timed automaton (Definition 1). Note that some of these properties can be defined using a timed temporal logic such as a subclass of MTL, which can be transformed into timed automata using the technique described in [3, 19].

We now define how to determine whether a regular property defined by a TA defines a safety or a co-safety property by examining its transition relation.

Definition 3

(Safety and co-safety TA) A complete and deterministic TA $(L,\,l_{0},\,X,\,\varSigma ,\,\varDelta ,\,G),$ where $G\subseteq L$ is the set of accepting locations, is said to be:

• a safety TA if $l_{0} \in G \wedge \not \exists (l,\,g,\,a,\,Y,\,l^{\prime })\in \varDelta :\, l\in L\setminus G$ $\wedge$ $l^{\prime }\in G;$

• a co-safety TA if $l_{0} \notin G \wedge \not \exists (l,\,g,\,a,\,Y,\,l^{\prime })\in \varDelta :\,l\in G \wedge l^{\prime }\in L\setminus G.$

It is easy to check that safety and co-safety TAs define safety and co-safety properties.³

Example 1

((Safety and co-safety) timed automata) We consider requirements $R_{1},\,R_{2},\,R_{3},$ and $R_{4},$ introduced in Sect. 1. These requirements are respectively formalized as properties $\varphi _{1},\,\varphi _{2},\,\varphi _{3},$ and $\varphi _{4}$ defined by the timed automata in Fig. 2. Accepting locations are denoted by squares. The safety TA in Fig. 2a defines property $\varphi _{1}$ defined over $\varSigma _{1} = \{a,\,r\}.$ The co-safety TA in Fig. 2b defines property $\varphi _{2}$ defined over $\varSigma _{2} = \{r,\,g,\,a\}.$ The TA in Fig. 2c defines property $\varphi _{3}$ defined over $\varSigma _3 = \{r,\,g\}.$ The TA in Fig. 2d defines property $\varphi _{4}$ defined over $\varSigma _{4} = \{r,\,g\}.$

Fig. 2

Examples of TA modeling timed properties

Combining properties using Boolean operations. The next definition, as described in [18], provides a way to combine (complete and deterministic) timed automata and will be used in the sequel to define properties expressed as a Boolean combination of other properties.

Definition 4

(Operations on timed automata) Given two properties $\varphi _{1}$ and $\varphi _{2}$ defined by TAs $\mathcal{A}_{\varphi _1} = ( L_{1},\,\ell ^{0}_{1},\,X_{1},\,\varSigma ,\,\varDelta _{1},\,G_{1})$ and $\mathcal{A}_{\varphi _2} =(L_{2},\,\ell ^{0}_{2},\,X_{2},\,\varSigma ,\, \varDelta _{2},\,G_{2}),$ respectively. The $\times _{op}$-product of $\mathcal{A}_{\varphi _{1}}$ and $\mathcal{A}_{\varphi _2},$ where $op \in \{\cup ,\,\cap \},$ is the timed automaton defined as $\mathcal{A}_{\varphi _{1}}\times _{op} \mathcal{A}_{\varphi _{2}}\mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}(L,\,{l_{0}},\,X,\,\varSigma ,\,\varDelta ,\,G)$ where $L=L_{1} \times L_{2},\,l_{0} = (l^{1}_{0},\,l^{2}_{0}),\,X = X_{1} \cup X_{2}$ (disjoint union), $\varDelta \subseteq L \times \mathcal {G}(X)\times \varSigma \times 2^{X} \times L$ is the transition relation, where $((l_{1},\,l_{2}),\,g_{1} \wedge g_{2},\,a,\,Y_{1} \cup Y_{2},\, (l_{1}^{\prime },\,l_{2}^{\prime })) \in \varDelta$ iff $( l_{1},\, g_{1},\,a,\,Y_{1},\,l_{1}^{\prime } ) \in \varDelta _{1}$ and $(l_{2},\,g_{2},\,a,\,Y_{2},\,l_{2}^{\prime })\in \varDelta _{2}.\,G_{ op }$ is a set of accepting locations with:

• $G_{\cap } = G_{1} \times G_{2},$

• $G_{\cup } = (L_{1} \times G_{2}) \cup (G_{1} \times L_{2}).$

Definition 5

(Negation of a timed automaton) Given a property $\varphi$ defined by a TA $\mathcal{A}_{\varphi } = (L,\,\ell ^{0},\,X,\,\varSigma ,\, \varDelta ,\,G)$ its negation is defined as $\lnot \mathcal{A}_{\varphi } \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}( L ,\,\ell ^{0},\,X,\,\varSigma ,\,\varDelta ,\,L\setminus G).$

The proposition below states that when performing the $\cap$-product (resp. $\cup$-product) between two TAs, it amounts to perform the intersection (resp. union) of the recognized languages.

Proposition 1

Consider two properties $\varphi _{1}$ and $\varphi _{2}$ defined by TAs $\mathcal{A}_{\varphi _{1}} = ( L_{1} ,\, \ell ^{0}_{1},\, X_{1},\, \varSigma ,\,\varDelta _{1},\,G_{1} )$ and $\mathcal{A}_{\varphi _{2}} = ( L_{2} ,\, \ell ^{0}_{2},\,X_{2},\, \varSigma ,\, \varDelta _{2},\,G_{{2}}),$ respectively. The following facts hold:

• $\mathcal{L}_{(\mathcal{A}_{\varphi _{1}}\times _{\cap } \mathcal{A}_{\varphi _{2}})(G_{\cap })} =\varphi _{1}\cap \varphi _{2},$

• $\mathcal{L}_{(\mathcal{A}_{\varphi _{1}}\times _{\cup } \mathcal{A}_{\varphi _{2}})(G_{\cup }) }=\varphi _{1}\cup \varphi _{2},$

• $\mathcal{L}_{\lnot \mathcal{A}_{\varphi _{1}}} = ({\mathbb {R}}_{\ge 0}\times \varSigma _{1})^{*} \setminus \mathcal{L}_{(\mathcal{A}_{\varphi _{1}})},$

• $\mathcal{L}_{\lnot \mathcal{A}_{\varphi _{2}}} = ({\mathbb {R}}_{\ge 0}\times \varSigma _{2})^{*} \setminus \mathcal{L}_{(\mathcal{A}_{\varphi _{2}})}.$

The above proposition entails that the classes of safety and co-safety properties are closed under union and intersection. However, the properties resulting of any other operation between safety, co-safety, and regular properties is a regular property. Finally, note that the negation of a safety (resp. co-safety) property is a co-safety (resp. safety) property. From the results shown in [18], the following proposition holds.

Proposition 2

(Closure of safety, co-safety and regular properties under Boolean operations)

• Safety and co-safety properties are closed under (finite) union and intersection.

• The negation of a safety property is a co-safety property, and vice-versa.

• Regular properties are closed under Boolean operations.

2.3 Preliminaries to runtime enforcement

Given $t\in {\mathbb {R}}_{\ge 0},$ and a timed word $\sigma \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*},$ we define the observation of $\sigma$ at time t as the timed word:

$$\begin{aligned} \mathrm {obs}(\sigma ,\,t) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\mathrm {max}_{\preccurlyeq }\left\{ {\sigma ^{\prime } \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*} \mid \sigma ^{\prime }\preccurlyeq \sigma \wedge {{\mathrm{time}}}(\sigma ^{\prime })\le t} \right\} , \end{aligned}$$

where $\mathrm {max}_{\preccurlyeq }$ takes the maximal sequence according to the prefix ordering $\preccurlyeq$ (unique in this case). That is $\mathrm {obs}(\sigma ,\,t)$ is the longest prefix of $\sigma$ of duration smaller than t. By definition, ${{\mathrm{time}}}(\mathrm {obs}(\sigma ,\,t))\le t,$ meaning that the duration of an observation at time t never exceeds t.

The maximal strict prefix of $\sigma$ that belongs to $\varphi$ is denoted as ${{\mathrm{max}}}^{\varphi }_{\prec ,\epsilon }(\sigma )$ and defined as: ${{\mathrm{max}}}^{\varphi }_{\prec ,\epsilon }(\sigma ) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}{{\mathrm{max}}}_{\preceq }(\{\sigma ^{\prime }\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\mid \sigma ^{\prime }\prec \sigma \wedge \sigma ^{\prime }\in \varphi \}\cup \{\epsilon \}).$

Orders on timed words. Apart from the prefix order $\preccurlyeq ,$ we define the following partial orders on timed words:

Delaying order $\preccurlyeq _\mathrm{d}:$ :

For $\sigma ,\,\sigma ^{\prime } \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*},$ we say that $\sigma ^{\prime }$ delays $\sigma$ (denoted $\sigma ^{\prime } \preccurlyeq _\mathrm{d}\sigma$) iff

$$\begin{aligned} \varPi _{\varSigma }(\sigma ^{\prime }) \preccurlyeq \varPi _{\varSigma }(\sigma )\quad \mathrm{and}\quad \forall i\le |\sigma ^{\prime }|:\,{{\mathrm{delay}}}(\sigma (i))\le {{\mathrm{delay}}}(\sigma ^{\prime }(i)), \end{aligned}$$

which means that $\sigma ^{\prime }$ is “a delayed prefix” of $\sigma .$ This order will be used to characterize outputs w.r.t. to inputs in enforcement monitoring.

Lexical order $\preceq _{\scriptscriptstyle \mathrm lex}:$ :

Given any two timed words $\sigma ,\,\sigma ^{\prime }$ with same untimed projection, i.e., $\varPi _{\varSigma }(\sigma )=\varPi _{\varSigma }(\sigma ^{\prime }),$ and any two timed events with identical actions $(\delta ,\,a)$ and $(\delta ^{\prime },\,a),$ we define $\preceq _{\scriptscriptstyle \mathrm lex}$ inductively as follows: $\epsilon \preceq _{\scriptscriptstyle \mathrm lex}\epsilon ,$ and $(\delta ,\,a)\cdot \sigma \preceq _{\scriptscriptstyle \mathrm lex}(\delta ^{\prime },\,a)\cdot \sigma ^{\prime }$ iff $\delta \le \delta ^{\prime } \vee (\delta =\delta ^{\prime } \wedge \sigma \preceq _{\scriptscriptstyle \mathrm lex}\sigma ^{\prime }).$ This ordering is defined for timed words with identical actions, and is useful to choose a unique timed word among some with same actions.

3 Enforcement monitoring in a timed context

Roughly speaking, the purpose of enforcement monitoring is to read some (possibly incorrect) input sequence produced by a running system (input to the enforcement mechanism), and to transform it into an output sequence that is correct w.r.t. a property $\varphi .$ To ease the design and implementation of enforcement monitoring mechanisms in a timed context, we introduce two sorts of mechanisms: enforcement functions and EMs. From an abstract point of view, an enforcement function describes the transformation of an input timed word into an output timed word according to time. An EM is a transition system, whose input/output behavior realizes an enforcement function. In other words, an enforcement function serves as an abstract description (black-box view) of an EM, and, an EM is an operational description of an enforcement function.

3.1 Enforcement functions

The input of an enforcement function is considered to be a timed word $\sigma$ where every action is associated to the delay since the previous action (or the initialization). Moreover, at this abstract level, even if $\sigma$ is partially known, it is considered to be fully determined from the beginning. At time t, the sequence observed by the enforcement mechanism is $\mathrm {obs}(\sigma ,\,t).$ The output of the enforcement function at time t should be a timed word representing a sequence of actions with delays between them computed from $\mathrm {obs}(\sigma ,\,t).$

Definition 6

(Enforcement function) An enforcement function for a property $\varphi$ is a function $E_\varphi$ from $({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\times {\mathbb {R}}_{\ge 0}$ to $({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}.$

An enforcement function $E_\varphi$ for property $\varphi$ transforms some (possibly incorrect) timed word $\sigma$ given as input (see Fig. 3). In this paper, we assume that enforcement mechanisms do not modify the actions they receive but are rather time retardants, i.e., their output at time t is a timed word $E_\varphi (\sigma ,\,t)$ with same actions as a prefix of their observation, but with possibly increased delays between actions, in such a way that the output timed word satisfies the property.

Fig. 3

Enforcement function $E_\varphi$

Constraints on enforcement functions. Similarly to the untimed setting, several constraints, namely soundness and transparency, are required on how $E_\varphi$ transforms timed words. Since our EMs are time retardants, the physical constraints in the following definition also apply to $E_\varphi .$

Definition 7

(Constraints on an enforcement mechanism) For a timed property $\varphi ,$ an enforcement mechanism behaves as a function $E_\varphi$ from $({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}\times {\mathbb {R}}_{\ge 0}$ to $({\mathbb {R}}_{\ge 0}\times \varSigma )^{*},$ satisfying the following constraints:

• Physically time retardant

  $$\begin{aligned} \begin{array}{ll} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t,\quad t^{\prime }\in {\mathbb {R}}_{\ge 0}:\,t\le t^{\prime } \implies E_\varphi (\sigma ,\,t) \preccurlyeq E_\varphi (\sigma ,\,t^{\prime }) &{}\quad \mathbf{(Phy1)},\\ \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t \in {\mathbb {R}}_{\ge 0}:\,{{\mathrm{time}}}\left( E_\varphi (\sigma ,\,t)\right) \le t &{} \quad \mathbf{(Phy2)}. \end{array} \end{aligned}$$

• Soundness

  $$\begin{aligned} \begin{array}{l} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t \in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t) \ne \epsilon \implies \left( \exists t^{\prime } \ge t:\, E_\varphi (\sigma ,\,t^{\prime }) \models \!\varphi \right) \! \mathbf{(Snd)}. \end{array} \end{aligned}$$

• Transparency

  $$\begin{aligned} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t \in {\mathbb {R}}_{\ge 0}:\,E_\varphi (\sigma ,\,t) \preccurlyeq _{d} \mathrm {obs}(\sigma ,\,t) \quad \mathbf{(Tr)}. \end{aligned}$$

The requirements on the enforcement function are specified by three constraints: physically time retardant, soundness, and transparency. (Phy1) means that the outputs of the enforcement function are concatenated over time, i.e., what is output cannot be modified. (Phy2) expresses that the duration of the output never exceeds t. Soundness (Snd) means that if a timed word is released as output by the enforcement function, in the future, the output of the enforcement function should satisfy property $\varphi .$ In other words, no event is output before being sure that the property will be satisfied by subsequent events. In the particular case of a safety property $\varphi ,$ since $\varphi$ is prefix closed, soundness reduces to $\forall \sigma \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*},\,\forall t \in {\mathbb {R}}_{\ge 0}:\,E_\varphi (\sigma ,\,t) \models \varphi .$ Transparency (Tr) expresses that, at any time t, the output is a delayed prefix of the observed input $\mathrm {obs}(\sigma ,\,t).$

3.2 Functional definition

We propose first a general definition of an enforcement function (Sect. 3.2.1) and then a simplified definition for safety properties (Sect. 3.2.2).

3.2.1 General definition

The enforcement function can be described as a composition of functions, each performing the following steps: (i) processing the input, (ii) computing the delayed timed word satisfying the property, and (iii) and processing the output sequence. Moreover, the enforcement function describes how these functions are composed to transform an input sequence. We will then prove that it satisfies the physical, soundness, and transparency constraints.

Definition 8

(Enforcement function) The enforcement function for a property $\varphi$ is $E_\varphi :\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}$ defined as:

$$\begin{aligned} E_\varphi (\sigma ,\,t) = \begin{array}{cc} \mathrm {obs}\left( \varPi _{1}({{\mathrm{store}}}(\mathrm {obs}(\sigma ,\,t))),\,t\right) , \end{array} \end{aligned}$$

where:

• ${{\mathrm{store}}}:\, ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \rightarrow ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}$ is defined as

  $$\begin{aligned} \begin{array}{rll} {{\mathrm{store}}}(\epsilon ) &{} = &{} (\epsilon ,\,\epsilon )\\ {{\mathrm{store}}}(\sigma \cdot (\delta ,\,a)) &{} = &{} {\left\{ \begin{array}{ll} (\sigma _{s}\cdot {{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}K,\,\epsilon )&{} \mathrm{if} K \ne \emptyset , \\ (\sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a)) &{} \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}$$

• $\kappa _{\varphi }(T,\,\sigma _{s},\,\sigma _c)$ is the set defined as:

  $$\begin{aligned} \begin{array}{lcl} \kappa _{\varphi }\left( T,\,\sigma _{s},\,\sigma _{c}\right) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}&{} \{w \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*} \mid &{} w \preccurlyeq _{d} \sigma _{c} \wedge |w| = \left| \sigma _{c}\right| \,\wedge \\ &{} &{} \sigma _{s}\cdot w\models \!\varphi \! \wedge {{\mathrm{delay}}}(w(1)) T - {{\mathrm{time}}}\left( \sigma _s\right) \}, \mathrm{and} \end{array} \end{aligned}$$

• ${{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}$ stands for minimal timed word according to the lexical order among the timed words with minimal duration.

In the definition of $E_\varphi ,\,\mathrm {obs}(\sigma ,\,t)$ is the prefix of the input that has been observed at time t, and thus can be processed by the enforcement function. The ${{\mathrm{store}}}$ function takes as input this observation, and computes a pair of timed words, whose first component extracted by $\varPi _{1}$ is processed by $\mathrm {obs}$ to produce the output.

The first element of the output of the ${{\mathrm{store}}}$ function is the transformation of a prefix of the observation for which delays have been computed (the property is satisfied by this prefix by appropriate delaying); the second element is the suffix of the observation for which delays still have to be computed. The ${{\mathrm{store}}}$ function is defined inductively: initially, for an empty observation, both elements are empty; if $\sigma$ has been observed, ${{\mathrm{store}}}(\sigma )=(\sigma _{s},\,\sigma _{c}),$ and a new event $(\delta ,\,a)$ is observed, there are two possible cases, according to the vacuity of the set $K=\kappa _{\varphi }({{\mathrm{time}}}(\sigma )+\delta ,\, \sigma _{s},\,\sigma _{c}\cdot (\delta ,\,a))$ (the set of candidate timed words appropriately delaying $\sigma _{c}\cdot (\delta ,\,a)$ and satisfying $\varphi ,$ see below):

• if $K\ne \emptyset ,$ among the set of timed words with minimal duration in K, the minimal timed word w.r.t the lexical order is appended to $\sigma _{s},$ and the second element is set to $\epsilon .$

• otherwise, $(\delta ,\,a)$ is appended to $\sigma _{c}$ and $\sigma _{s}$ is not modified.

The function $\kappa _{\varphi }$ has three parameters: T (the duration of the current observation), $\sigma _{s},$ and $\sigma _{c}.$ It computes the set of candidate timed words w “appropriately delaying” $\sigma _{c}$ such that $\sigma _{s}\cdot w$ satisfies $\varphi .$ The appropriate delaying is such that w and $\sigma _{c}$ have identical actions, same length but delays of w are greater than or equal to those of $\sigma _{c}.$ Moreover the delay of the first action in w should exceed the difference between the duration of the observation and the duration of $\sigma _{s}.$ The reason for this constraint is that $\sigma _{s}$ will be output entirely after a duration of ${{\mathrm{time}}}(\sigma _{s}),$ while the decision to output w is taken after T t.u., thus a smaller value for ${{\mathrm{delay}}}(w(1))$ would cause this delay to be elapsed before the decision is taken. Notice that upon reading an input event $(\delta ,\,a),$ in case if no appropriate delays exist, and correcting the sub-sequence $\sigma _{c}\cdot (\delta ,\,a)$ is impossible (when $\kappa _{\varphi }$ is empty), then the input event $(\delta ,\,a)$ is appended to $\sigma _{c}.$ If the sub-sequence $\sigma _{c}\cdot (\delta ,\,a)$ can be corrected, it is appended immediately to $\sigma _{s}$ (with appropriate delays) without relying on events that will be read later. The adopted “policy” here is to correct the observation of the input sequence as soon as possible (see also Proposition  4 later). Consequently, the input sequence is treated as a series of sub-sequences, each sub-sequence allowing to satisfy the property.

Proposition 3

(Physicality, soundness, and transparency of enforcement functions) Given some property $\varphi ,$ its enforcement function $E_\varphi$ as per Definition 8 satisfies:

• (1) the physical constraints $\mathbf {(Phy1)}$ and $\mathbf {(Phy2)},$

• (2) the soundness $\mathbf {(Snd)}$ and transparency $\mathbf {(Tr)}$ constraints,

as per Definition 7.

In addition, the functional definition also ensures that each sub-sequence is output as soon as possible, as expressed by the following proposition:

Proposition 4

(Optimality of enforcement functions) Given some property $\varphi ,$ its enforcement function $E_\varphi$ as per Definition 8 satisfies the following optimality constraint $\mathbf {(Op)}:$

Intuition of optimality. For any input $\sigma ,$ at any time t, if the output $E_\varphi (\sigma ,\,t)$ is not $\epsilon ,$ and satisfies $\varphi ,$ then the output is considered as two sub-sequences $w_\mathrm{\scriptscriptstyle mx},$ followed by w, such that $w_\mathrm{\scriptscriptstyle mx}$ is the maximal strict prefix of $E_\varphi (\sigma ,\,t),$ satisfying property $\varphi$ and w is the remaining sub-sequence such that $E_\varphi (\sigma ,\,t) = w_\mathrm{\scriptscriptstyle mx}\cdot w.$

The last sub-sequence of the output which again makes the output to satisfy $\varphi$ after $w_\mathrm{\scriptscriptstyle mx}$ is w. The optimality constraint expresses that the sum of the delays (i.e., the time required to output) of w is minimal. The delay for the events in w should be chosen such that $E_\varphi (\sigma ,\,t)=w_\mathrm{\scriptscriptstyle mx}\cdot w$ satisfies $\varphi$ and the transparency condition, and the delay of the first event is greater than the difference between the duration of the input sequence $\sigma _{[1\cdots |E_\varphi (\sigma ,t)|]}$ and the duration of $w_\mathrm{\scriptscriptstyle mx}.$

Notice that if ${{\mathrm{time}}}(\sigma _{[1\cdots |E_\varphi (\sigma ,t)|]}) - {{\mathrm{time}}}(w_\mathrm{\scriptscriptstyle mx})$ is negative or null, then this means that the delay corresponding to some events in the sequence preceding w (which is $w_\mathrm{\scriptscriptstyle mx}$) are increased, providing sufficient amount of time to observe the last sub-sequence (which is $\sigma _{[|w_\mathrm{\scriptscriptstyle mx}|+1\cdots |w_\mathrm{\scriptscriptstyle mx}|+|w|]}$) entirely. In case ${{\mathrm{time}}}(\sigma _{[1\cdots |E_\varphi (\sigma ,t)|]}) - {{\mathrm{time}}}(w_\mathrm{\scriptscriptstyle mx})$ is positive, all events in $w_\mathrm{\scriptscriptstyle mx}$ have been released as output before the last sub-sequence $\sigma _{[|w_\mathrm{\scriptscriptstyle mx}|+1\cdots |w_\mathrm{\scriptscriptstyle mx}|+|w|]}$ is observed entirely as input. After releasing $w_\mathrm{\scriptscriptstyle mx}$, ${{\mathrm{time}}}(\sigma _{[1\cdots |E_\varphi (\sigma ,t)|]}) - {{\mathrm{time}}}(w_\mathrm{\scriptscriptstyle mx})$ time units have elapsed and thus the last sub-sequence w can be released as output only after a delay of ${{\mathrm{time}}}(\sigma _{[1\cdots |E_\varphi (\sigma ,t)|]}) - {{\mathrm{time}}}(w_\mathrm{\scriptscriptstyle mx})$ time units.

Proof (of Propositions 3 and 4: sketch only)

The proofs are given in Appendices 1.1 (for physical constraints), 1.2 (for soundness and transparency), 1.3 (for optimality), in p. 31, 32, 33, respectively. The proofs rely on an induction on the length of the input word $\sigma .$ The induction step uses a case analysis, depending on whether the input is completely observed or not at time t, whether the input can be delayed into a correct output or not, and whether the memory content (computed by ${{\mathrm{store}}}$) is completely dumped or not at time t. $\square$

The following example illustrates the notion of enforcement function.

Example 2

(Enforcement function) We now illustrate how Definition 8 is applied to enforce property $\varphi _{3}$ defined by the automaton depicted in Fig. 2c with $\varSigma =\{g,\,r\}$, and the input timed word $\sigma = (3,\,g) \cdot (10,\,r) \cdot (3,\,g) \cdot (5,\,g).$ Variable t describes global time. Figure 4 shows the evolution of $\mathrm {obs},\,{{\mathrm{store}}},$ and $E_\varphi$ over time for the input $\sigma .$ The resulting output is $(13,\,g)\cdot (15,\,r),$ which satisfies property $\varphi _{1}.$

Fig. 4

Evolution of the enforcement function for $\varphi _{3}$

It is worth noticing that not all regular properties are enforceable, as illustrated by the following example.

Example 3

(Enforcement function: a non-enforceable property) Let us consider again property $\varphi _{4},$ formalized by the TA in Fig. 2d, with $\varSigma$= $\{g,\,r\}$, and the input timed word $\sigma = (3,\,r)\cdot (4,\,g)\cdot (2,\,r)\cdot (6,\,g).$ Figure 5 shows the evolution of $\mathrm {obs},\,{{\mathrm{store}}},$ and $E_\varphi .$ Variable t describes global time. The resulting output of the enforcement function is $\epsilon$ at any time instant.

Fig. 5

Evolution of the enforcement function for $\varphi _{4}$

Remark 3

(Non-enforceable properties) From Example 3, notice that the output of the enforcement function is $\epsilon ,$ though the input sequence itself satisfies the property. The monitor observes action r followed by action g only at $t = 7.$ Hence, the delay associated with the first action in output should be at least 7 t.u., but increasing the delay associated with the first action to 7, would falsify the guard on transition between $l_{0}$ to $l_{1},$ which is a possible move upon the first event $req$, and there is no transition with a reset of clock x before.

It can be noticed that guards with $<,\,\le ,$ and $=$ impose urgency on releasing an event as output at or before some time. For some properties, some input sequences that can be delayed to satisfy $\varphi$ cannot be corrected by enforcement, because the delay of the first event of each sub-sequence may be increased, which may falsify a guard with $<,\,\le ,\,=.$ However, even for such properties, the enforcement function will never produce incorrect outputs. Moreover, note that the notion of non-enforceability exhibited here does not stem from the fact that we focus on enforcement mechanisms that act as delayers. Indeed, even if our enforcement mechanisms were able to reduce delays between events (by for instance releasing g immediately after r), the property would remain non-enforceable because of the guard “$x \le 5$” on the transition between locations $l_{0}$ and $l_{1}.$

Remark 4

(Alternative enforcement strategies) The optimality constraint presented in Proposition 4 allows only to augment delays of events. For each event, a delay greater than or equal to the actual delay is chosen. This condition can be modified or relaxed according to our requirements. This condition can be easily adapted to a given time bound in ${\mathbb {R}}_{\ge 0}.$ It may also be possible to shorten the delay of some events (as long as the duration of the output is greater than the input, i.e., when it satisfies Phy2). Additionally, processing input and output actions is assumed to be done in zero time. Some delay (either fixed or depending on additional parameters) can be considered for this action by modifying the ${{\mathrm{store}}}$ function, and adding this constraint in the definition of $\kappa _{\varphi }.$ Such modification would reduce the set of enforceable properties.

Remark 5

(Elimination of some acceptable behaviors by the enforcement function) As we saw earlier in Remark 3, some input sequences that can be delayed to satisfy $\varphi$ cannot be accepted (and released as output) by the enforcement function. This behavior of the enforcement function stems from the following facts:

• At anytime, decision is taken based on the input events received until that time, and the enforcer has no information regarding the events that it will receive in the future.

• Moreover, we defined optimality in such a way that, the decision about releasing events is taken as soon as possible (when a mechanism knows that there is a possibility to correct, it does not wait for any further input events).

Note, this is also the case for control mechanisms in supervisory control theory for discrete event systems.

3.2.2 Simplified functional definitions

The functional definitions for enforcement in the case of safety or co-safety properties can be simplified. As an example, we briefly explain how the functional definition can be simplified for safety properties.

Simplified functional definition for safety properties. For safety properties, the store function can be simplified: the output is a timed word instead of a pair of timed words ($\mathrm {store}_{\varphi }^\mathrm{sa}:\, ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*$). In fact for a safety property, the delay of each input event, if there exists one, can be computed immediately. Thus the second element of the store output pair (which stores events with undetermined delays) is unnecessary. The store function for safety properties can be defined as follows:

$$\begin{aligned} \begin{array}{rcl} \mathrm {store}_{\varphi }^\mathrm{sa}(\epsilon ) &{} = &{} \epsilon ,\\ \mathrm {store}_{\varphi }^\mathrm{sa}(\sigma \cdot (\delta ,\,a)) &{} = &{} \left\{ \begin{array}{ll} \mathrm {store}_{\varphi }^\mathrm{sa}(\sigma ) \cdot ({{\mathrm{min}}}(K),\,a) &{}\quad \mathrm{if}\, K \ne \emptyset , \\ \mathrm {store}_{\varphi }^\mathrm{sa}(\sigma ) &{}\quad \mathrm{otherwise}, \end{array} \right. \end{array} \end{aligned}$$

where $K \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\{\delta ^{\prime } \in {\mathbb {R}}_{\ge 0}\mid \delta ^{\prime } \ge \delta \wedge \mathrm {store}_{\varphi }^\mathrm{sa}(\sigma )\cdot (\delta ^{\prime },\,a) \preccurlyeq _{d} \sigma \cdot (\delta ,\,a) \wedge \mathrm {store}_{\varphi }^\mathrm{sa}(\sigma )\cdot (\delta ^{\prime },\,a) \models \varphi \}.$

K is the set of delays $\delta ^{\prime }$ that can be associated to a such that the extension $\mathrm {store}_{\varphi }^\mathrm{sa}(\sigma )\cdot (\delta ^{\prime },\,a)$ of the previous $\mathrm {store}_{\varphi }^\mathrm{sa}(\sigma )$ delays $\sigma \cdot (\delta ,\,a)$ and still satisfies property $\varphi .$ It depends on $\varphi ,$ $\sigma$ (more precisely $\mathrm {store}_{\varphi }^\mathrm{sa}(\sigma )$), and $(\delta ,\,a).$

Remark 6

For the particular case of safety properties, Propositions 3 and 4 also hold when using the simplified functional definition (using the $\mathrm {store}_{\varphi }^\mathrm{sa}$ function).

Moreover, with the alternative functional definition for safety properties using function $\mathrm {store}_{\varphi }^\mathrm{sa},$ the optimality constraint in Proposition 4 which the enforcement function satisfies can be simplified and defined alternatively as follows.

Simplified optimality constraint of an enforcement function for safety properties. If $E_\varphi$ is sound, transparent, and satisfies the physical constraints (Phy1) and (Phy2), $E_\varphi$ is said to be optimal if the following constraint holds:

$$\begin{aligned} \begin{array}{lr} \forall \sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*, \forall t\in {\mathbb {R}}_{\ge 0}:\\ \quad |E_\varphi (\sigma ,\,t)| \!=\! {{\mathrm{max}}}\big \{ |o^{\prime }| \mid o^{\prime } \preccurlyeq _{d} \!\mathrm {obs}(\sigma ,\,t) \!\wedge o^{\prime } \!\models \varphi \cap \left( \widehat{E_\varphi }(\sigma ,\,t)\!\cdot ({\mathbb {R}}_{\ge 0}\times \Sigma )^*\right) \big \} &{} \mathbf{(Op-saf)}\\ \qquad \qquad \mathrm{where}\,\widehat{E_\varphi }(\sigma ,\,t) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}\mathrm {max_{\preccurlyeq }}\left\{ E_\varphi (\sigma ,\,t^{\prime }) \mid t^{\prime } < t\right\} . \end{array} \end{aligned}$$

The optimality constraint (Op-saf) expresses that at any time instant t, the output sequence $E_\varphi (\sigma ,\,t)$ should be the longest correct timed word delaying the input sequence $\mathrm {obs}(\sigma ,\,t)$ that extends $\widehat{E_\varphi }(\sigma ,\,t),$ the maximal output sequence strictly before t. Notice that the term $({\mathbb {R}}_{\ge 0}\times \Sigma )^*$ takes into account the fact that several timed actions may be output at time t.

3.3 Enforcement monitor

In what follows, we consider a property $\varphi$ defined by a TA $\mathcal{A}_{\varphi }$ whose semantics is a transition system $[\![\mathcal{A}_{\varphi }]\!]=(Q,\,q_{0},\,\varGamma ,\,\rightarrow ,\,F_{G}).$

An enforcement function $E_\varphi$ for $\varphi$ is implemented by an EM, defined as a transition system $\mathcal{E}.$ An EM is an operational view of the enforcement function. It is equipped with a memory and a set of enforcement operations used to store and dump some timed events to and from the memory, respectively. The memory of an EM consists of two queues, each containing a timed word, one storing the received actions (with increased delays) which are corrected and can be released as output. The other queue stores the actions that are read by the EM, but are yet to be corrected (and cannot be released as output). In addition, an EM also keeps track of the state of the underlying TA, and clock values used to count time between input events and between output events.

Before presenting the definition of EM, we introduce $\mathrm {update}$ as a function from $Q \times ({\mathbb {R}}_{\ge 0}\times \varSigma )^{+} \times {\mathbb {R}}_{\ge 0}$ to $({\mathbb {R}}_{\ge 0}\times \varSigma )^{+} \times \mathbb {B}.$ The update function takes as input a triple $(q,\,\sigma _{c},\,m_{t})$ where $q \in Q$ is the (current) state of $[\![\mathcal{A}_{\varphi }]\!],\,\sigma _{c} \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{+}$ is a non-empty timed word, and $m_{t}\in {\mathbb {R}}_{\ge 0}$ is the difference between the duration of the input sequence observed minus the duration of the corrected sequence, and returns a timed word of length $|\sigma _{c}|$ and a Boolean as output.

$$\begin{aligned} \mathrm {update}\left( q,\,\sigma _{c},\,m_{t}\right) \mathop {=}\limits ^{{\scriptstyle \mathrm {def}}}{\left\{ \begin{array}{ll} \left( \sigma _{c},\,\mathtt {ff} \right) &{} \mathrm{if}\,\varLambda \left( \sigma _{c},\, m_{t},\,q\right) = \emptyset ,\\ \left( \sigma ^{\prime }_{c},\,\mathtt {tt}\right) &{} \mathrm{otherwise};\\ \end{array}\right. } \end{aligned}$$

where $\sigma ^{\prime }_{c} = {{{\mathrm{min}}}_{\preceq _{\scriptscriptstyle \mathrm lex,time}}}\varLambda (\sigma _{c},\,m_{t},\,q)$ with $\varLambda :\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{+} \times {\mathbb {R}}_{\ge 0}\times Q\rightarrow 2^{({\mathbb {R}}_{\ge 0}\times \Sigma )^*}$ defined as:

$$\begin{aligned} \begin{array}{rl} \varLambda \left( \sigma _{c},\,m_{t},\,q\right) =&{} \big \{w \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{+} \mid w \preccurlyeq _{d} \sigma _{c} \wedge |w| = \left| \sigma _{c}\right| \wedge {{\mathrm{delay}}}(w(1)) \ge m_{t}\\ &{} \quad \quad \quad \quad \quad \quad \quad \quad \quad \wedge q\mathop {\rightarrow }\limits ^{w}F_{G}\big \}. \end{array} \end{aligned}$$

$\varLambda (\sigma _{c},\,m_{t},\,q)$ is the set of timed words w of length $|\sigma _{c}|$ with same actions as $\sigma _{c},$ each delay in the sequence is equal to or greater than the delay at the corresponding index in the provided input sequence $\sigma _{c},$ and the first delay in w should be greater than or equal to $m_{t},$ and an accepting state is reachable from state q upon sequence w.

• The first case applies when there are no good delays such that an accepting state is reachable from the state q upon with a sequence delaying $\sigma _{c}\,(\varLambda (\sigma _{c},\,m_{t},\,q) = \emptyset$). In this case, the $\mathrm {update}$ function returns the same timed word $\sigma _{c}$ (which is provided as input), and a Boolean value $\mathtt {ff},$ indicating that no accepting state is reachable.

• The second case applies when there are good delays and an accepting state in $q_{1}\in Q_{F}$ is reachable from q upon a sequence delayed from $\sigma _{c}.$ In this case, the $\mathrm {update}$ function returns a timed word of minimal duration belonging to $\varLambda (\sigma _{c},\,m_{t},\,q),$ chosen according to the lexical order; and a Boolean value $\mathtt {tt},$ indicating that an accepting state is reachable.

Definition 9

(Enforcement Monitor) An EM $\mathcal{E}$ for $\varphi$ is a transition system $(C^{\mathcal{E}},\,c_{0}^{\mathcal{E}},\, \varGamma ^{\mathcal{E}},\,\hookrightarrow _{\mathcal{E}})$ s.t.:

• $C^{\mathcal{E}} = ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times {\mathbb {R}}_{\ge 0}\times {\mathbb {R}}_{\ge 0}\times {\mathbb {R}}_{\ge 0}\times Q$ is the set of configurations,

• $c_{0}^{\mathcal{E}} = \langle \varepsilon ,\, \varepsilon ,\, 0,\, 0,\, 0,\, q_{0}\rangle \in C^{\mathcal{E}}$ is the initial configuration,

• $\varGamma ^{\mathcal{E}}=(({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \}) \times Op \times (({\mathbb {R}}_{\ge 0}\times \varSigma )\cup \{\epsilon \})$ is the alphabet, which is composed of triples, comprised of an optional input event, an operation, and an optional output event, where the set of possible operations is $Op=\{ \mathrm {store}$-$\overline{\varphi }(\cdot ),\,\mathrm {store}$-$\varphi (\cdot ),\, {{\mathrm{dump}}}(\cdot ),\,{{\mathrm{idle}}}(\cdot )\},$

• $\hookrightarrow _{\mathcal{E}} \subseteq C^{\mathcal{E}} \times \varGamma _{\mathcal{E}} \times C^{\mathcal{E}}$ is the transition relation defined as the smallest relation obtained by the following rules applied with the priority order below:

  • (1) store- $\overline{\varphi }:$ $\left( \sigma _{s},\,\sigma _{c},\,\delta ,\,d,\,m_{t},\,q\right) \mathop {\hookrightarrow _{\mathcal{E}}}\limits ^{(\delta ,\,a)/\mathrm {store}{\text {-}} \overline{\varphi }(\delta ,\,a)/\epsilon } \left( \sigma _{s},\,\sigma _{c} \cdot (\delta ,\,a),\,0,\,d,\,m^{\prime }_{t},\,q\right) ,$    if  $\varPi _{2}\left( \mathrm {update}\left( q,\,\sigma _{c}\cdot (\delta ,\,a),\,m_{t}+\delta \right) \right) =\mathtt {ff},$ where:

    • $m^{\prime }_{t} = m_t+ \delta ,$

  • (2) store- $\varphi :$ $\left( \sigma _{s},\,\sigma _{c},\,\delta ,\,d,\,m_{t},\,q\right) \mathop {\hookrightarrow _{\mathcal{E}}}\limits ^{(\delta ,\,a)/\mathrm {store}{\text {-}}\varphi (\delta ,\,a)/\epsilon } \left( \sigma _{s} \cdot \sigma ^{\prime }_{c},\,\epsilon ,\,0,\,d,\,m^{\prime }_{t},\,q^{\prime }\right) ,$ if $\left( \mathrm {update}\left( q,\,\sigma _{c}\cdot (\delta ,\,a),\,m_{t}+\delta \right) \right) = (\sigma ^{\prime }_{c},\,\mathtt {tt}),$ where:

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

    • $q^{\prime }$ is defined as $q\mathop {\rightarrow }\limits ^{\sigma ^{\prime }_{c}}q^{\prime },$

  • (3) dump: $\left( (\delta ,\,a)\cdot \sigma _{s},\,\sigma _{c},\,s,\,\delta ,\,m_{t},\, q\right) \mathop {\hookrightarrow _{\mathcal{E}}}\limits ^{\epsilon /{{\mathrm{dump}}}(\delta ,\,a)/(\delta ,\,a)}\left( \sigma _{s},\,\sigma _{c},\,s,\,0,\,m_{t},\,q\right) ,$

  • (4) idle: $\left( \sigma _{s},\,\sigma _{c},\,s,\,d,\,m_{t},\,q\right) \mathop {\hookrightarrow _{\mathcal{E}}}\limits ^{\epsilon /{{\mathrm{idle}}}(\delta )/\epsilon } \left( \sigma _{s},\,\sigma _{c},\,s+\delta ,\,d+\delta ,\,m_{t},\,q\right) .$

A configuration $(\sigma _{s},\,\sigma _{c},\,s,\,d,\,m_{t},\,q)$ of the EM consists of the current stored sequence (i.e., the memory content) $\sigma _{s},$ and $\sigma _{c}.$ The sequence that is corrected and can be released as output is denoted by $\sigma _{s}.$ The sequence $\sigma _{c}$ is sort of an internal memory for the $\mathrm {store}$ function: this is the input sequence read by the EM, but yet to be corrected. The configuration also contains two clock values s and d indicating respectively the time elapsed since the last store and dump operations, and one more counter $m_{t}$ indicating the difference between the duration of the observed input sequence and the duration of the corrected sequence. q is the current state of $[\![\mathcal{A}_{\varphi }]\!]$ reached after processing the sequence already released followed by the timed word in memory $\sigma _{s}.$

Semantic rules can be understood as follows:

• Upon reception of an event $(\delta ,\,a),$ one of the following store rules is executed.

  • The store- $\overline{\varphi }$ rule is executed if the $\mathrm {update}$ function returns $\mathtt {ff}$ (indicating that $\sigma _{c}\cdot (\delta ,\,a)$ cannot be corrected). The clock s is reset to 0, and the event $(\delta ,\,a)$ is appended to the internal memory $\sigma _{c}.$ The delay corresponding to the input event $\delta$ is added to $m_{t}.$

  • The store- $\varphi$ rule is executed if the $\mathrm {update}$ function returns $\mathtt {tt},$ indicating that $\varphi$ can be satisfied for the sequence already released as output, followed by the sequence in $\sigma _{s},$ followed by $\sigma _{c}\cdot (\delta ,\,a)$ with possibly increased delays. When executing this rule, s is reset to 0, and the timed word $\sigma ^{\prime }_{c}$ returned by the $\mathrm {update}$ function is appended to the content of the output memory $\sigma _{s}.$ The delay of the input event $\delta$ is added to $m_{t},$ and the duration of the corrected sub-sequence returned by the $\mathrm {update}$ function, ${{\mathrm{time}}}(\sigma ^{\prime }_{c}),$ is subtracted from $m_{t}.$

• The dump rule is executed if the time elapsed since the last dump operation d, is equal to the delay corresponding to the first event of the timed word $\sigma _{s}$ in the memory. The event $(\delta ,\,a)$ is released as output and removed from $\sigma _{s},$ and the clock d is reset to 0.

• The idle rule adds the time elapsed $\delta$ to the current values of s and d when neither the store nor the dump rule applies.

Example 4

(Execution of an EM) We now illustrate how the rules of Definition 9 are applied to enforce property $\varphi _{3},$ defined by the automaton depicted in Fig. 2c. Let us consider the input timed word $\sigma = (3,\,g) \cdot (10,\,r) \cdot (3,\,g) \cdot (5,\,g).$ Figure 6 shows how semantic rules are applied, and the evolution of the configurations of the EM. In a configuration, the input (resp. output) is on the right (resp. left). Variable t describes global time. The resulting output is $(13,\,g)\cdot (15,\,r),$ which satisfies property $\varphi _{3}.$ From $t=28,$ only the idle rule can be applied.

Fig. 6

Execution of an enforcement monitor

Remark 7

(Simplified definitions of EM) To synthesize an EM for a safety or co-safety property, one can use simplified definitions. For example, for a safety property, only one timed word is needed in the configuration. Indeed, recall that $\sigma _{c}$ is a sort of internal memory used to store the input events used when it may be possible to reach an accepting state if more events are observed in the future. Since a safety property is prefix-closed, upon an event that cannot be delayed to keep satisfying the property, no future extension can. Hence, $\sigma _{c}$ is not necessary for safety properties. Therefore, some simplifications, that may lead to performance improvements, are possible.

3.4 Relating enforcement functions and EMs

We present how the definitions of enforcement function and EM can be related: given a property $\varphi ,$ any input sequence $\sigma ,$ at any time instant t, the output of the associated enforcement function and the output-behavior of the associated EM are equal.

We first describe how an EM reacts to an input sequence. In the remainder of this section, we consider an EM $\mathcal{E}=(C^{{\scriptscriptstyle \mathcal{E}}},\, c_{0}^{{\scriptscriptstyle \mathcal{E}}},\,\varGamma ^{{\scriptscriptstyle \mathcal{E}}},\,\hookrightarrow _{{\scriptscriptstyle \mathcal{E}}}).$ EMs, as defined in Sect. 3.3, are deterministic. By determinism, we mean that the observable behavior of our EMs, i.e., given an input sequence the observable output sequence is unique. Moreover, given $\sigma \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}$ and $t\in {\mathbb {R}}_{\ge 0},$ how an EM reads $\sigma$ until time t is unique: it goes through a unique sequence of configurations. However, given an input sequence $\sigma$ and a time instant t, because of $\epsilon$’s in the input alphabet there is possibly an infinite set of corresponding sequences over the input–operation–output alphabet (as in Definition 9). All these sequences are equivalent: they involve the same configurations for the EM and the same output sequence. Consequently, the rules of the transition relations are ordered in such a way that reading $\epsilon$ will always be the transition with least priority. As a consequence given an input sequence reading $\epsilon$ (and doing other operations such as outputting some event) will always be possible when the monitor cannot read an input. This constraint is consistent with our hypothesis stating that EMs execute infinitely faster than their environment.

More formally, let us define $\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)\in (\varGamma ^{{\scriptscriptstyle \mathcal{E}}})^{*}$ to be the unique sequence over the alphabet of actions (triples comprised of an optional input event, an operation, and an optional output event) that is “triggered” when the EM reads $\sigma$ until time t.

Definition 10

(Input–operation–output sequence) Given an input sequence $\sigma \in ({\mathbb {R}}_{\ge 0}\times \varSigma )^{*}$ and some time instant $t\in {\mathbb {R}}_{\ge 0},$ we define the input–operation–output sequence denoted as $\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)$ and which triggered when an EM of initial configuration $c_{0}^{{\scriptscriptstyle \mathcal{E}}}$ reads $\sigma$ until time t. $\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)$ is defined as the unique sequence of $(\varGamma ^{{\scriptscriptstyle \mathcal{E}}})^{*}$ such that:

$$\begin{aligned} \begin{array}{rl} \exists c\in C^{{\scriptscriptstyle \mathcal{E}}}:\,&{} c_{0}^{{\scriptscriptstyle \mathcal{E}}} {\mathop {\hookrightarrow ^{*}_{{\scriptscriptstyle \mathcal{E}}}}\limits ^{\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)}} c\\ \wedge &{} \varPi _{1}\left( \mathcal{E}_\mathrm {ioo}(\sigma ,\,t)\right) =\mathrm {obs}(\sigma ,\,t)\\ \wedge &{} {{\mathrm{timeop}}}\left( \varPi _{2}\left( \mathcal{E}_\mathrm {ioo}(\sigma ,\,t)\right) \right) = t\\ \wedge &{} \not \exists c^{\prime }\in C^{{\scriptscriptstyle \mathcal{E}}},\quad \exists e\in ({\mathbb {R}}_{\ge 0}\times \varSigma ):\, c \mathop {\hookrightarrow }\limits ^{(\epsilon ,{{\mathrm{dump}}}(e),e)} c^{\prime }, \end{array} \end{aligned}$$

where the ${{\mathrm{timeop}}}$ function indicates the duration of a sequence of enforcement operations and says that only the ${{\mathrm{idle}}}$ enforcement operation consumes time. Formally:

$$\begin{aligned} {{\mathrm{timeop}}}( op \cdot ops )&= \left\{ \begin{array}{ll} d + {{\mathrm{timeop}}}( ops ) &{} \mathrm{if}\,\exists d \in {\mathbb {R}}_{\ge 0}:\, op = {{\mathrm{idle}}}(d),\\ {{\mathrm{timeop}}}( ops ) &{} \mathrm{otherwise}; \end{array}\right. \\ {{\mathrm{timeop}}}(\epsilon )&= 0. \end{aligned}$$

The input timed word corresponding to $\mathrm {obs}(\sigma ,\,t)$ at any time $t$ is the concatenation of all the input events read/consumed by the EM over various steps. Observe that because of the assumptions on $\varGamma ^{{\scriptscriptstyle \mathcal{E}}},$ only the idle rule applies to the configuration c: the dump rule does not apply by definition of $\mathcal{E}_\mathrm {ioo}(\sigma ,\,t)$ and none of the store rules applies because $\varPi _{1}(\mathcal{E}_\mathrm {ioo}(\sigma ,\,t))=\mathrm {obs}(\sigma ,\,t).$

Relating enforcement functions and EMs. Now, we can relate the enforcement function and the EM, for a property $\varphi .$ Seen from the outside, an EM $\mathcal{E}$ behaves as a device reading and producing timed words. Overloading notations, we can characterize this input/output behavior as a function $\mathcal{E}:\,({\mathbb {R}}_{\ge 0}\times \varSigma )^{*} \times {\mathbb {R}}_{\ge 0}\rightarrow ({\mathbb {R}}_{\ge 0}\times \Sigma )^*$ defined as:

$$\begin{aligned} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\, \mathcal{E}(\sigma ,\,t) = \varPi _{3}\left( \mathcal{E}_\mathrm {ioo}(\sigma ,\,t)\right) . \end{aligned}$$

The corresponding output timed word $\mathcal{E}(\sigma ,\,t)$ at any time t is the concatenation of all the output events produced by the EM over various steps of the EM (erasing $\epsilon$’s). As before, the $\epsilon$’s output by the store operation are erased. In the following, we do not make the distinction between an EM and the function that characterizes its behavior.

Finally, we are able to relate enforcement functions, and the functions derived from an EM. For this purpose, we define an implementation relation between EMs and enforcement functions as follows.

Definition 11

(Implementation relation between enforcement functions and EMs) Given an enforcement function $E_\varphi$ (as per Definition 6) and an EM (as per Definition 9) whose behavior is characterized by a function $\mathcal{E},$ we say that $\mathcal{E}$ implements $E_\varphi$ iff:

$$\begin{aligned} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t)= \mathcal{E}(\sigma ,\,t). \end{aligned}$$

Proposition 5

(Relation between enforcement function and EM) Given a property $\varphi ,$ its enforcement function $E_\varphi$ (as per Definition 8), and its EM $\mathcal{E}$ (as per Definition 9), $\mathcal{E}$ implements $E_\varphi$ in the sense of Definition 11.

Proof (of Proposition 5: sketch only)

The proof is given in Appendix 1, p. 37. The proof is done by induction on the length of the input sequence and uses a similar case analysis as the proof of Proposition 6. The proof also uses several intermediate lemmas that characterize some special configurations (e.g., value of the store and dump variables, memory content) of an EM at some time instants.

3.5 Implementation of EMs

Let us now see the algorithms, which are a straightforward translation of the EM semantics, showing how EMs can be implemented. The implementation of an EM consists of two processes running concurrently (Store and Dump) as shown in Fig. 7, and a memory. The Store process models the store rules. The memory contains the timed word $\sigma _{s}:$ the corrected sequence that can be released as output. The memory $\sigma _{s}$ is realized as a queue, shared by the Store and Dump processes, where the Store process adds events which are processed and corrected to this queue. The Dump process reads events stored in the memory $\sigma _{s}$ and releases them as output after the required amount of time. The Store process also makes use of another internal buffer $\sigma _{c}$ (not shared with any other process), to store the events which are read, but cannot be corrected (to satisfy the property). In the algorithms the $\mathrm {await}$ primitive is used to wait for a trigger event from another process or to wait until some condition becomes true. The $\mathrm {wait}$ primitive is used by a process to wait for a certain amount of time, that is determined by the process itself.

Fig. 7

Realizing an EM

The $\mathsf {StoreProcess}$ algorithm (see Algorithm 1) is an infinite loop that scrutinizes the system for input events. In the algorithm, $(l,\,\nu )$ represents the state of the automaton defining the property, where l represents the location and $\nu$ is the current clock valuation. It is initialized to $(l_{0},\,[X\leftarrow 0]).$ The variable $m_{t}$ is used to keep track of the difference between the duration of the input sequence read (the sequence which is already corrected followed by the sequence in $\sigma _{c}$), and the duration of the corrected sequence. The $\mathrm {update}$ function takes the events stored in the internal memory of the store process $\sigma _{c},$ the current state, and $m_{t},$ and returns a timed word of same length as $\sigma _{c}$ and a Boolean indicating whether an accepting state is reachable from the current state upon the timed word it returns as a result. The function ${\mathrm {post}}$ takes a state of the automaton defining the property $(l,\,\nu ),$ a timed word, and computes the state reached by this automaton.

The algorithm proceeds as follows. The $\mathsf {StoreProcess}$ initially waits for an input event. A received event is appended to the internal buffer $\sigma _{c},$ with the corresponding delay $\delta ,$ and this delay $\delta$ is added to $m_{t}.$ Then the $\mathrm {update}$ function is invoked providing the events stored in $\sigma _{c}$ as input. If the $\mathrm {update}$ function indicates that there is a path leading to an accepting state, (i.e., if $isPath =\mathtt {tt}$), then the timed word $\sigma ^{\prime }_{c}$ returned by the $\mathrm {update}$ function, is appended to the shared memory $\sigma _{s}$ (since it now corrected with respect to the property, and can be released as output). Then, the duration of $\sigma ^{\prime }_{c}$ is subtracted from $m_{t}.$ Before proceeding to the next iteration, the state of the automaton $(l,\,\nu )$ is updated, and the internal memory $\sigma _{c}$ is cleared.

The $\mathsf {DumpProcess}$ algorithm (see Algorithm 2) is an infinite loop that scrutinizes the memory and proceeds as follows: initially, the clock d is set to 0. If the memory is empty ($\sigma _{s}=\epsilon$), the $\mathsf {DumpProcess}$ waits until a new element $(\delta ,\,a)$ is stored in the memory. Else (the memory is not empty), it proceeds with the first element in the memory. Using the dequeue operation, the first element stored in the memory is removed, and is stored as $(\delta ,\,a).$ Meanwhile, d keeps track of the time elapsed since the last dump operation. The $\mathsf {DumpProcess}$ waits for $(\delta -d)$ time units before performing the dump(a) operation, releasing the action a as output (which amounts to appending $(\delta ,\,a)$ to the output of the EM). Finally, the clock d is reset to 0 before the next iteration starts.

Remark 8

(Using non-deterministic TAs to define properties) In this paper, the presentation considers only deterministic TAs. Extending the results to non-deterministic TAs comes directly from the policy used to choose a unique solution to define the $\mathrm {update}$ function (which computes the correct and optimal delays). The $\mathrm {update}$ function first computes all accepting paths from the current state, for the given input sub-sequence. And from this set of all accepting paths, a unique solution with minimal duration is chosen using the lexical order. Thus, note that the same mechanisms and algorithms remain valid (without requiring any change) to also enforce properties defined with non-deterministic TAs.

Remark 9

(Simplified algorithms) For safety and co-safety properties, if we want to implement monitors following the simplified functional and EM definitions, the algorithm for the $\mathsf {StoreProcess}$ can also be simplified. In particular, in the algorithm for safety properties, the content of the memory can be maintained by a single sequence of events instead of a tuple. Also, in case of safety properties, the $\mathrm {update}$ function is always invoked with a single event as input, instead of a sequence of events. The simplified algorithms for safety and co-safety properties are described in detail in [16].

Remark 10

(Enforcing several properties) Earlier in this section, we described how any regular property can be enforced. When a Boolean combination of properties has to be enforced on a system, we can combine the properties in a single one and synthesize one EM for the resulting property. Definition 4 in Sect. 2 describes how two properties defined by TAs can be combined using Boolean operations (e.g., union, intersection and negation).

4 Implementation and evaluation

We implemented the algorithms in Sect. 3.5 and developed an experimentation framework called TIPEX: (TImed Properties Enforcement during eXecution) in order to:

• (1) validate through experiments the architecture and feasibility of enforcement monitoring, and

• (2) measure and analyze the performance of the $\mathrm {update}$ function of the $\mathsf {StoreProcess}$ in the case of safety and co-safety properties.

From [16], we completely re-implemented the EMs. Still following the algorithms proposed in [16], TIPEX is more independent and offers better performance. It is now completely independent from UPPAAL at runtime. Moreover, TIPEX does not invoke UPPAAL to realize $\mathrm {update}$ anymore, and some other redundancies, such as updating the UPPAAL model file after each event, are also eliminated.

In this paper, we focus on evaluating the performance using some safety and co-safety properties. In Sect. 3, we described how the definitions of enforcement mechanisms can be simplified if we know that the property is safety (or co-safety). Thus, instead of using the algorithms proposed for regular properties in Sect. 3.5, TIPEX is implemented using the algorithms based on the simplified definitions for safety and co-safety properties described in [16]. Extending TIPEX for regular properties based on the algorithms proposed in this paper, and evaluation using some regular properties which are neither safety nor co-safety, is ongoing.

We focus on benchmarking the $\mathrm {update}$ function of the $\mathsf {StoreProcess}$ for safety and co-safety properties proposed in [16], which are the simplified versions of the general ${\mathsf {StoreProcess}}$ described in Sect. 3.5. Indeed, examining the algorithms, the steps in the algorithm of the $\mathsf {DumpProcess}$ of monitors are algorithmically simple and lightweight from a computational point of view. Regarding the $\mathsf {StoreProcess}$ function for safety and co-safety properties, their most computationally intensive step is their call to their $\mathrm {update}$ function.

Experimental framework. Let us briefly look into the experimental framework, which is depicted in Fig. 8. The Main module uses the module Trace Generator that provides a set of input traces, to test the Store module. The Trace Generator module takes as input the alphabet of actions, the range of possible delays between actions, the desired number of traces, and the increment in length per trace. For example if the number of traces in 5, and increment in length per trace is 100 then 5 traces will be generated, where the first trace is of length 100 and the second trace of length 200 and so on. It returns a set of traces. For each event, the Trace Generator picks an action (from the set of possible actions), and a delay (from the set of possible delays) randomly using methods from the Python random module.

Fig. 8

Experimental framework

The Store module takes as input a property and one trace, and returns the total execution of the $\mathrm {update}$ function to process the given input trace. The TA modeling the property is a UPPAAL [20] model written in XML. The Store module uses the pyuppaal library to parse the UPPAAL model (input property), and the UPPAAL DBM library to implement the $\mathrm {update}$ function.⁴ More details about the implementation of the Store module for safety and co-safety properties are in Appendix 2. The UPPAAL model also contains another automaton representing the sequence of events received by the EM. The Main Test Method sends the sequence to the Store module (using the property), and keeps track of the result returned by the Store module for each trace.

Experiments were conducted on an Intel Core i7-2720QM at 2.20 GHz CPU, with 4 GB RAM, and running on Ubuntu 12.04 LTS. The reported numbers are mean values over 10 runs and are represented in seconds. We have chosen to compute the average values over 10 runs because, for all metrics, with 95 $\%$ confidence, the measurement error was less than 1 $\%.$ For example, referring to Table 1, for safety property ${\varphi _\mathrm{s}^{1.1}},$ the mean value of the total execution time of the $\mathrm {update}$ function is 8.6306 s, and the error is 0.018 s. Thus, with 95 $\%$ confidence, the execution time of $\mathrm {update}$ for input trace of length 10,000 lies within the interval $[8.6126,\,8.6486]$ (s). For the average time per call, as shown in the table, ${\varphi _\mathrm{s}^{1.1}},$ the mean value is 0.863 ms, and the error is 0.005 ms. Thus, with 95 $\%$ confidence, the average time per call to $\mathrm {update},$ for input trace of length 10,000 lies within the interval $[0.858,\,0.868]$ (ms).

Table 1 Performance analysis of enforcement monitors for safety properties

4.1 Performance evaluation of the $\mathrm {update}$ function for safety properties

We describe the properties used in our experiments and discuss the results of the performance analysis. The considered safety properties follow different patterns [21].

Property $\varphi _\mathrm{s}^{1}$ belongs to the absence pattern. It expresses that “There cannot be n or more a-actions in every k time units”, where n is a parameter of the pattern. Following this pattern, the considered properties are $\varphi _\mathrm{s}^{1.1},\,\varphi _\mathrm{s}^{1.2}$ and $\varphi _\mathrm{s}^{1.3},$ each varying in the value of n: $n=2$ for $\varphi _\mathrm{s}^{1.1},\,n=10$ for $\varphi _\mathrm{s}^{1.2},\,n=20$ for $\varphi _\mathrm{s}^{1.3}.$ Property $\varphi _\mathrm{s}^{2}$ belongs to the precedence pattern. It expresses that “A sequence of n a-actions enables action b after a delay of k time units”. Following this pattern, the considered properties are $\varphi _\mathrm{s}^{2.1},\,\varphi _\mathrm{s}^{2.2}$ and $\varphi _\mathrm{s}^{2.3},$ each varying in the value of n: $n=1$ for $\varphi _\mathrm{s}^{2.1},\,n=5$ for $\varphi _\mathrm{s}^{2.2}$, and $n=10$ for $\varphi _\mathrm{s}^{2.3}.$

Results and analysis. Results of the performance analysis of our running example properties are reported in Table 1. The entry $\mathrm {t\_\mathrm {update}}$ indicates the total execution time of the $\mathrm {update}$ function, and the entry $\mathrm {t\_avg}$ is the average time per call. From the results presented in Table 1, as expected for safety properties, we can observe that the time taken per call to $\mathrm {update}$ is independent on the length of the trace. This behavior is as expected: since we update the state of the TA after each event, and after receiving a new event, we explore the possible transitions leading to a good state from the current state. Moreover, from the curves shown in Fig. 9, notice that, for a given trace length, the execution time of $\mathrm {update}$ is similar for the two patterns and their variants in size.

Fig. 9

Length of the input trace (Vs) total execution time of $\mathrm {update}$

4.2 Performance evaluation of the $\mathrm {update}$ function for co-safety properties

We describe the properties used in our experiments and discuss the results of the performance analysis. The considered co-safety properties follow different patterns [21].

Property $\varphi _\mathrm{cs}^{1}$ belongs to the existence pattern [21]. It expresses that “There should be n r-actions, which should be immediately followed by a g-action with a delay of at least k time units”. Following this pattern, the considered properties are $\varphi _\mathrm{cs}^{1.1}$ and $\varphi _\mathrm{cs}^{1.2}$ each varying in the value of n: $n=1$ for $\varphi _\mathrm{cs}^{1.1},$ and $n=5$ for $\varphi _\mathrm{cs}^{1.2}.$

Results and analysis. Results of the performance analysis of our running example properties are presented in Table 2. Entry $\mathrm {t\_\mathrm {update}}$ indicates the execution time of function $\mathrm {update}.$ Entry $\mathrm {t\_avg}$ is the average time per call, and the entry $\mathrm {t\_last}$ is the execution time of $\mathrm {update}$ upon the last event. Note that the execution on the last event is the most time consuming. The considered input traces are generated in such a way that an accepting state is reachable only upon the last event. From the results presented in Table 2, notice that $\mathrm {t\_last}$ and $\mathrm {t\_avg}$ increase with $|tr|.$ This behavior is as expected for a co-safety property because the $\mathrm {update}$ function starts the computation from the initial state for a given input trace. This behavior is also clearly shown by the curves in Fig. 10, showing the total time taken by the $\mathrm {update}$ function versus the length of the input trace. Moreover, notice that, for a given trace length, the execution time of $\mathrm {update}$ is similar for the two properties of the same pattern varying in size.

Fig. 10

For $\varphi _\mathrm{cs}^{1}:$ length of the input trace (Vs) total execution time of $\mathrm {update}$

Table 2 Performance analysis of enforcement monitors for co-safety properties

Remark 11

In case of a co-safety property, the monitor starts to output events only after reading an input sequence which can satisfy the property (after the optimal delays are computed for the input sequence). Once an accepting state is reached, then it is not necessary to invoke the $\mathrm {update}$ and to correct the delays anymore.

4.3 Discussion

On precision. In theory, the delays between actions and the optimal delay computed by the $\mathrm {update}$ function are real numbers. In the implementation, in order to compute optimal delay, we need to set precision.

We use UPPAAL [20] to model the input TA, and some UPPAAL libraries to realize the algorithms. In UPPAAL, only integers can be used to compare the values of clocks in the guards. But, in practice, we may have to use real-numbers to express requirements and timing constraints. This issue can be handled by setting the precision of real-numbers, and representing values on guards with equivalent integers. For example, if we set the precision with four digits after the decimal point, 0.0024 can be represented as 24, and 5.0012 can be represented as 50,012. Note that having a large integer value on a guard such as in $x > 50,000$ is not an issue with region and zone computations, as computation is done on-the-fly. After each event, we check for possible paths from the current state.

On performance and overhead. Assessing the performance of runtime EMs is paramount in a timed context as. Using the experimental results, one can determine the guards and the properties for which the assumptions stated in the introduction hold. Regarding safety properties, one can see that, on the used experimental setup, the computation time of the $\mathrm {update}$ function is below 1 ms. By taking guards with constraints using integers above 0.1 s, one can see that the computation time can be negligible in some sense as the impact on the guard is below 1 %, and makes the overhead of enforcement monitoring acceptable.

5 Related work

Several runtime verification and enforcement approaches are related to the one proposed in this paper. We propose a comparison with approaches for the runtime enforcement of untimed properties (Sect. 5.1), for the runtime verification of timed properties (Sect. 5.2), and runtime enforcement of timed properties (Sect. 5.3)

5.1 Runtime enforcement of untimed properties

Most of the work in runtime enforcement was dedicated to untimed properties (see [9] for a short overview). Schneider introduced security automata as the first runtime mechanism for enforcing safety properties [7]. Then the set of enforceable properties was later refined by Schneider, Hamlen, and Morrisett by showing that security automata were actually restrained by the computational limits exhibited by Viswanathan and Kim [22]: the set of co-recursively enumerable safety properties is a strict upper limit of the power of (execution) EMs defined as security automata. Ligatti et al. [8] later introduced edit-automata as EMs. Edit-automata can either insert a new action by replacing the current input, or suppress it. The set of properties enforced by edit-automata is called the set of infinite renewal properties: it is a super-set of safety properties and contains some liveness properties (but not all). Similar to edit-automata are generic EMs [10] are able to enforce the set of (untimed) response regular properties in the safety-progress classification. Moreover, some variants of edit-automata differ in how they ensure the transparency constraints (see e.g., [23]).

5.2 Runtime verification of timed properties

Several approaches have been proposed for the runtime verification of timed properties. We shall categorize them into (i) rather theoretical efforts aiming at synthesizing monitors (Sect. 5.2.1), and (ii) tools for runtime monitoring of timed properties (Sect. 5.2.2).

5.2.1 Synthesis of timed automata from timed logical formalisms

Bauer et al. propose an approach to runtime verify timed-bounded properties expressed in a variant of timed linear temporal logic (TLTL) [4]. Contrarily to TLTL, the considered logic, TLTL$_{3},$ processes finite timed words and the truth-values of this logic are suitable for monitoring. After reading some timed word u, the monitor synthesized for a TLTL$_{3}$ formula $\varphi$ states the verdict $\top$ (resp. $\bot$) when there is no infinite timed continuation w such that $u\cdot w$ satisfy (resp. does not satisfy) $\varphi .$ Another variant of LTL in a timed context is metric temporal logic (MTL), a dense extension of LTL. Nickovic et al. [3, 19] propose a translation of MTL to timed automata. The translation is defined under the bounded variability assumption stating that, in a finite interval, a bounded number of events can arrive to the monitor. Still for MTL, Thati et al. propose an online monitoring algorithm which works by rewriting of the monitored formula and study its complexity [1]. Basin et al. propose an improvement of the aforementioned approach with a better complexity but considering only the past fragment of MTL [5].

Runtime enforcement of timed properties as presented in this paper is compatible with the previously-described approaches. These approaches synthesize automata-based decision procedures for logical formalisms. Decision procedures synthesized for regular properties can be used as input to our framework.

5.2.2 Tools for runtime monitoring of timed properties

The analog monitoring tool [11] is a tool for monitoring specifications over continuous signals. The input logic of AMT is STL/PSL where continuous signals are abstracted into propositions and operations are defined over signals. Input signal traces can be monitored in an offline or incremental fashion (i.e., online monitoring with periodic trace accumulation).

RT-MaC [24] is a tool for verifying timed properties at runtime. RT-MaC allows to verify timeliness and reliability correctness. Using the time-bound temporal operators provided by the tool, one can specify a deadline after which a property must hold.

LARVA [12, 25] takes as input properties expressed in several notations, e.g., Lustre, duration calculus. Properties are translated to DATE (dynamic automata with timers and events) which basically resemble timed automata with stop watches but also feature resets, pauses, and can be composed into networks. Transitions are augmented with code that modify the internal system state. DATE target only safety properties. In addition, LARVA is able to compute an upper-bound on the overhead induced on the target system. The authors also identify a subset of the duration calculus, called counter-examples traces, where properties are insensitive to monitoring [26].

Our monitors not only differ by their objectives but also by how they are interfaced with the system. We propose a less restrictive framework where monitors asynchronously read the outputs of the target system. We do not assume our monitors to be able to modify the internal state of the target program. The objective of our monitors is rather to correct the timed sequence of output events before this sequence is released to the environment (i.e., outside the system augmented with a monitor).

5.3 Runtime enforcement of timed properties

Matteucci inspires from partial-model checking techniques to synthesize controller operations to enforce safety and information-flow properties using process-algebra [13]. Monitors are close to Schneider’s security automata [7]. The approach targets discrete-time properties and systems are modeled as timed processes expressed in CCS. Compared to our approach, the description of enforcement mechanisms remains abstract, directly restricts the monitored system, and no description of monitor implementation is proposed. Besides, in a general study, Rinard discusses monitoring and enforcement strategies for real-time systems [27], and mentions the fact that enforcement mechanisms could delay input individual events in an input stream when they arrive too early w.r.t. the constraints of the system. In the same way, we consider in our work that an enforcer is time retardant. However, the work in [27] remains at a high-level of abstraction and does not propose any detailed description of enforcement mechanisms.

More recently, Basin et al. [14] proposed a general approach related to enforcement of security policies with controllable and uncontrollable events, investigating enforceability (with complexity results), and how to synthesize enforcement mechanisms for several specification formalisms (automata-based or logic-based). A monitor observes the system and terminates it to prevent violations. Timed properties described in MLTL logic are handled in this work. Discrete time is considered, clock ticks are used to determine the enforceability of an MLTL formula. In our approach, we consider dense time, using the expressiveness of timed automata and efficiency of UPPAAL. Moreover, our enforcement mechanisms may modify the execution of the observed system, and termination is decided if correcting the execution by delaying is not possible.

6 Conclusion and future work

Conclusion. This paper presents a general enforcement monitoring framework for systems with (dense) timing requirements. We showed how to synthesize enforcement mechanisms for any regular timed property (modeled with a timed automaton). We propose adapted notions of enforcement mechanisms that delay input actions in order to satisfy the required property. Enforcement mechanisms are described at several levels of abstraction (enforcement function, monitor, and algorithm), thus facilitating the design and implementation of such mechanisms. We describe how to realize the EM using concurrent processes. We propose a prototype implementation and our experiments demonstrate the feasibility of enforcement monitoring for timed properties.

Future work. Several avenues for future work are opened by this paper.

First, we believe it is important to study and delineate the set of enforceable timed properties. As shown informally by this paper, some timed properties should be characterized as non-enforceable. For this purpose, an enforceability condition should be defined and used to delineate enforceable properties. Such a criterion should ideally also be expressible on timed automata. We conjecture that several enforceability notions exist. Some notions depend on the underlying mechanism used to enforce properties. We believe that there is also one (formalism-independent) enforceability notion that stems only from the physical time constraints faced by enforcement mechanisms.

Note that even for properties which are non-enforceable, the EMs proposed in this paper can be built, which may not be able to correct some input sequences, but their outputs are always sound.

Properties are currently defined with timed automata. We consider synthesizing enforcement mechanisms from more expressive formalisms. For instance, we will consider formalisms such as context-free timed languages (which can be useful for recursive specifications) or introduce data into requirements (which can be useful in some application domains). Implementing efficient EMs is another important aspect and should be done w.r.t. a particular application domain.

We implemented the tool in Python with the objectives of (i) making a quick prototype that shows feasibility of enforcement monitoring in a timed context, and (ii) reusing some existing UPPAAL libraries. In the future, we will consider implementing our EMs in other languages such as C or Java, and we expect even better performance and a more stand-alone implementation.

Alternative enforcement primitives can be afforded to timed retardants, which could be of interest in some application domains. For instance, we could relax the constraint of only augmenting delays of events. For instance, time retardants that delay the total duration of the observation (while being allowed to shorten the delay of some events) have yet to be studied. Suppressing events also can be considered, by erasing some events which are stored in the memory. An event should be suppressed if it is not possible to satisfy the property in the future, whatever is the remainder of the input sequence (i.e., the TA has reached q non-accepting state from which no accepting states can be reached). Formalizing suppression is however quite involved, requiring to redefine relations between input and output sequences which impacts on transparency.

Also related to expressiveness is the question of how the set of timed enforceable properties is impacted when the underlying memory is limited and/or the primitive operations endowed to the monitor are modified.

Appendices

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:

$$\begin{aligned} \begin{array}{ll} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t,\, t^{\prime }\in {\mathbb {R}}_{\ge 0}:\, t\le t^{\prime }\implies E_\varphi (\sigma ,\,t) \preccurlyeq E_\varphi (\sigma ,\,t^{\prime })\quad \mathbf{(Phy1)},\\ \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\,{{\mathrm{time}}}\left( E_\varphi (\sigma ,\,t)\right) \le t\quad \mathbf{(Phy2)}. \end{array} \end{aligned}$$

• 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:

$$\begin{aligned} E_\varphi (\sigma ,\,t) = \begin{array}{cc} \mathrm {obs}\left( \varPi _{1}\left( {{\mathrm{store}}}(\mathrm {obs}(\sigma ,\,t))\right) ,\,t\right) , \end{array} \end{aligned}$$

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).

$$\begin{aligned} \begin{array}{l} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t) \ne \epsilon \wedge E_\varphi (\sigma ,\,t) \models \varphi \\ \quad \implies \exists w_\mathrm{\scriptscriptstyle mx},\quad w \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*}:\\ \quad \;\; w_\mathrm{\scriptscriptstyle mx}= {{\mathrm{max}}}^{\varphi }_{\prec ,\epsilon }\left( E_\varphi (\sigma ,\,t)\right) \\ \quad \wedge E_\varphi (\sigma ,\,t) = w_\mathrm{\scriptscriptstyle mx}\cdot w \\ \quad \wedge {{\mathrm{time}}}(w) = {{\mathrm{min}}}\big \{{{\mathrm{time}}}(w^{\prime }) \mid {{\mathrm{delay}}}(w^{\prime }(1))\ge {{\mathrm{time}}}\left( \sigma _{[1\cdots |E_\varphi (\sigma ,t)|]}\right) - {{\mathrm{time}}}\left( w_\mathrm{\scriptscriptstyle mx}\right) \\ \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \wedge w_\mathrm{\scriptscriptstyle mx}\cdot w^{\prime } \models \varphi \wedge \varPi _{\varSigma }(w^{\prime }) = \varPi _{\varSigma }(w)\big \}. \end{array} \end{aligned}$$

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

$$\begin{aligned} \sigma \cdot \left( \epsilon ,\,{{\mathrm{idle}}}\left( \delta _{1}\right) ,\,\epsilon \right) \cdot \left( \epsilon ,\,{{\mathrm{idle}}}\left( \delta _{2}\right) ,\,\epsilon \right) \cdot \sigma ^{\prime }\quad \mathrm{is\,equivalent\,to}\,\sigma \cdot \left( \epsilon ,\,{{\mathrm{idle}}}\left( \delta _{1}+\delta _{2}\right) ,\,\epsilon \right) \cdot \sigma ^{\prime }, \end{aligned}$$

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)

$$\begin{aligned}&\forall \sigma \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\quad \forall t_{1},\,t_{2},\,t_{3}\in {\mathbb {R}}_{\ge 0}:\, t_{1}\le t_{2}\le t_{3} \implies \mathcal{E}\left( \sigma ,\,t_{1},\,t_{3}\right) \\&\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad = \mathcal{E}\left( \sigma ,\,t_{1},\,t_{2}\right) \cdot \mathcal{E}\left( \sigma ,\,t_{2},\,t_{3}\right) . \end{aligned}$$

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)

$$\begin{aligned} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\,\mathcal{E}(\sigma ,\,t) = \mathcal{E}(\mathrm {obs}(\sigma ,\,t),\,t). \end{aligned}$$

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)

$$\begin{aligned} \begin{array}{l} \forall \sigma ,\,\sigma ^{\prime }\in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\\ \qquad (\sigma ^{\prime }\preceq \sigma \wedge t = {{\mathrm{time}}}(\sigma ^{\prime })) \implies {{\mathrm{config_{in}}}}(\sigma ,\,t) = (\_,\,\_,\,{{\mathrm{time}}}({{\mathrm{last}}}(\sigma ^{\prime })),\,\_,\, \_,\,\_). \end{array} \end{aligned}$$

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)

$$\begin{aligned} \begin{array}{l} \forall \sigma ,\,\sigma _{s},\,\sigma _{c} \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\quad \forall t \in {\mathbb {R}}_{\ge 0},\quad \forall s,\,d,\,m_{t} \in {\mathbb {R}}_{\ge 0},\quad \forall q \in Q:\\ \quad t \ge {{\mathrm{time}}}(\sigma ) \wedge {{\mathrm{config_{out}}}}(\sigma ,\,t)=\left( \sigma _{s},\,\sigma _{c},\,s,\,d,\,m_{t},\,q\right) \\ \quad \quad \implies \forall \sigma _{s}^{\prime }\preceq \sigma _{s},\quad \exists \sigma ^{\prime }_{c} \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\quad \exists s^{\prime }\in {\mathbb {R}}_{\ge 0},\quad \exists m^{\prime }_{t}\in {\mathbb {R}}_{\ge 0},\quad \exists q^{\prime }\in Q:\\ \quad \quad \quad {{\mathrm{config_{out}}}}\left( \sigma ,\,t + {{\mathrm{time}}}\left( \sigma _{s}^{\prime }\right) - d\right) = \left( \sigma _{s}\setminus \sigma _{s}^{\prime },\,\sigma ^{\prime }_{c},\,s^{\prime },\,0,\,m^{\prime }_{t},\,q^{\prime }\right) . \end{array} \end{aligned}$$

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

$$\begin{aligned} \begin{array}{l} \forall \sigma ,\,\sigma _{s},\,\sigma _{c} \in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\quad \forall t \in {\mathbb {R}}_{\ge 0},\quad \forall s,\,d,\,m_{t} \in {\mathbb {R}}_{\ge 0},\quad \forall q \in Q:\\ \quad t \ge {{\mathrm{time}}}(\sigma ) \wedge {{\mathrm{config_{out}}}}(\sigma ,\,t) = \left( \sigma _{s},\,\sigma _{c},\,s,\,d,\,m_{t},\,q\right) \\ \quad \quad \implies \forall \sigma _{s}^{\prime }\in ({\mathbb {R}}_{\ge 0}\times \Sigma )^*,\quad \forall t^{\prime }\in {\mathbb {R}}_{\ge 0}:\\ \quad \quad \quad \quad \sigma _{s}^{\prime }\preceq \sigma _{s}\wedge d\le t^{\prime }\le {{\mathrm{time}}}\left( \sigma _{s}^{\prime }\right) \implies \mathcal{E}(\sigma ,\,t,\,t+t^{\prime }-d) = \mathrm {obs}\left( \sigma _{s}^{\prime },\,t^{\prime }\right) . \end{array} \end{aligned}$$

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:

$$\begin{aligned} \forall \sigma \in \left( {\mathbb {R}}_{\ge 0}\times \varSigma \right) ^{*},\quad \forall t\in {\mathbb {R}}_{\ge 0}:\, E_\varphi (\sigma ,\,t)= \mathcal{E}(\sigma ,\,t). \end{aligned}$$

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.