Yliès Falcone
email: ylies.falcone@inria.fr

Jean-Claude Fernandez
email: jean-claude.fernandez@imag.fr

Laurent Mounier
email: laurent.mounier@imag.fr

What can you Verify and Enforce at Runtime ?

The underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the sets of properties for which runtime analysis approaches can be applied to. This paper presents a unified view of runtime verification and enforcement of properties in the Safety-Progress classification. Firstly, we extend the Safety-Progress classification of properties in a runtime context. Secondly, we characterize the set of properties which can be verified (monitorable properties) and enforced (enforceable properties) at runtime. We propose in particular an alternative definition of "property monitoring" to the one classically used in this context. Finally, for the delineated sets of properties, we define specialized verification and enforcement monitors.

Introduction

In the past decades, we have seen the emergence of a world in which information systems are ubiquitous. System dissemination entails a growing need of confidence. System failures in history showed limits of existing engineering methodologies and enabled the emergence of formal methods [START_REF] Clarke | Formal methods: State of the art and future directions[END_REF]. Ideally, one would like to validate a program prior to its execution. However, static validation methods such as model-checking [START_REF] Emerson | Characterizing correctness properties of parallel programs using fixpoints[END_REF] suffer from limits preventing their use in real large-scale applications. For instance, those techniques are often bound to the design stage of a system and hence they are not shaped to face-off specification evolution. Even when those techniques (e.g., static analysis [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF]) do scale well, they are Send offprint requests to: Yliès Falcone limited by the properties they can check, and may not be able to check interesting behavioral properties. Thus, the verification of some properties, and elimination of some faults, have to be complemented using methods relying on dynamic analysis. In this paper, we are interested in runtime verification and runtime enforcement. These methods, said to be incomplete, operate on one execution of the system. Acknowledging the loss of completeness enables to face-off the limitations of static validation methods.

Runtime-verification [34, [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF][START_REF] Bauer | Comparing ltl semantics for runtime verification[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Havelund | Verify your runs[END_REF] is an effective technique to ensure at execution time that a system meets a desirable behavior. It can be used in numerous application domains, and more particularly when integrating together untrusted software components. A possible approach for runtime verification consists in analyzing a run of the system under scrutiny in an incremental way using a decision procedure called a monitor. This monitor may be generated from a user-provided high level specification (consisting in e.g., a property expressed by temporal logic formula or an automaton). The primary goal of this monitor is to detect violation or satisfaction with respect to the given specification. It can be viewed as a state machine (with an output function) processing an execution sequence (step by step) of the monitored program, and producing a sequence of verdicts (truth values taken from a truth-domain) indicating specification satisfaction or violation. Most research endeavors focused on monitoring safety properties (stating that something bad can never happen), as seen for example in [START_REF] Roşu | Synthesizing monitors for safety properties -this time with calls and returns[END_REF][START_REF] Havelund | Efficient monitoring of safety properties[END_REF]. Moreover, it has been shown by Viswanathan and Kim [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF] that some computability constraints apply to runtime monitors. Considering the monitoring of safety properties, the violation detection mechanism used in the runtime device needs to be effective. Thus, for a safety property to be monitorable it has to be co-recursively enumerable. However, the au-thors of [START_REF] Amorim | Efficient monitoring of ω-languages[END_REF] show that, when monitoring is purposed to detect violations of a property, safety properties are not the only monitorable properties. Recently, a new definition of monitorability was given by Pnueli and Zaks [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF] where monitoring not only detects violations but also satisfactions, and it is proved in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF] that safety and cosafety properties represent only a proper subset of the set of the monitorable properties.

Runtime enforcement is an extension of runtime verification aiming to circumvent property violations. It was initiated by the work of Schneider [START_REF] Schneider | Enforceable security policies[END_REF] on the so-called security automata. In this work the enforcement monitor watches the current execution sequence and halts the underlying program whenever it deviates from the desired property. Schneider announced that security automata are able to enforce the whole class of safety properties. The results in [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF], previously mentioned in the introduction, that impose computability constraints on monitors, also apply to security automata. Thus the known class of enforceable properties with security automata was refined into the class of co-recursively enumerable properties. Later, Hamlen et al. [START_REF] Hamlen | Computability classes for enforcement mechanisms[END_REF] addressed the question of determining, in general, the class of properties enforceable on programs seen as Turing machines. The authors showed that enforcement at runtime can be addressed for co-recursively enumerable properties.

More recently, Ligatti et al. [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF] showed that it is possible to enforce at runtime more than safety properties. Using more powerful enforcement mechanisms called editautomata, it is possible to enforce the larger class of infinite renewal properties. Within the classical safetyliveness dichotomy, the renewal class is a super set of the safety class which contains some liveness properties (but not all). More than simply halting an underlying program, edit-automata can also suppress (i.e., freeze) and insert (frozen) actions in the current execution sequence.

Several tools have been proposed in this context, and in practice there is not always a clear distinction between runtime-verification and runtime-enforcement. For instance a verification monitor may execute an exception handler when detecting an error, hence modifying the initial program execution.

Motivations and contributions. Based on the amount of works published and existing tools now available within the runtime-validation community, it appears that this technique progressed a lot in the last decade and seems now mature enough to address concrete industrial challenges. However, some interesting questions remain about its expressiveness. More precisely, the main questions we consider in this work are the following: what are the classes of properties that can be handled at runtime, and is there a distinct answer for runtime verification and runtime enforcement? These questions are not original in themselves, but we propose here to address them within a unified framework: the Safety-Progress (SP) classification of properties [START_REF] Manna | A hierarchy of temporal properties[END_REF][START_REF] Chang | Characterization of temporal property classes[END_REF]. The contributions of the paper are then the following:

1. to propose a suitable framework for specifying and reasoning about properties in a runtime context; 2. to integrate and improve within this framework some existing expressiveness results related to runtime monitoring [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF][START_REF] Bauer | Comparing ltl semantics for runtime verification[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF], and to propose an alternative definition of the notion of monitorability, leveraging the semantics of finite execution sequences; 3. and to improve some recent results related to property enforcement [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF][START_REF] Falcone | Enforcement Monitoring wrt. the Safety-Progress Classification of Properties[END_REF], giving a more accurate classification of enforceable properties; 4. to get a generic monitor synthesis technique, allowing to produce either a verification or an enforcement monitor from the same property description.

Let us illustrate a bit more the second motivation. Consider a system on which it is possible to evaluate two atomic propositions called p and q. At system runtime, system events are fed to a monitor. Each event is a pair containing the truth-values of p and q. Now let us consider the following requirement: "Either p is always true or q is eventually true". This means that, for the observed sequence of events, either p is evaluated to true on every event, or there exists an event on which q is evaluated to true. Now consider the two following possible executions of the system, represented by their sequences of events of length 2:

-{p, q} • {p, q}: on both events p is true, q is false; -{p, q}•{p, q}: on the first event p is true and q is false, on the second event p and q are false.

After observation of the first sequence of events, one can reasonably state that the property is "currently" true. Thus, if the program execution stops after this observation, the requirement is satisfied. Indeed, p has been always true during the program execution. Conversely, after observing the second sequence of events, one can reasonably state that the property is "currently" false. Indeed, the last observed event does not fulfill the requirement (neither p nor q evaluate to true). We will see in Section 5 that this kind of property is monitorable according to the classical definition of monitorability. Moreover, a monitor built following this definition of monitorability would produce the same verdict for those two sequences, namely a don't know verdict. This situation is undesirable from our point of view. Thus, we will propose an alternative definition of monitorability able to better cope with these kinds of properties, and to give more precise verdicts.

This paper is a revised and extended version of [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF] which appeared in the 9 th international workshop on Runtime Verification. This new version brings the following additional contributions. First, it contains a more comprehensive theoretical basis by revisiting and extending results about the Safety-Progress classification of properties. Moreover, we provide additional results on monitorability. Furthermore, the synthesis of verification and enforcement monitors is given with full details (it was previously sketched). Finally, the presentation has been improved by means of additional examples, corrected results, and complete proofs.

Paper Organization. The remainder of this article is organized as follows. First, Section 2 introduces some preliminary notations used throughout this paper and Section 3 overviews related work on the issues we address. In Section 4, we propose an extension of the Safety-Progress classification of properties in a runtime verification context. Section 5 is dedicated to runtime monitoring, whereas Section 6 is dedicated to runtime enforcement. In both sections we provide some characterizations of the classes of properties that can be handled by these techniques, with respect to the Safety-Progress framework. Then, in Section 7, we show how to obtain runtime verification and enforcement monitors for the delineated sets of properties. Finally, we give some concluding remarks and future work in Section 8.

In order to facilitate the reading of this article, some of the proofs have been sketched. Complete proofs can be found in Appendix.

Preliminaries and notations

This section introduces some background, namely the notions of program execution sequences and program properties.

Sequences and execution sequences

Considering a finite set of elements E, we define notations about sequences of elements belonging to E. A sequence σ containing elements of E is formally defined by a total function σ : I → E where I is either the integer interval [0, n] for some n ∈ N, or N itself (the set of natural numbers). We denote by E * the set of finite sequences over E (partial function from N), by E + the set of non-empty finite sequences over E, and by E ω the set of infinite sequences over E. The set E ∞ def = E * ∪ E ω is the set of all sequences over E. The empty sequence of E is denoted by ǫ E or ǫ when clear from context. The length (number of elements) of a finite sequence σ is noted |σ| and the (i+1)-th element of σ is denoted by σ i . For a finite sequence σ ∈ E * , we may use last(σ) to denote the last element of σ, i.e., σ |σ|-1 . For two sequences σ ∈ E * , σ ′ ∈ E ∞ , we denote by σ • σ ′ the concatenation of σ and σ ′ , and by σ ≺ σ ′ the fact that σ is a strict prefix of σ ′ . The sequence σ is said to be a strict prefix of σ ′ ∈ E ∞ when ∀i ∈ [0, |σ| -1], σ i = σ ′ i and |σ| < |σ ′ |. When σ ′ ∈ E * , we note σ σ ′ def = σ ≺ σ ′ ∨ σ = σ ′ . For σ ∈ E ∞ and n ∈ N, σ •••n is the sub-sequence containing the n + 1 first elements of σ. Also, when |σ| > n, the subsequence σ n••• is the sequence containing all elements of σ but the n first ones. The set of prefixes pref (σ) of a sequence σ ∈ E ∞ is defined as follows. If σ ∈ E * , then pref (σ)

def = {σ ′ ∈ E * | σ ′ σ}. If σ ∈ E ω , then pref (σ) def = {σ ′ ∈ E * | σ ′ ≺ σ}.
The set Pref (X) of prefixes of a set of sequences X is the union of the sets of prefixes of X-sequences: Pref (X) def = σ∈X pref (σ). The set Pref (X, σ) of prefixes of a set of sequences X which are also strict prefixes of a sequence σ ∈ Σ ∞ is: Pref ≺ (X, σ) def = Pref (X) ∩ pref (σ) \ {σ}. The σ-continuations, i.e., the continuations of a sequence σ, are the finite and infinite sequences belonging to the set

{σ ′ ∈ E ∞ | σ ≺ σ ′ }. For σ ′ ∈ E ∞ a σ-continuation, if σ ′ = σ • σ ′′ , then σ ′′ ∈ E ∞ is called an extension of σ.
A program P is considered as a generator of execution sequences. We are interested in a restricted set of operations the program can perform. These operations influence the truth-value of properties the program is supposed to fulfill. Such execution sequences can be made of access events on a secure system to its resources, or kernel operations on an operating system. In a software context, these events may be abstractions of relevant instructions such as variable modifications or procedure calls. These events may also be fed from the underlying program and contain the evaluation of some propositions of the system under scrutiny. We abstract these operations by a finite set of events, namely an alphabet Σ. We denote by P Σ a program for which the alphabet is Σ. The set of execution sequences of P Σ is denoted by Exec(P Σ ) ⊆ Σ ∞ . This set is prefix-closed, i.e., ∀σ ∈ Exec(P Σ ), ∀σ ′ ∈ Σ * , σ ′ σ ⇒ σ ′ ∈ Exec(P Σ ). In the remainder of this article, we use an alphabet Σ.

Properties

Properties as sets of execution sequences. A finitary property (resp. an infinitary property, a property) is a subset of execution sequences of Σ * (resp. Σ ω , Σ ∞ ). Considering a given finite (resp. infinite, finite or infinite) execution sequence σ and a property φ (resp. ϕ, θ), when σ ∈ φ, noted φ(σ) (resp. σ ∈ ϕ, denoted ϕ(σ), σ ∈ θ, noted θ(σ)), we say that σ satisfies φ (resp. ϕ, θ). A consequence of this definition is that properties we will consider are restricted to single execution sequences1 , excluding specific properties defined on power-sets of execution sequences (like fairness, for instance).

Runtime properties. In this paper we will focus on properties to be evaluated at runtime. As stated in the introduction, this means that we would have to consider finite and infinite execution sequences (that a program may produce). A runtime verification technique should address both kinds of sequences in a uniform way. So we introduce a notion of "runtime property" (r -property) as a pair of finite/infinite execution sequence sets2 : Definition 1 (runtime properties). An r -property is a pair (φ, ϕ) ⊆ Σ * × Σ ω . The property φ is called the finitary part of the r -property, whereas ϕ is called the infinitary part of the r -property.

Intuitively, the finitary property φ represents the desirable property that finite execution sequences should fulfill, whereas the infinitary property ϕ is the expected property for infinite execution sequences. Notations for r -properties follow from the notations for finitary and infinitary properties. For an r -property (φ, ϕ), its negation, noted (φ, ϕ), is defined as (Σ * \ φ, Σ ω \ ϕ). Boolean combinations of r -properties are defined in a natural way:

(φ 1 , ϕ 1 ) ∨ (φ 2 , ϕ 2 ) = (φ 1 ∪ φ 2 , ϕ 1 ∪ ϕ 2 ), and (φ 1 , ϕ 1 ) ∧ (φ 2 , ϕ 2 ) = (φ 1 ∩ φ 2 , ϕ 1 ∩ ϕ 2 )
. Considering an execution sequence σ ∈ Exec(P Σ ), we say that σ satisfies (φ, ϕ) when σ ∈ Σ * ∧ φ(σ) ∨ σ ∈ Σ ω ∧ ϕ(σ). For an r -property Π = (φ, ϕ), we note Π(σ) (resp. ¬Π(σ)) when σ satisfies (resp. does not satisfy) (φ, ϕ). The set of prefixes of an r -property Π = (φ, ϕ) is defined as:

Pref (Π) = Pref (φ) ∪ Pref (ϕ).
Intersection between finitary, infinitary properties and r -properties is straightforward and denoted using operator ⊓, e.g., Σ * ⊓(φ, ϕ) = φ.

Evaluation of r-properties. Monitorability, enforceability, and monitor synthesis are based on the evaluation of r -properties by a monitor. Evaluating an execution sequence σ w.r.t. an r -property consists in producing a verdict regarding the current property-satisfaction of σ or future satisfactions of the possible σ-continuations. As a matter of fact, the verdicts produced by monitors are not necessarily usual Boolean values: they are truth-values taken from a truth-domain. A truth-domain is a lattice, i.e., a partially ordered set with an upperbound and a lower-bound. Examples of truth-domains are the classical Boolean domain {true, false} or the realnumber interval [0, 1], or any relevant set of values used for evaluating properties. Considering a truth-domain B, an r -property Π and a finite execution sequence σ, the evaluation of

σ ∈ Σ * w.r.t. Π in B, noted [[Π]] B (σ), is an element of B depending on Π(σ) and satisfaction of σ-continuations w.r.t. Π.
The sets of monitorable and enforceable properties (Sections 5 and 6) rely both upon the truth-domain and evaluation function we consider.

Related Work

This section overviews some related work on the topics we will discuss in this paper 3 . In particular we summa-events verdicts Monitor rize the basic concepts used for runtime verification and runtime enforcement, and we recall the existing results in terms of sets of properties that can be addressed by each of these techniques.

σ |= Π? B Verification ω ∈ B ∞ Π σ ∈ Σ ∞

Runtime verification

Basic concepts. As stated in the introduction, the notion of runtime verification can be formalized by a verification monitor (see Fig. 1) whose behavior consists in translating a sequence of events σ ∈ Σ ∞ into a sequence of verdicts ω ∈ B ∞ , where B is a given truth-domain. This monitor is defined with respect to an r -property Π, and the sequence of verdicts ω is expected to give some information on the evaluation of Π on σ with respect to B. Thus, one of the problems to be addressed is that each evaluation

[[Π]] B (σ •••n ) = ω •••n of a finite se- quence should not only give some relevant information on Π(σ •••n
), but also possibly on Π(σ). In this context several notions of monitorability were proposed in the past, and we review below the most important results.

Monitorability in the sense of [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF]. Viswanathan and Kim gave the first characterization of monitorable properties in [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF]. Monitorable properties were characterized as a strict subset of safety properties defined over infinite sequences. The authors show that, due to the undecidability of some problems, a verification monitor is limited by some computability constraints Moreover, this definition of monitorability was specifically defined for the detection of errors. Thus, the mechanism used for the error detection needs to be effective. Consequently, a property ϕ ⊆ Σ ω was defined to be monitorable if it is a safety property and Σ * \ Pref (ϕ) is recursively enumerable. The authors establish the equality between this set of properties and the class Π 0 1 of the arithmetical hierarchy which is the class of co-recursively enumerable properties.

Monitorability in the sense of [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF]: Pnueli et al. gave a more general notion of monitorable properties relying on the notion of verdict determinacy by a finite sequence. More precisely, considering a finite sequence σ ∈ Σ * , a property θ ⊆ Σ ∞ is negatively determined (resp. positively determined) by an execution sequence σ if σ and each of its possible continuations does not satisfy (resp. does satisfy) θ. Then, θ is σ-monitorable if σ has a continuation s.t. θ is negatively or positively determined by this continuation. Finally, θ is monitorable, if it is σ-monitorable for every σ ∈ Σ * . The idea is that it becomes unnecessary to continue the execution of a θmonitor after reading σ if θ is not σ-monitorable.

In Section 5, we give the corresponding formal definition in the context of r -properties.

Monitorability in the sense of [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]: Bauer et al., inspired from Pnueli's definition of monitorable properties, proposed a slightly different one based on the notion of good and bad prefix introduced in model-checking by Kupferman and Vardi [START_REF] Kupferman | Model checking of safety properties[END_REF]. The intuitive idea is that with monitorable properties it is possible to "detect" a violation or satisfaction of infinitary properties with finite sequences. More precisely, the definition of monitorable properties comes in the following way. Considering an infinitary property ϕ ⊆ Σ ω , a prefix σ is said to be a bad prefix, noted bad _prefix (σ, ϕ) (resp. good prefix, noted good _prefix

(σ, ϕ)) of ϕ if ∀w ∈ Σ ω , ¬ϕ(σ • w) (resp. ∀w ∈ Σ ω , ϕ(σ • w)).
Then, a prefix σ is said to be ugly if it does not have good nor bad continuation, i.e., ¬∃v ∈ Σ ω , bad _prefix

(σ • v, ϕ) ∨ good _prefix (σ • v, ϕ).
Finally, a property is said to be monitorable if it has no ugly prefix, formally:

∀σ ∈ Σ * , ∃v ∈ Σ * , bad _prefix (σ • v, ϕ) ∨ good _prefix (σ • v, ϕ).

About previous characterizations of monitorable properties:

The first characterization of monitorable properties given in [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF] may seem arbitrary. It characterizes the class of monitorable properties directly as a class of properties. However, let us remark that, in this definition a monitor is dedicated to the detection of "bad behaviors" from finite observations. It seems reasonable that a verification monitor is used to detect "good" behaviors as well, e.g., the satisfaction of a desired property. This is actually the idea behind the definition given in [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF]. The last definition, given in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF], is equivalent to the previous one on Σ ω . We will refer to the definition given in [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF] as the classical definition as it was enunciated before the definition in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]. Furthermore, Bauer et al. have shown that, according to this definition, the set of monitorable properties is a strict superset of safety and co-safety properties. These classes of properties are taken from the classical Safety-Liveness classification of properties [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Alpern | Defining liveness[END_REF]. They also gave an example of request/acknowledge property which is not monitorable. Such a property can be framed in the set of response properties (see Section 4) w.r.t. the SP classification (see Example 5 in Section 5).

Runtime enforcement

Basic concepts. In runtime enforcement, the purpose of an enforcement monitor (see Fig. 2) used at runtime is to transform an input sequence σ ∈ Σ ∞ into an output sequence o ∈ Σ ∞ with respect to an r -property Π. The expected constraints on o are (usually) the following: According to this definition, the set of properties that can be enforced at runtime clearly depends on the capabilities of the enforcement mechanism. To this purpose, the authors of [START_REF] Hamlen | Computability classes for enforcement mechanisms[END_REF] proposed a very general classification of enforceable properties: a program is viewed as a Turing machine and the enforcement mechanisms they considered were based respectively on static analysis, program rewriting and runtime enforcement monitors.

Other research efforts [START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF][START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Ligatti | Enforcing Non-safety Security Policies with Program Monitors[END_REF][START_REF] Falcone | Enforcement Monitoring wrt. the Safety-Progress Classification of Properties[END_REF] focused more specifically on runtime enforcement monitors and proposed a characterization of enforceable properties in this context. We summarize these results below.

Security automata and co-recursively enumerable safety properties: Schneider introduced security automata (a variant of Büchi automata) as the first runtime mechanism for enforcing properties in [START_REF] Schneider | Enforceable security policies[END_REF]. The announced set of enforceable properties with this kind of security automata is the set of safety properties. Then, Schneider, Hamlen, and Morrisett refined the set of enforceable properties and showed that these security automata were actually restrained by the computational limits exhibited by Viswanathan and Kim in [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF]. Hence, Schneider, Hamlen, and Morrisett showed that the set of corecursively enumerable safety properties is a strict upper limit of the power of (execution) enforcement monitors defined as security automata [START_REF] Hamlen | Computability classes for enforcement mechanisms[END_REF].

Edit-automata and infinite renewal properties: Ligatti et al. [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Ligatti | Enforcing Non-safety Security Policies with Program Monitors[END_REF] introduced edit-automata as runtime monitors. Depending on the current input and its control state, an edit-automaton can either insert a new action by replacing the current input, or suppress it. The properties enforced by edit-automata are called infinite renewal properties: it is a superset of safety properties and contains some liveness properties (but not all). More precisely, a property θ is said to be an infinite renewal property if each valid infinite sequence σ has an infinite number of valid prefixes:

∀σ ∈ Σ ∞ , θ(σ) ⇒ ∀σ ′ ∈ Σ * , σ ′ ≺ σ ⇒ ∃σ ′′ ∈ Σ * , σ ′ σ ′′ ≺ σ ∧ θ(σ ′′ ).
Shallow History Automata and an information-based lattice of enforceable policies. Fong [START_REF] Philip | Access control by tracking shallow execution history[END_REF] studied the effect of restraining the capacity of the runtime execution monitor and the effect on the enforcement power. Shallow History Automata (SHA) keep as history a set of access events the underlying program made. Fong showed that these automata can enforce a set of properties strictly contained in the set of properties enforceable by Schneider's automata. The result has been generalized by using abstraction mechanisms on an equivalent variant of Schneider's automata. It raised up an information-based lattice of enforceable policies. At the top of this lattice is the set of properties enforceable by security automata (SHA keeps history of all events). At the bottom of this lattice is the set of policies prohibiting a set of events (SHA does not distinguish between prefixes of execution sequences made of the same events). Fong's classification has a practical interest in the sense that it studies the effect of practical programming constraint (limited memory). It also shows that some classical security policies remain enforceable using such shallow automata.

Generic runtime enforcers and response properties:

In previous work [START_REF] Falcone | Enforcement Monitoring wrt. the Safety-Progress Classification of Properties[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF] we introduced a generic notion of enforcement monitor encompassing previous mechanisms and gave a lower-bound on the set of properties they can enforce in the Safety-Progress classification (see Section 4). In this paper, we will show that this bound is tight. Furthermore, in [START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF], we have studied the question of enforcement monitor composition.

Synthesis of monitors

We give a short overview of the works related to the synthesis of monitors. An exhaustive list of works on monitor synthesis is far beyond the scope of this paper. We refer to [34,[START_REF] Leucker | A brief account of runtime verification[END_REF][START_REF] Havelund | Verify your runs[END_REF] (resp. [START_REF] Falcone | You should better enforce than verify[END_REF]) for more information on this topic in runtime verification (resp. runtime enforcement).

For runtime verification: Generally, runtime verification monitors are generated from LTL-based specifications, as seen recently in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Chen | MOP: An Efficient and Generic Runtime Verification Framework[END_REF]. Alternatively, ω-regular expressions have been used as a basis for generating monitors, as for example in [START_REF] Amorim | Efficient monitoring of ω-languages[END_REF].

For runtime enforcement: In [START_REF] Martinelli | Through modeling to synthesis of security automata[END_REF] Martinelli and Matteucci tackle the synthesis of enforcement mechanisms as defined by Ligatti. More generally, the authors consider security automata and edit-automata. The monitor is modeled by an algebraic operator expressed in CCS. The program under scrutiny is then a term Y ⊲ K X where X is the target program, Y the controller program and ⊲ K the operator modeling the monitor, where K is the kind of monitor (truncation, insertion, suppression or edit). The desired property for the underlying system is formalized using µ-calculus. In [START_REF] Matteucci | Automated synthesis of enforcing mechanisms for security properties in a timed setting[END_REF] Matteucci extends the approach in the context of real-time systems. In [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF] we defined transformations for some classes of the safety-progress classification of properties. Those classspecific transformations take as input a Streett automaton recognizing a property and produce an enforcement monitor for this property. In this paper, we will provide a unified class-independent transformation.

The SP classification in a runtime context

This section recalls and extends some results about the Safety-Progress classification of properties [START_REF] Chang | The Safety-Progress Classification[END_REF][START_REF] Chang | Characterization of temporal property classes[END_REF][START_REF] Manna | A hierarchy of temporal properties[END_REF]. In the original papers this classification introduced a hierarchy between regular properties4 defined as sets of infinite execution sequences. We extend the classification with finite-length execution sequences in a conservative way.

Informal description

The Safety-Progress classification is made of four basic classes over execution sequences. Informally, the classes were defined as follows:

safety properties are the properties for which whenever a sequence satisfies a property, all its prefixes satisfy this property; -guarantee properties are the properties for which whenever a sequence satisfies a property, there are some prefixes (at least one) satisfying this property; -response properties are the properties for which whenever a sequence satisfies a property, an infinite number of its prefixes satisfy this property; -persistence properties are the properties for which whenever a sequence satisfies a property, all but finitely many of its prefixes satisfy this property; i.e., a finite number of its prefixes does not satisfy the property.

Furthermore, two extra classes can be defined as finite Boolean combinations (union and intersection) of basic classes.

-The obligation class can be defined as the class obtained by Boolean combinations of safety and guarantee properties. -The reactivity class can be defined as the class obtained by Boolean combinations of response and persistence properties. This is the most general class containing all linear temporal properties [START_REF] Chang | The Safety-Progress Classification[END_REF].

An r -property of a given class is said to be pure when it is a property of none of the other sub-classes. The Safety-Progress classification is an alternative to the more classical Safety-Liveness dichotomy [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Alpern | Defining liveness[END_REF]. Unlike this later, the Safety-Progress classification is a hierarchy and not a partition. It provides a finer-grain classification, and the properties of each class are characterized according to four views [START_REF] Chang | The Safety-Progress Classification[END_REF]: a language-theoretic view, a topological view, a temporal logic view, and an automata-based view. The language-theoretic view describes the hierarchy according to the way each class can be constructed from sets of finite sequences. The topological view characterizes the classes as sets with topological properties. The third vision links the classes to their expression in temporal logic. At last, the automata view gives syntactic characterizations on automata recognizing properties of a given class. We will consider here only the language-theoretic and the automata views dedicated to r -properties.

4.2

The language-theoretic view of r-properties

Construction of r -properties

The language-theoretic view of the Safety-Progress classification is based on the construction of infinitary properties and finitary properties from finitary ones. It relies on the use of four operators A, E, R, P (building infinitary properties) and four operators A f , E f , R f , P f (building finitary properties) applying to finitary properties. In the original classification of Manna and Pnueli, the operators A, E, R, P, A f , E f were introduced. In this paper, we add the operators R f and P f and give a formal definition of all operators. In these definitions ψ is a finitary property over Σ. Definition 2 (Operators A, E, R, P ).

-

A(ψ) = {σ ∈ Σ ω | ∀σ ′ ∈ Σ * , σ ′ ≺ σ ⇒ ψ(σ ′ )}. -E(ψ) = {σ ∈ Σ ω | ∃σ ′ ∈ Σ * , σ ′ ≺ σ ∧ ψ(σ ′ )}. -R(ψ) = {σ ∈ Σ ω | ∀σ ′ ∈ Σ * , σ ′ ≺ σ ⇒ ∃σ ′′ ∈ Σ * , σ ′ ≺ σ ′′ ≺ σ ∧ ψ(σ ′′ )}. -P (ψ) = {σ ∈ Σ ω | ∃σ ′ ∈ Σ * , ∀σ ′′ ∈ Σ * , σ ′ ≺ σ ′′ ≺ σ ⇒ ψ(σ ′′ )}.
A(ψ) consists of all infinite words σ s.t. all prefixes of σ belong to ψ. E(ψ) consists of all infinite words σ s.t. some prefixes of σ belong to ψ. R(ψ) consists of all infinite words σ s.t. infinitely many prefixes of σ belong to ψ. P (ψ) consists of all infinite words σ s.t. all but finitely many prefixes of σ belong to ψ.

The operators A f , E f , R f , P f build finitary properties from finitary ones. Based on these operators, each class can be seen from the language-theoretic view. Definition 4. Π = (φ, ϕ) is defined to be:

Definition 3 (Operators

A f , E f , R f , P f ). -A f (ψ) = {σ ∈ Σ * | ∀σ ′ ∈ Σ * , σ ′ σ ⇒ ψ(σ ′ )}. -E f (ψ) = {σ ∈ Σ * | ∃σ ′ ∈ Σ * , σ ′ σ ∧ ψ(σ ′ )}. -R f (ψ) = {σ ∈ Σ * | ψ(σ) ∧ ∀n ∈ N, ∃σ ′ ∈ Σ * , σ ≺ σ ′ ∧ |σ ′ | ≥ n ∧ ψ(σ ′ )}. -P f (ψ) = {σ ∈ Σ * | ψ(σ) ∧ ∃σ ′ ∈ Σ * , σ σ ′ ∧ ∀n ∈ N, ∃σ ′′ ∈ Σ * , |σ ′′ | = n ∧ ψ(σ ′ • σ ′′ )}. A f (ψ)
-A safety r -property if Π = (A f (ψ), A(ψ)) for some finitary property ψ. That is, all prefixes of a finite word σ ∈ φ or of an infinite word σ ∈ ϕ belong to ψ.

-A guarantee r -property if Π = (E f (ψ), E(ψ)) for some finitary property ψ. That is, each finite word σ ∈ φ or infinite word σ ∈ ϕ is guaranteed to have some prefixes (at least one) belonging to ψ.

-A response r -property if Π = (R f (ψ), R(ψ)) for some finitary property ψ. That is, each finite word σ ∈ φ or infinite word σ ∈ ϕ recurrently has (infinitely many) prefixes belonging to ψ.

-A persistence r -property if Π = (P f (ψ), P (ψ)) for some finitary property ψ. That is, each finite word σ ∈ φ or infinite word σ ∈ ϕ persistently has (continuously from a certain point on) prefixes belonging to ψ.

In all cases, we say that Π is built over ψ. Furthermore, obligation (resp. reactivity) r -properties are obtained by Boolean combinations of safety and guarantee (resp. response and persistence) r -properties.

Given a set of events Σ, Safety(Σ) (resp. Guarantee(Σ), Obligation(Σ), Response(Σ), Persistence(Σ)) designates the set of safety (resp. guarantee, obligation, response, persistence) r -properties defined over Σ.

We illustrate in the following example the construction of infinitary properties from finitary ones (described as regular expressions) for each of the four operators.

Example 1 (Construction of infinitary and finitary properties from finitary ones -r-properties). We consider a client-server application, with a set of observable events Σ ⊆ {r, g, d} where r denotes a client request of a given resource and g (resp. d) denotes a corresponding grant (resp. deny) of this resource provided by the server.

-For the finitary property

ψ = ǫ + r + • g * , A f (ψ) = ǫ + r + • g * , A(ψ) = r ω + r + • g ω , Π 1 = (A f (ψ), A(ψ))
is a safety r -property. This language contains all the words that have either only occurrences of r or a finite number of occurrences of r (at least one) followed only by occurrences of g. According to this property a resource should be requested at least once to be granted, and, when granted once, it should not be requested anymore. -For the finitary property ψ

= r + • g, E f (ψ) = r + • g • Σ * , E(ψ) = r + •g•Σ ω , Π 2 = (E f (ψ), E(ψ)
) is a guarantee r -property. This property tells that the client will issue some requests and will receive a positive answer later on. -For the finitary property

ψ = g + (r • g) * , R f (ψ) = (r • g) * , R(ψ) = (r • g) ω , Π 3 = (R f (ψ), R(ψ)
) is a response r -property. This language contains all the words that have infinitely many occurrences of r • g. This property tells that clients will repeatedly send requests and receive back a positive answer (the pattern r • g can be seen here as a transaction). -For the finitary property

ψ = g + r • g • (r + r • g) * , P f (ψ) = r • g • (r + r • g) * , P (ψ) = r • g • (r + r • g) ω , Π 4 = (P f (ψ), P (ψ)
) is a persistence r -property. This language contains all the words starting with r • g • r and ending with occurrences of r + r • g. According to this property, after a first granted resource, at some point this resource should be granted forever.

Some useful facts about the language view

Now, we give some useful facts about r -properties in the language view. Those facts will be used in the remainder when characterizing the set of monitorable properties. Basic classes were defined in a constructive fashion. It is sometimes interesting to have a direct characterization for the properties of those classes. The following property gives a characterization for safety and guarantee r -properties. The proof is a direct adaptation of the proof given in [START_REF] Chang | The Safety-Progress Classification[END_REF].

Property 1 (Characterization of safety and guarantee r -properties). An r -property

Π = (φ, ϕ) is -a safety iff Π = (A f (Pref (φ)), A(Pref (ϕ))), -a guarantee iff Π = E f (Pref (φ)), E(Pref (ϕ)) .
We expose the closure of safety and guarantee r -properties as a straightforward consequence of definitions of safety and guarantee r -properties.

Property 2 (Closure of r -properties). Considering an r -property Π = (φ, ϕ) defined over an alphabet Σ built from a finitary property ψ, the following facts hold:

1 If Π is a safety r -property, all prefixes of a sequence belonging to Π also belong to

Π. That is, ∀σ ∈ Σ ∞ , Π(σ) ⇒ ∀σ ′ ≺ σ, Π(σ ′ ). 2 If Π is a guarantee r -property, all continuations of a finite sequence belonging to Π also belong to Π. That is, ∀σ ∈ Σ * , Π(σ) ⇒ ∀σ ′ ∈ Σ ∞ , Π(σ • σ ′ ).
Proof. The proof can be found in Appendix A.1.1, it uses the definitions of the operators A f , A, E f , E. ⊓ ⊔

The following lemma (inspired from [START_REF] Chang | The Safety-Progress Classification[END_REF]) provides a decomposition of each obligation properties in a normal form.

Lemma 1. Any obligation r-property can be represented as the intersection

k i=1 (Safety i ∪ Guarantee i )
for some k > 0, where Safety i and Guarantee i are respectively safety and guarantee r-properties. We refer to this presentation as the conjunctive normal form of obligation r-properties.

When an r -property Π is expressed as ∩ k i=1 (Safety i ∪ Guarantee i ), Π is said to be a k-obligation r -property. The set of k-obligation r -properties (with k ≥ 1) is denoted k-Obligation(Σ). Similar definitions and properties hold for reactivity r -properties which are expressed by Boolean combinations of response and persistence rproperties.

The automata view of r-properties

For the automata view of the Safety-Progress classification, we follow [START_REF] Chang | The Safety-Progress Classification[END_REF] and define r -properties using Streett automata. Furthermore, for each class of the Safety-Progress classification it is possible to syntactically characterize a recognizing finite-state automaton. Moreover, we introduce transformations that take a deterministic finite-state automaton and a "modification pattern" so as to obtain a Streett automaton. These transformations are the representatives in the automata view of the operators defined in the language view.

Streett automata

We define a variant of deterministic and complete Streett automata (introduced in [START_REF] Streett | Propositional dynamic logic of looping and converse[END_REF] and used in [START_REF] Chang | The Safety-Progress Classification[END_REF]) for property recognition 5 . These automata process events and decide properties of interest. We add to original Streett automata a finite-sequence recognizing criterion in such a way that these automata uniformly recognize r -properties.

Definition 5 (Streett automaton).

A deterministic finite-state Streett automaton is a tuple (Q, q init , Σ, -→, {(R 1 , P 1 ), . . . , (R m , P m )}) defined relatively to a set of events Σ. The set Q is the set of automaton states, q init ∈ Q is the initial state. The function -→: Q × Σ → Q is the (complete) transition function. In the following, for q, q ′ ∈ Q, e ∈ Σ we abbreviate -→ (q, e) = q ′ by q e -→ q ′ . The set {(R 1 , P 1 ), . . . , (R m , P m )} is the set of accepting pairs, for all i ≤ n, R i ⊆ Q are the sets of recurrent states, and P i ⊆ Q are the sets of persistent states.

We refer to an automaton with m accepting pairs as an m-automaton. When m = 1, a 1-automaton is also called a plain-automaton, and we refer to R 1 and P 1 as R and P . Moreover, for σ = σ 0 • • • σ n-1 a word over Σ of length n and q, q ′ ∈ Q A two states, we note

q σ -→ q ′ when ∃q 1 , . . . , q n-2 ∈ Q A , q σ0 -→ q 1 ∧ . . . ∧ q n-2 σn-1 -→ q ′ . In the following A = (Q A , q A init , Σ, -→ A , {(R 1 , P 1 ), . . . , (R m , P m )}) designates a deterministic finite state Streett m- automaton.
For q ∈ Q A , Reach A (q) is the set of reachable states from q with at least one transition in A (denoted Reach(q) when clear from context), that is

Reach A (q) def = {q ′ ∈ Q A | ∃σ ∈ Σ + , q σ -→ A q ′ }. For σ ∈ Σ ∞ , the run of σ on A is the sequence of states involved by the execution of σ on A. It is formally defined as run(σ, A) = q 0 • q 1 • • • where ∀i, (q i ∈ Q A ∧ q i σi -→ A q i+1 ) ∧ q 0 = q A init .
The trace resulting in the execution of σ on A is the unique sequence (finite or not) of tuples (q 0 , σ 0 , q 1 )

• (q 1 , σ 1 , q 2 ) • • • where run(σ, A) = q 0 • q 1 • • • .
For an execution sequence σ ∈ Σ ω on a Streett automaton A, we define vinf (σ, A), as the set of states appearing infinitely often in run(σ, A). It is formally defined as follows: vinf (σ, A)

def = {q ∈ Q A | ∀n ∈ N, ∃m ∈ N, m > n ∧ q = q m with run(σ, A) = q 0 • q 1 • • • }.
For a Streett automaton, the notion of acceptance condition is defined using the accepting pairs. Definition 6 (Acceptance condition for infinite sequences). For σ ∈ Σ ω , we say that

A accepts σ if ∀i ∈ [1, m], vinf (σ, A) ∩ R i = ∅ ∨ vinf (σ, A) ⊆ P i .
To deal with r -properties we need to also define an acceptance criterion for finite sequences: a finite sequence is accepted by a Streett automaton if and only if it terminates on a distinguished state R i or P i for each accepting pair i.

Definition 7 (Acceptance condition for finite sequences). For a finite-length execution sequence

σ ∈ Σ * s.t. |σ| = n, we say that the m-automaton A accepts σ if (∃q 0 , . . . , q n ∈ Q A , run(σ, A) = q 0 • • • q n ∧ q 0 = q A init and ∀i ∈ [1, m], q n ∈ P i ∪ R i ).

The hierarchy of automata

An interesting feature of Streett automata is that the class of properties they recognize can be easily characterized by some syntactic considerations.

-A safety automaton is a plain-automaton s.t. R = ∅ and there is no transition from a state q ∈ P to a state q ′ ∈ P . -A guarantee automaton is a plain-automaton s.t. P = ∅ and there is no transition from a state q ∈ R to a state q ′ ∈ R.

-An m-obligation automaton is an m-automaton s.t. for each i in [1, m]:
-there is no transition from q ∈ P i to q ′ ∈ P i , -there is no transition from q ∈ R i to q ′ ∈ R i . -A response automaton is a plain-automaton s.t. P = ∅.

-A persistence automaton is a plain-automaton s.t. R = ∅. -A reactivity automaton is any unrestricted automaton.

The syntactic restrictions are illustrated in Fig. 4: shapes of Streett automata for basic classes are depicted. One may remark that these syntactic restrictions hold for the automata represented in Fig. 3.

Automata and properties. We now link Streett automata to r -properties.

Definition 8 (Automata and r -properties). We say that a Streett automaton A defines an r -property (φ, ϕ) ∈ 2 Σ * ×Σ ω if and only if the set of finite (resp. infinite) execution sequences accepted by A is equal to φ (resp. ϕ), which is noted L(A) = (φ, ϕ). Conversely, an r -property (φ, ϕ) ∈ 2 Σ * ×Σ ω is said to be specifiable by an automaton A if the set of finite (resp. infinite) execution sequences accepted by the automaton A is φ (resp. ϕ).

Example 2 (Streett Automata). In Fig. 3 are represented Streett plain-automata for the properties presented in Example 1.

-A Π1 is a safety automaton, its set of recurrent states is empty, its set of persistent states is P = {1, 2, 3}. A finite sequence is accepted if its run ends in either states 1, 2 or 3, meaning that, if a grant happened there was at least one request previously. An infinite sequence is accepted if the only states visited infinitely often are states 1, 2 or 3, meaning that requests have been made and they were followed by only grants.

-A Π2 is a guarantee automaton, its set of persistent states is empty, its set of recurrent states is R = {3}. A finite sequence is accepted if its run ends in state 3. An infinite sequence is accepted if the state 3 is visited infinitely often. In both cases, it means that requests have been issued and then have been granted.

-A Π3 is a response automaton, its set of persistent states is empty, its set of recurrent states is R = {1}. A finite sequence is accepted if its run ends in state 1, meaning that every request has been followed by a grant (in this order). An infinite sequence is accepted if it visits the state 1 infinitely often, meaning that this infinite sequence contains a succession of action sequences "one request followed by one grant".

-A Π4 is a persistence automaton, its set of recurrent states is empty, its set of persistent states is P = {3, 4}. A finite sequence is accepted if its run ends in state 3 or 4, meaning that a first successful request has been made and, after that, the user performs only successful requests (if he makes a requests, this request is granted). An infinite sequence is accepted if it visits infinitely often only states 3 and 4, meaning that after a first successful request all user's requests have been granted. In Section 4.5 we link the syntactic characterizations on the automata to the semantic characterization of the properties they specify.

From a DFA to a Streett automaton

We now introduce four transformations allowing to obtain a Streett automaton, given a deterministic finitestate automaton and a "pattern" for this underlying property. These patterns are inspired from the different classes of the Safety-Progress hierarchy. These simple transformations correspond, in the automata view, to the operators in the language view and the temporal modalities in the logical view 6 . We start by first defining those transformations and then prove their soundness.

A deterministic finite-state automaton (DFA) [START_REF] John | Introduction to Automata Theory, Languages, and Computation[END_REF], is given relatively to an alphabet Σ, and is here formally defined as a tuple

(Q, q init , -→, F ) where Q is a finite set of states, q init ∈ Q is the initial state, -→: Q × Σ → Q is the transition function, and F ⊆ Q is the set of accepting states.
Definitions of the transformations. In the following definitions,

A ψ = (Q A ψ , q A ψ init , -→ A ψ , F A ψ )
designates a complete DFA recognizing a finitary regular property ψ. We define a transformation for each basic class of the hierarchy.

Synthesis of safety automata. For this class of r -properties, the transformation is defined as follows:

6 i.e., operators A, E, R, P (and their finitary versions) of the language view and the temporal modalities , ♦ , ♦ , ♦ of the logical view.

Definition 9 (DFA to Streett safety automaton). The transformation of

A ψ into a Streett safety automa- ton is DFA2S_Saf(A ψ ) = (Q A Π , q A Π init , → A Π , {(∅, P )}
) and defined by:

-Q A Π = F A ψ ∪ {sink }, where sink / ∈ Q A ψ , -q A Π init = q A ψ init if q A ψ init ∈ F A ψ
, and sink otherwise, -→A Π is defined as the smallest relation verifying:

-q e -→A Π q ′ if q ∈ F A ψ ∧ q ′ ∈ F A ψ ∧ q e -→A ψ q ′ (TSafe1) -q e -→A Π sink if ∃q ′ ∈ Q A ψ , q ′ / ∈ F A ψ ∧ q e -→A ψ q ′ (TSafe2), -∀e ∈ Σ, sink e -→A Π sink (TSafe3), -P = ReachA Π (q A Π init ) \ {sink }, (m = 1).
One can remark that the resulting automaton is indeed a Streett safety automaton since R = ∅ and there is no transition from the states in P to the states in P . This transformation adds a sink state and modifies the transition function in order to redispatch the transitions outgoing from accepting states to the sink state. Furthermore, the transitions outgoing from a non-accepting state have been removed. The set of persistent states is the set of accepting states of the DFA. Moreover, according to the syntactic restrictions of the obtained Streett safety automata, the following property holds: for a sequence σ ∈ Σ ω and an automaton resulting of the transformation

A Π , if sink ∈ vinf (σ, A Π ), then vinf (σ, A Π ) = {sink }; else vinf (σ, A Π ) ⊆ P .
Synthesis of Streett guarantee automata. For this class of r -properties, the transformation is defined as follows:

Definition 10 (DFA to Streett guarantee automaton). The transformation of A ψ into a Streett guarantee automaton is

DFA2S_Guar(A ψ ) = (Q A Π , q A Π init , → A Π , {(R, ∅)}
) and defined by: q = qo qi = q l qj Fig. 5. Principle for tagging recurrent states in DFA2S_Res

-Q A Π is the smallest subset of Q A ψ containing the reachable states from the initial state q A Π init with -→A Π (defined below),

-q A Π init = q A ψ init , -→A Π is defined as the smallest relation verifying: -q e -→A Π q if ∃q ′ ∈ Q A ψ , q e -→A ψ q ′ ∧q ∈ F A ψ (TGuar1), -q e -→A Π q ′ if q / ∈ F A ψ ∧ q e -→A ψ q ′ (TGuar2), -R = F A ψ , (m = 1).
One may remark that the resulting automaton is indeed a Streett guarantee automaton since P = ∅ and there is no transition from the R-states to the R-states. This automaton may not be minimal regarding the number of R-states. They can be merged into one unique state since they are all equivalent w.r.t. property recognition. This transformation modifies the transition function in the following manner: outgoing transitions from the accepting states (to an accepting state or not) are modified into a loop on the same state. Indeed, when a run reaches a state in F , this suffix suffices in order to satisfy the guarantee property. The initial state is not modified, and the set of states of the Streett automaton is defined as the smallest set of reachable states from the initial state with the new transition function.

Synthesis of Streett response automata. For this class of r -properties, the transformation is defined as follows:

Definition 11 (DFA to Streett response automaton). The transformation of A ψ into a Streett response automaton is

DFA2S_Resp(A ψ ) = (Q A Π , q A Π init , → A Π , {(R, ∅)}
) and defined by:

-Q A Π = Q A ψ , -q A Π init = q A ψ init , -→A Π =→A ψ , -R = {q ∈ F A ψ | ∃l > 0, ∃q0, . . . , q l ∈ Q A ψ , (1) ∧ (2) } ∪ {q ∈ F A ψ | q -→A ψ q}, where ∀j ∈ [0, l -1], qj -→A ψ qj+1 (1) ∃i ∈ [0, l], ∃j ∈ [i, l -1], qj ∈ F A ψ ∧ qi = q l ∧ q0 = q (2)
The resulting automaton is indeed a Streett response automaton since P = ∅. This transformation does not modify the set of states nor the transition function. It marks as recurrent states (cf. Fig. 5) every accepting state of the DFA s.t. it is possible from this state to reach a cycle containing at least one accepting state. q = qo qi = q l qi+1 q l-1 Fig. 6. Principle for tagging persistent states in DFA2S_Per

Synthesis of Streett persistence automata. For this class of r -properties, the transformation is defined as follows:

Definition 12 (DFA to Streett persistence automaton). The transformation of A ψ into a Streett persistence automaton is

DFA2S_Per(A ψ ) = (Q A Π , q A Π init , → A Π , {(∅, P )}
) and defined by:

-Q A Π = Q A ψ , -q A Π init = q A ψ init , -→A Π =→A ψ , -P = {q ∈ F A ψ | ∃l > 0, ∃q0, . . . , q l ∈ Q A ψ , (1) ∧ (3) } ∪ {q ∈ F A ψ | q -→A ψ q}, where ∃i ∈ [0, l], ∀j ∈ [i, l -1], qj ∈ F A ψ ∧ qi = q l ∧ q0 = q (3)
The resulting automation is indeed a Streett persistence automaton since R = ∅. This transformation does not modify the set of states nor the transition function. It marks (cf. Fig. 6) as persistent state every accepting state of the DFA from which it is possible to reach a cycle of accepting states.

Soundness of the transformations. Given a finitary property ψ, defining a regular language over an alphabet Σ and specified by a DFA A ψ , the safety (resp. guarantee, response, persistence) r -property (X f (ψ), X(ψ)) where X ∈ {A, E, R, P } is specified by the Streett automaton obtained by the transformation DFA2S specific to safety (resp. guarantee, response, persistence) properties. This is stated formally by the following theorem:

Theorem 1 (Soundness of the transformations of DFAs to Streett automata). The transformation DFA2S _Saf (resp. DFA2S _Guar , DFA2S _Resp, DFA2S _Per ) in the automata view "corresponds" to the operator A f and A (resp. E f and E, R f and R, P f and P ) in the language view. Formally, when L(A ψ ) = ψ,

A Π = DFA2S _Saf (A ψ ) ⇒ L(A Π ) = (A f (ψ), A(ψ)) A Π = DFA2S _Guar (A ψ ) ⇒ L(A Π ) = (E f (ψ), E(ψ)) A Π = DFA2S _Resp(A ψ ) ⇒ L(A Π ) = (R f (ψ), R(ψ)) A Π = DFA2S _Per (A ψ ) ⇒ L(A Π ) = (P f (ψ), P (ψ))
Proof. Proofs are conducted for each class of properties and the associated transformation by using the acceptance criteria and examining runs of accepted sequences. The complete proof can be found in Appendix A.1.2. ⊓ ⊔ Remark 1. Let us remark that these transformations may entail a loss of information. It is in general not possible to find again the finitary language from which a Streett automaton has been built. Consider for example the Streett guarantee automaton represented on Fig. 3. There exists an infinite number of finitary languages from which this automaton can be constructed. Indeed, to obtain them, it suffices to re-transform this Streett automaton into a minimal DFA by forgetting accepting pairs and changing the R-state into an accepting state. Then, from this accepting state, we can add arbitrary transitions. The automata produced by doing so will always be transformed by DFA2S _Guar into A Π2 .

Characterizing states of Streett automata

To better identify particular execution sequences on a Streett automaton we characterize some subsets of its states in terms of reachability of distinguished states. More precisely, the set

P A = {Good A , Good A c , Bad A c , Bad A } is a partition of Q A , s.t. Good A , Good A c , Bad A c , Bad A designate
respectively the good (resp. currently good, currently bad, bad) states. The set P A is defined as follows:

q is in Good A iff it terminates an accepted sequence and every sequence starting from q is accepted:

Good A def = {q ∈ m i=1 (Ri∪Pi) | ReachA(q) ⊆ m i=1 (Ri∪Pi)}; -q is in Good A
c iff it terminates an accepted sequence and there exist non accepted sequences starting from q:

Good A c def = {q ∈ m i=1 (Ri∪Pi) | ReachA(q) ⊆ m i=1 (Ri∪Pi)}; -q is in Bad A
c iff it terminates a non accepted sequence and there exist accepted sequences starting from q:

Bad A c def = {q ∈ m i=1 (Ri ∩Pi) | ReachA(q) ⊆ m i=1 (Ri ∩Pi)}; -q is in Bad A iff
it terminates a non accepted sequence and every sequence starting from q is not accepted:

Bad A def = {q ∈ m i=1 (Ri ∩Pi) | ReachA(q) ⊆ m i=1 (Ri ∩Pi)}.
The subsets are illustrated for basic classes in Fig. 7.

Example 3 (Characterization of Streett automata states).

We illustrate the characterization on the states of the Streett automata presented in Example 2:

-

Bad A Π1 = {4}, Good A Π1 c = {1, 2, 3}, -Bad A Π2 = {4}, Bad A Π2 c = {1, 2}, Good A Π2 = {3}, -Bad A Π3 = {3}, Bad A Π2 c = {2}, Good A Π3 c = {1}, -Bad A Π4 = {5}, Bad A Π4 c = {1, 2, 6}, Good A Π4 c = {3, 4}.
Remark 2. For a Streett automaton A Π , all states in Bad A Π (resp. Good A Π ) are equivalent w.r.t. property recognition -they can be merged into one single state. This characterization of states will be useful in the following sections when characterizing monitorable properties and when synthesizing monitors.

Summary

A graphical representation of the Safety-Progress hierarchy of properties is depicted in Fig. 8. A link between two classes means that the higher class contains strictly

(A f (ψ), A(ψ)) P = ∅, R R (E f (ψ), E(ψ)) (R f (ψ), R(ψ)) (P f (ψ), P (ψ)) P i P i , R i R i i [Safety i ∪ Guarantee i ] R = ∅ i [Response i ∪ Persistence i ] P = ∅
ψ ⊆ Σ * A (DFA) r -property (X f (ψ), X(ψ)) DFA2S _X (A) X ∈ {A, E, R, P } X ∈ {Saf ., Guar .,
Resp., Persit.} the lower one. Furthermore, for each class, we have recalled and uniformly extended the characterizations in the language-theoretic and automata views.

In Table 1 is represented each "basic block", i.e., the element used to build an r -property. In the language view, r -properties are built from a finitary language ψ, and using operators X f , and X, with X ∈ {A, E, R, P }. In the automata view, a finite-state automaton is transformed, by one of the transformations DFA2S specific to a class of properties, into a Streett automaton which recognizes (X f (ψ), X(ψ)) according to the class of properties.

Remark 3. It is worth noticing that property interpretation of finite sequences extends to infinite sequences in a consistent way, depending on the class of properties under consideration: -for a persistence property Π, ¬(

-for a safety property Π, ∀i ∈ N, Π(σ •••i ) ⇒ Π(σ), -for a guarantee property Π, ∃i ∈ N, Π(σ •••i ) ⇒ ¬Π(σ), -for a response property Π, ∞ ∃ i ∈ N, Π(σ •••i ) ⇒ Π(σ), P Good P Goodc P Bad R Good R Bad R Badc R Good R Goodc R Bad
∞ ∃ i ∈ N, ¬Π(σ •••i )) ⇒ ¬Π(σ).

Monitorability w.r.t. the SP classification

As stated in the introduction, studying the question of monitorability amounts to studying the expressiveness of runtime verification, i.e., characterizing the classes of properties that can be verified at runtime. In this section we first recall and extend existing monitorability results in the Safety-Progress classification of properties. Second, we propose to parameterize the classical definition with a truth-domain. Third, we propose an alternative definition of monitorability and characterize monitorable properties according to this new definition.

In fact, characterizing the set of "monitorable" properties depends on several parameters: the property semantics for finite sequences, the set of monitor verdicts we consider, and the exact definition of monitoring.

Monitorable properties according to the classical definition of monitorability

We express the classical definition of monitorability given by Pnueli and Zaks in the SP framework introduced in the previous section. Then, we characterize the set of monitorable properties according to this classical definition.

The classical definition of monitorability

The main objective of monitoring, in its classical definition, is to evaluate an (infinitary) property ϕ on a possibly infinite execution sequence from one of its finite prefix. Intuitively, the idea is to be able to detect verdicts, i.e., find an evaluation, w.r.t. an infinitary property, from a finite observation of a system behavior. This is formalized as follows for r -properties: Definition 13 (Positive/Negative determinacy of an r -property [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF]). Let σ ∈ Σ * , an r -property Π ⊆ Σ * × Σ ω is said to be:

-negatively determined by σ if ∀µ ∈ Σ ∞ , ¬Π(σ • µ); -positively determined by σ if ∀µ ∈ Σ ∞ , Π(σ • µ).
An r -property is negatively (resp. positively) determined if every possible future continuation (finite or infinite) does not (resp. does) satisfy the property. The practical meaning is the following: when a monitor observes a system in order to check a property, if this property is negatively or positively determined, then the observation of the system can be stopped. In this case, a monitor emits the verdict ⊥ (resp. ⊤) after reading σ if the property is negatively (resp. positively determined) by σ. The obtained verdict is definitive. In others cases, a monitor issues the value "?", meaning that no definitive verdict can be produced. Definition 14 (Monitorable r -properties, "classical" definition [START_REF] Pnueli | PSL model checking and run-time verification via testers[END_REF]). An r -property Π is:

σ-monitorable, if there exists a (finite

) µ ∈ Σ * s.t. Π is positively or negatively determined by σ • µ; -monitorable, if it is σ-monitorable for every σ ∈ Σ * .
The set of monitorable properties, according to the classical definition is noted MP c . An r -property is monitorable if, for any execution sequence that can be observed, a possible continuation of this sequence determines negatively or positively the property. One can notice that the classical definition of monitorability is bound to an implicit 3-valued truth-domain {⊥, ?, ⊤} where the truth-values are issued by a monitor as described previously.

Remark that the classical definition of monitorability is hard to use in practice. So a characterization of monitorable properties is needed in practice.

Characterization of monitorable properties according to the classical definition

One of our first objectives is to characterize the subset of monitorable properties within the Safety-Progress classification.

We first enunciate a lemma that will be used later on. This lemma states that the set of MP c -monitorable properties is closed under Boolean operations.

Lemma 2 (Closure of monitorable properties under boolean operations). Given two r-properties Π 1 , Π 2 , we have:

Π 1 , Π 2 ∈ MP c ⇒ Π 1 ∧ Π 2 ∈ MP c , Π 1 , Π 2 ∈ MP c ⇒ Π 1 ∨ Π 2 ∈ MP c , Π 1 ∈ MP c ⇒ ¬Π 1 ∈ MP c .
Proof. The complete proof is given in Appendix A. We are now able to establish that the set of monitorable properties according to the classical definition strictly contains the set of obligation properties.

Theorem 2 (Obligation(Σ) ⊂ MP c ). The obligation properties are strictly contained in the set of monitorable properties.

Proof. The formal proof can be found in Appendix A.2.2 and uses the following facts:

-Safety and guarantee properties are monitorable.

-The set of obligation properties is the union of the sets of k-obligation properties for k ≥ 1 (Lemma 1).

-Union and intersection of two monitorable properties are monitorable (Lemma 2).

-Example 6 shows that the inclusion is strict. ⊓ ⊔ Thus, we have extended the previous bound established by Bauer et al. in [3] 7 stating that

Safety(Σ) ∪ Guarantee(Σ) ⊂ MP c .
Indeed, the set of obligation properties is a strict super set of the union of safety and guarantee properties.

Example 4 (Classical monitoring of an obligation property). We go back to the example presented in the introduction, defined using two atomic propositions p or q, stating that p should always hold or q should eventually hold. This is a 1-obligation r -property8 , defined as the disjunction of a safety r -property ("p should always hold") and a guarantee r -property ("q should eventually hold"). According to the classical definition of monitorability, this property is monitorable. Indeed, for any finite sequence σ, this property can be positively determined by σ • {p, q} or by σ • {p, q}, i.e., by completing σ with an event in which q is true. Beyond Obligation properties. Following the classical definition of monitorability, it is possible to show that there exist non-monitorable and monitorable properties for super classes of the Obligation class. The above two properties are pure response properties, one is not monitorable, the other one is.

Example 5 (Non-monitorable response property [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]). The (response) property "Every request is eventually followed by an acknowledgement"9 is not monitorable. This property is represented by the Streett (response) automaton depicted in Fig. 9 with R = {1}. Its alphabet is Σ = {req, ack , oth} where req (resp. ack, oth) denotes the request (resp. the acknowledgment, any other event).

Using the acceptance criteria for finite and infinite sequences, one can reasonably be convinced that this automaton defines the considered property. Indeed, a finite sequence is accepted if and only if previous requests have been acknowledged. An infinite sequence is accepted if and only if state 1 is visited infinitely often which means for an infinite sequence that requests have been acknowledged. For this property, there are two limitations for monitoring using the classical definition of monitorability. First, it is impossible to distinguish correct (ending in state 1) and incorrect finite sequences (ending in state 2): both evaluate to "?". Second, for all finite sequences, it is never possible to decide ⊤ or ⊥ since every finite sequence can be extended to correct or incorrect infinite continuations. In other words, it is never possible to satisfy or falsify this property with a finite observation.

Example 6 (Monitorable response property). The (response) property "Every request should be acknowledged, and it is forbidden to send two successive requests (without acknowledgment)" is monitorable. This property is represented by the Streett response automaton depicted in Fig. 10 with R = {1} and the same alphabet Σ as in Example 5. Notice that this property is indeed a pure response property: it cannot be represented by a finitestate Streett obligation automaton. Intuitively, given an execution sequence, this r -property can always be negatively determined by one of its continuations. Indeed, for any σ ∈ Σ * , the property is negatively determined by σ • req • req, and is thus σ-monitorable.

Thus there exist monitorable (pure) response properties. Consequently, using Lemma 2, there exist also monitorable pure persistence and reactivity properties. Indeed, monitorable properties are closed under Boolean operations.

Parametrization of the classical definition of monitorability

As we will see, the characterization of monitorable properties may also depend on a truth-domain B we consider when evaluating an execution sequence. Thus we parameterize the classical definition of monitorable properties with a truth-domain.

The first truth-domain we have studied is a 3-valued truth-domain B 3 def = {⊥, ?, ⊤}. This truth-domain is inherent in the classical definition. The value "⊥" is used to express property violation when the property is negatively determined. The value "⊤" is used to express property satisfaction when the property is positively determined. The value "?" is used to express that no verdict can be produced. B 3 can be viewed as a complete lattice, whose minimal value is ⊥ and maximal value is ⊤. Boolean operators ∨ and ∧ are then defined respectively as upper and lower bounds.

The classical definition of monitorability is purposed to the detection of verdicts for infinitary properties, i.e., to detect either ⊤ or ⊥. This definition can be parameterized by a truth-domain B containing at least one of these two elements: This latest remark shows a first limitation of the definition of (parameterized) classical monitorability: considering finer truth-domains, as it could be required in specific application domains, will not increase the set of monitorable properties. This is one of the motivations to introduce an alternative definition of monitorability (in Section 5.3).

Monitorability with a truth-domain of cardinality 2. Restraining B 3 to a truth-domain of cardinality 2 allows only either positive or negative determinacy, and hence reduces the set of monitorable properties. Indeed, the purpose of the monitor is then either to detect only bad behaviors or only good behaviors (but not both).

In the sequel we consider two subsets of B 3 , namely

B ⊥ 2 def = {⊥, ?} and B ⊤ 2 def
= {?, ⊤}. However, there is no simple characterization of these properties in the Safety-Progress hierarchy. Intuitively one may think that with B ⊥ 2 = {⊥, ?}, the set of monitorable properties would be the set of safety properties. Actually, there are numerous safety properties which can never be negatively determined. For example, the r -property true = (Σ * , Σ ω ) = (A f (Σ * ), A(Σ * )) cannot be negatively determined nor falsified. Moreover all safety properties which are valid forever for execution sequences longer than a given k ∈ N are not σ -B ⊥ 2monitorable when |σ| > k. For these kinds of properties a monitor would produce only verdict sequences containing "?" when evaluating an execution sequence. Similarly, there exist many guarantee properties that cannot be positively determined, and therefore are not monitorable with B ⊤ 2 = {?, ⊤}. Regarding these sets of monitorable properties, it appears that there is no simple characterization, in terms of classes of the Safety-Progress classification. However, in Section 5.4, we will provide a syntactic criterion on Streett automata in order to decide whether the r -property recognized by a given automaton is monitorable according to the mentioned truth-domains.

Monitorable properties according to an alternative definition of monitorability

The interest of previous definitions of monitorability is due to two facts: the underlying truth-domain is 2-valued or 3-valued and the aim is the detection of verdict of infinitary properties. Although it is possible to give a semantics to all reactive properties with either a 2-valued or 3-valued truth-domain, the question is whether those values make sense for some properties in a monitoring context.

As noticed in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Leucker | A brief account of runtime verification[END_REF], it seems interesting to investigate further the set of monitorable properties, and to answer more precisely questions like "what verdict to issue if the program execution stops here". This means a better distinction between finite sequences which evaluate to "?" in a 2-valued or a 3-valued truth-domain.

Hence, the authors of [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Leucker | A brief account of runtime verification[END_REF] proposed to consider a 4-valued truth-domain B 4 = {⊥, ⊥ c , ⊤ c , ⊤}. The truthvalue ⊤ c (resp. ⊥ c ) denotes "currently true" (resp. "currently false") and it expresses "Π-satisfaction (resp. Πviolation) if the program execution stops here". Boolean operators ∨ and ∧ are defined in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]. Using B 4 leads to an alternative definition of monitoring. This new definition leverages the evaluation of finite sequences in the Safety-Progress classification framework.

Property evaluation in a truth-domain

We first introduce how, given an r -property, we evaluate an execution sequence in the truth-domains we considered so far.

Definition 16 (Property evaluation w.r.t. a truthdomain). For each of the possible truth-domain B, we define the evaluation functions

[[•]] B (•) : 2 Σ * ×Σ ω × Σ * → B as follows: For B ⊥ 2 : [[Π]] B ⊥ 2 (σ) = ⊥ if ∀µ ∈ Σ ∞ , ¬Π(σ • µ); [[Π]] B ⊥ 2 (σ) = ? otherwise. For B ⊤ 2 : [[Π]] B ⊤ 2 (σ) = ⊤ if ∀µ ∈ Σ ∞ , Π(σ • µ); [[Π]] B ⊤ 2 (σ) = ? otherwise. For B 3 : [[Π]] B3 (σ) = ⊥ if ¬Π(σ) ∧ ∀µ ∈ Σ ∞ , ¬Π(σ • µ); [[Π]] B3 (σ) = ⊤ if Π(σ) ∧ ∀µ ∈ Σ ∞ , Π(σ • µ); [[Π]] B3 (σ) = ? otherwise.
For B 4 :

[[Π]] B4 (σ) = [[Π]] B3 (σ) if [[Π]] B3 (σ) = ⊥ ∨ [[Π]] B3 (σ) = ⊤, [[Π]] B4 (σ) = ⊤ c if [[Π]] B3 (σ) = ? ∧ Π(σ), [[Π]] B4 (σ) = ⊥ c if [[Π]] B3 (σ) = ? ∧ ¬Π(σ).
Remark 6. The defined property evaluation w.r.t. B 4 is similar to the semantics of the LTL variant RV-LTL defined in [START_REF] Bauer | Comparing ltl semantics for runtime verification[END_REF].

An alternative definition of monitorability

Intuitively, the monitorability notion we propose relies on the ability for a given monitor to distinguish between good and bad finite execution sequences with respect to a property Π.

Definition 17 (Alternative Monitorability

). An rproperty Π = (φ, ϕ) is said to be monitorable with the truth-domain B, or B-monitorable if

∀σ good ∈ φ, ∀σ bad ∈ φ, [[Π]] B (σ good ) = [[Π]] B (σ bad ).
We note MP * (B), the set of monitorable properties with truth-domain B according to this definition.

Thus, an r -property is monitorable with a given truthdomain B if and only if evaluations of good and bad finite execution sequences lead to distinct values. Remark that this definition seemingly does not rely on the infinitary part of the r -property (although this infinitary part is taken into account in the evaluation function).

Characterization of monitorable properties

Lemma 3 (MP * (B 3 ), safety, and guarantee properties). The set of monitorable properties (according to Definition 17) with B 3 is included in the union of safety and guarantee properties. Formally:

MP * (B 3 ) ⊆ Safety(Σ) ∪ Guarantee(Σ).
Proof. The formal proof can be found in Appendix A.2.3. It is done by reductio ad absurdum and supposing the existence of an r -property Π = (φ, ϕ) defined on Σ which is neither a safety nor a guarantee r -property. The proof shows the existence of two execution sequences, one good, the other one bad, for Π s.t. these sequences are evaluated to "?". ⊓ ⊔ Theorem 3 (Multi-valued characterization of alternative monitorability). The sets of monitorable properties according to the truth-domains considered so far are the following:

(i) MP * (B ⊥ 2 ) = Safety(Σ), (ii) MP * (B ⊤ 2 ) = Guarantee(Σ), (iii) MP * (B 3 ) = Safety(Σ) ∪ Guarantee(Σ), (iv) MP * (B 4 ) = Reactivity(Σ).
The proof can be found in Appendix A.2.4.

Example 7 (Alternative monitoring of an obligation property).

Let us go back again to the property considered in the introduction, stating that "p should always hold or q should eventually hold". We examine again the execution sequences: σ good = {p, q}•{p, q} and σ bad = {p, q}•{p, q}.

Considering B 3 , we have [[Π]] B3 (σ good ) = [[Π]] B3 (σ bad ) = ?. Thus, Π is not B 3 -monitorable. However, Π is B 4 - monitorable and [[Π]] B4 (σ good ) = ⊤ c and [[Π]] B4 (σ bad ) = ⊥ c .
This example shows how the finite sequence semantics leverages the interest of monitoring certain properties. Furthermore, it shows that under our definition of monitoring, ambiguous situations, such as those encountered with the classical definition, are avoided.

Our definition of monitorability has the advantage of being able to identify the properties which should not be monitored with a truth-domain "not fine enough". Indeed the last property shows that if we build a monitor for such a property with the truth-domain B 3 , this monitor would produce an evaluation "?" for correct and incorrect execution sequences w.r.t. the property. This seems not desirable to us.

Furthermore, we have shown in Section 4.4 that, for a given finite sequence σ and an r -property Π, [[Π]] B4 (σ) is easy to compute from the set of states of a Streett automaton recognizing Π.

Characterizations in the automata view

Although some sets of monitorable properties we considered cannot be precisely expressed in terms of Safety-Progress classes, it is still possible to characterize them with some syntactic criteria on Streett automata. It relies on the characterization of the states of Streett automata introduced in Section 4.4.

Property 3 (Correspondence between Streett automata states and B 4 ). Given a Streett m-automaton recognizing an r -property Π and a sequence σ ∈ Σ * of length n s.t. run(σ, A Π ) = q 0 • • • q n , we have:

q n ∈ Good AΠ ⇔ [[Π]] B4 (σ) = ⊤, q n ∈ Good AΠ c ⇔ [[Π]] B4 (σ) = ⊤ c , q n ∈ Bad AΠ c ⇔ [[Π]] B4 (σ) = ⊥ c , q n ∈ Bad AΠ ⇔ [[Π]] B4 (σ) = ⊥.
Proof. The proof is given in Appendix A.2, it uses the acceptance criteria of Streett automata to establish the correspondence. ⊓ ⊔ Remark 7 (Correspondance with B 3 , B ⊥ 2 , and B ⊤ 2 ). From Property 3 and Definition 16, one can easily deduce a correspondence between the set of states and the evaluation in the truth-domain of a lower cardinality:

-For B 3 :

-

q n ∈ Good AΠ ⇔ [[Π]] B3 (σ) = ⊤, -q n ∈ Good AΠ c ∪ Bad AΠ c ⇔ [[Π]] B3 (σ) =?, -q n ∈ Bad AΠ ⇔ [[Π]] B3 (σ) = ⊥. -For B ⊤ 2 : -q n ∈ Good AΠ ⇔ [[Π]] B ⊤ 2 (σ) = ⊤, -q n ∈ Good AΠ c ∪ Bad AΠ c ∪ Bad AΠ ⇔ [[Π]] B ⊤ 2 (σ) = ?. -For B ⊥ 2 : -q n ∈ Bad AΠ ⇔ [[Π]] B ⊥ 2 (σ) = ⊥, -q n ∈ Bad AΠ ∪ Good AΠ c ∪ Bad AΠ c ⇔ [[Π]] B ⊥ 2 (
σ) = ?. Now we are able to give an exact characterization of monitorable properties in the automata view.

Theorem 4 (Automata view of classical monitorability). The r-property Π recognized by the Streett m-automaton

A Π = (Q A Π , q A Π init , → A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) is (i) MP (B ⊥ 2 )-monitorable iff ∀q ∈ Reach(q A Π init ), Reach(q) ∩ Bad A Π = ∅; (ii) MP (B ⊤ 2 )-monitorable iff ∀q ∈ Reach(q A Π init ), Reach(q) ∩ Good A Π = ∅; (iii) MP (B3)-monitorable iff ∀q ∈ Reach(q A Π init ), Reach(q) ∩ (Bad A Π ∪ Good A Π ) = ∅.
Proof. This property is established by noticing first that it is a consequence of Property 3 and second that we are considering deterministic and complete Streett automata. Thus, the two following facts are equivalent:

-from every accessible state, a bad (resp. good, bad or good) is reachable; -every finite sequence has a continuation that determines negatively (resp. positively, negatively or positively) the underlying property.

⊓ ⊔

Example 8 (Automata view of lassical monitorability). We illustrate the use of the previous theorem to state whether the properties of Example 2 (Fig. 3), with their provided automata, are monitorable according to the classical definition:

-The property Π 1 specified by A Π1 is B ⊥ 2 -
A Π = (Q A Π , q A Π init , → A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) is (i) MP * (B ⊥ 2 )-monitorable iff Bad A Π = m i=1 R i ∩ P i ; (ii) MP * (B ⊤ 2 )-monitorable iff Good A Π = m i=1 R i ∪ P i ; (iii) MP * (B 3 )-monitorable iff ∄q ∈ Reach(q A Π init ) ∩ m i=1 R i ∪ P i , ∄q ′ ∈ Reach(q A Π init ) ∩ m i=1 R i ∩ P i , q ∈ Good A Π c ∧ q ′ ∈ Bad A Π c .
Proof. The proof is conducted in three steps:

(i) The expressed condition generalizes the syntactic restriction of Streett safety automata and is also a condition when a given not minimal Streett m-automaton is recognizing a safety property and can be minimized so as to be represented as a Streett safety automaton. (ii) The expressed condition generalizes the syntactic restriction of Streett guarantee automata and is also a condition when a given not minimal Streett mautomaton is recognizing a guarantee property and can be minimized so as to be represented as a Streett safety automaton. MP * (B 3 )

MP * (B ⊥ 2 ) MP * (B ⊤ 2 )
MP * (B 4 ) Fig. 11. Monitorable r -properties in the Safety-Progress classification

(iii) The third condition can be established using the two following facts:

-An r -property is not monitorable according to this theorem if and only if for two sequences, a good and a bad sequences evaluate to "?". Other evaluations are not simultaneously possible for a bad and good sequences. -We are considering deterministic and complete Streett automata. ⊓ ⊔

Summary

We depict in Fig. 11 the main results obtained in this section, which can be summarized as follows:

-The classes of monitorable properties, according to the classical definition, are:

-MP (B ⊤ 2 ), which can not be compared directly with any other class; -MP (B ⊥ 2 ), which can not be compared directly with any other class; -and MP (B 3 ) = MP c which contains strictly the class of obligation properties. -The classes of monitorable properties, according to the new definition we introduced are:

-MP * (B ⊥ 2 ) is the set of safety r -properties; -MP * (B ⊤ 2 )
is the set of guarantee r -properties; -MP * (B 3 ) is strictly contained in the class of obligation r -properties and is the union of the sets of safety and guarantee properties; -and MP * (B 4 ) is the set of reactivity r -properties.

Remark that using the truth-domain B 4 does not add any expressiveness to the classical definition of monitorability (i.e., MP (B 4 ) = MP (B 3 )). Indeed, this definition is bound to the notion of positive and negative determinacy. However using this domain would permit to better distinguish execution sequences and to avoid ambiguity exposed in Example 4. Note also that some obligation properties (between MP (B 3 ) and MP * (B 3 )) should not be monitored unless with a truth-domain equipped with an interpretation of finite sequences allowing to distinguish good and bad finite sequences (e.g., with truthvalues ⊥ c and ⊤ c ).

Remark 8. One can notice that the monitorability results expressed in the automata view (i.e., Theorems 4 and 5) hold only for regular r -properties. Whereas the results that were not expressed in the automata view (i.e., Lemma 2, Theorems 2 and 3) hold for all r -properties (e.g., regular, context-free, context-sensitive, recursively enumerable), independently from any computability constraint on their recognizing mechanisms.

Enforceability w.r.t. the SP classification

Now we address the question of the expressiveness of runtime enforcement, that is, we characterize the class of enforceable properties. In Section 3, we have seen that the previous proposed classes were delineated according to the mechanism used to enforce the properties. Such mechanisms should obey the soundness and transparency constraints. We choose here to take an alternative approach. Indeed we believe that the set of enforceable properties can be characterized independently from any enforcement mechanism complying to these constraints, provided that this memory is unbounded but finite. This will give us an upper-bound of the set of enforceable properties with any enforcement mechanism.

Enforcement criteria

The enforcement constraints exposed in Section 3, namely soundness and transparency, express a relation between the input sequence (submitted to an enforcement monitor) and an output sequence (produced by this monitor). We interpret these constraints in the following way: if the input sequence already verifies the property, then it should remain unchanged (up to a given equivalence relation), otherwise its longest prefix satisfying the property should be issued 10 .

A consequence is that an r -property (φ, ϕ) will be considered as enforceable only if each incorrect infinite sequence has a longest correct prefix. This means that any infinite incorrect sequence should have only a finite number of correct prefixes 11 . We give two enforcement criteria, in the language and automata views.

Definition 18 (Enforcement criterion in the language view). An r -property (φ, ϕ) is said to be en-

forceable if ∀σ ∈ Σ ω , ¬ϕ(σ) ⇒ (4) ∃σ ′ ∈ Σ * , σ ′ ≺ σ ∧ ∀σ ′′ ∈ Σ * , σ ′ ≺ σ ′′ ≺ σ ⇒ ¬φ(σ ′′ )
Alternatively, it is possible to express an enforcement criterion for an r -property Π on its recognizing Streett m-automaton A Π . This criterion uses the set S(A Π ) of (maximal and non-maximal) Strongly Connected Components of A Π . For an m-automaton A Π and s an SCC of A Π , we define

I s def = {i ∈ [1, m] | s ⊆ R i ∧ s ∩ P i = ∅}.
Intuitively, I s is the set of accepting pairs of A Π that leads the infinite sequences, visiting infinitely often the SCC s, to be rejected. The criterion is formally expressed as follows:

Definition 19 (Enforcement criterion in the automata view). The r -property Π recognized by an m-automaton A Π is said to be enforceable if

∀s ∈ S(A Π ), I s = ∅ ⇒ ∃i ∈ I s , s ⊆ P i (5)
Intuitively, this later enforcement criterion states that for every non-accepting SCC s (s is non accepting because it contains at least one pair in [1, m] for which the infinite acceptance criterion is not satisfied), then, among these indexes, there is at least one index i s.t. all states in the SCC s are in P i . Enforcement criteria of Definitions 18 and 19 are equivalent, as stated below.

Property 4 (Equivalence between enforcement criteria). Considering an r -property

Π = (φ, ϕ), recog- nized by a Streett m-automaton (Q A Π , q A Π init , Σ, → A Π , {(R 1 , P 1 ), . . . , (R m , P m )}), we have: (4) ⇔ (5).
Proof. We just give a sketch of the proof, the formal proof can be found in Appendix A.3.1. The proof shows the implications in both ways and uses the definitions of the acceptance criteria of Streett automata for finite and infinite sequences. Then one has to remark that:

-(4) expresses a condition on the set of infinite sequences that do not satisfy the r -property; -(5) expresses a condition on the set of SCC s that reject the sequences visiting s infinitely often.

As we are dealing with complete and deterministic automata, these conditions are equivalent. ⊓ ⊔

The set of enforceable r -properties, equivalently defined by Definition 4 or Definition 5, is denoted EP . We will now characterize EP w.r.t. the SP classification. We will prove that EP is exactly the class of response properties. Note that the enforcement criterion in the automata view is still useful as it provides a syntactic procedure to determine whether a property is enforceable or not.

Enforceable properties

We start first by proving that response properties are enforceable. Then, we give the intuition on the nonenforceability of persistence properties by providing an illustrative example. Then, we prove that the set of response properties is exactly the set EP .

Response(Σ) ⊆ EP

Proof. Indeed consider a response r -property Π = (φ, ϕ) and an execution sequence σ ∈ Σ ω . Π can be expressed as (R f (ψ), R(ψ)) for a given finitary language ψ. Let us suppose that ¬ϕ(σ). It means that σ ∈ R(ψ), i.e., σ has finitely many prefixes belonging to ψ. Consider the set

S = {σ ′ ∈ Σ * | ∀σ ′′ ∈ Σ * , σ ′ ≺ σ ′′ ≺ σ ∧ ¬ψ(σ ′′ )}
of finite sequences from which all finite continuations do not satisfy ψ. As ¬R(ψ)(σ), this set is not empty. Let us note σ 0 the smallest element of S regarding ≺.

We have

∀σ ′ ∈ Σ * , σ 0 ≺ σ ′ ≺ σ ⇒ ¬ψ(σ ′ ). Since ∀ψ ′ ⊆ Σ * , R f (ψ ′ ) ⊆ ψ ′ (cf.
the definition of operators building finitary properties), it implies that ∀σ ′ ∈ Σ * , σ 0 ≺ σ ′ ≺ σ ⇒ ¬φ(σ ′ ). Thus, Π is enforceable according to Definition 18. ⊓ ⊔

A straightforward consequence is that safety, guarantee and obligation r -properties are enforceable. We prove that, in fact, pure persistence properties are not enforceable. Let us explain the intuition through an example.

For Σ ⊇ {a, b}, an example of pure persistence rproperty is Π = (Σ * • a + , Σ * • a ω ) stating that "it will be eventually true that a always occurs". One can notice that this property is neither a safety, guarantee nor obligation property. Π is recognized by the Streett automaton A Π depicted in Fig. 12 (with P = {1}). One can understand the enforcement limitation intuitively with the following argument: if this property was enforceable it would imply that an enforcement monitor can decide from a certain point that the underlying program will always produce the event a. However such a decision can never be taken by a monitor without memorizing the entire execution sequence beforehand. This is unrealistic for an infinite sequence. More formally, as stated in Definition 18, an r -property (φ, ϕ) is enforceable if for all infinite execution sequences σ when ¬ϕ(σ), the longest prefix of σ satisfying φ always exists. For the above automaton, the execution sequence σ ′ bad = (a • b) ω does not satisfy the property whereas an infinite number of its prefixes do (prefixes ending with a).

Applying enforcement criteria on persistence properties, it turns out that the enforceable persistence properties are in fact response properties.

Theorem 7 (Enforceable persistence properties are response properties).

Persistence(Σ) ∩ EP ⊆ Response(Σ)

Proof. A persistence r -property Π becomes non enforceable as soon as there exists a SCC of R-states containing a P -state and a P -state on its recognizing automaton A Π (see Definition 19). Indeed, on a Streett automaton it allows infinite invalid execution sequences with an infinite number of valid prefixes. When removing this possibility on a Streett automaton, the constrained automaton can be easily translated to a response automaton. Indeed, the states visited infinitely often are then either all in P or P , that is: ∀σ ∈ Σ ω , vinf (σ, A Π ) ∩ P = ∅ ⇔ vinf (σ, A Π ) ⊆ P . On such automaton there is no difference between R-states and P -states. Consequently by re-tagging P -states to R-states, this automaton recognizes the same property. The re-tagged automaton is a response automaton. ⊓ ⊔ Corollary 1. Pure persistence properties are not enforceable:

(Persistence(Σ) \ Response(Σ)) ∩ EP = ∅
Proof. This is a direct consequence of Theorem 7. ⊓ ⊔ Theorem 8 (Enforceable m-reactivity properties are response properties).

Reactivity(Σ) ∩ EP ⊆ Response(Σ)

Proof. The formal proof can be found in Appendix A.3.2.

The proof shows that an m-reactivity automaton which is constrained by the enforcement criterion (Definition 19) can be translated to an m-response automaton accepting exactly the same sequences. Thus, the only enforceable reactivity properties are the response ones. ⊓ ⊔ Corollary 2. Pure reactivity properties are not enforceable:

Reactivity(Σ) ⊆ EP Reactivity(Σ) \ (Persistence(Σ) ∪ Response(Σ)) ∩ EP = ∅
Proof. This is a direct consequence of Theorem 8. ⊓ ⊔ Corollary 3. Enforceable properties are exactly response properties:

EP = Response(Σ)
Proof. It remains to prove that the set of enforceable properties is included in the set of response properties. Suppose that there exists an enforceable property which is not a response one. Then, according to the definition of the Safety-Progress hierarchy, this property would be either a pure persistence or a pure reactivity property. Consequently this property would not be enforceable.

⊓ ⊔

Example 9 (Enforceable and not enforceable properties).

We illustrate the enforcement criterion on the properties introduced in Example 1 and represented by their Streett automata described in Example 2 and depicted in Fig. 3.

-The properties Π 1 , Π 2 , Π 3 are enforceable.

A ψ A Π A ?Π A ↓Π ψ Π = (X f (ψ), X(ψ)) (EM) X ∈ {A, E, R, P } (VM)
Fig. 13. Automaton transformations -The property Π 4 is not enforceable; e.g., the infinite sequence r

• g • (r • d • r • g) ω
is not accepted while this sequence has an infinite number of correct prefixes: e.g., all sequences belonging to r

• g • (r • d • r • g) * .
Being enforceable or not can be determined rather easily either by observing the automata and using the acceptance criteria for finite and infinite sequences or by using the criterion in the automata view.

Monitor synthesis

Now we show how it is possible to obtain easily a monitor either for verifying or enforcing a property thanks to the framework introduced in Section 4. Generally speaking, a monitor is a device processing an input sequence of events or states in an incremental fashion. It is purposed to yield a property-specific decision according to its goal. In (classic) runtime verification such a decision is a truth-value taken from a truth-domain. This truthvalue states an appraisal of property satisfaction or violation by the input sequence. For runtime enforcement, the monitor produces a sequence of enforcement operations. The monitor uses an internal memory and applies enforcement operations to the input event and its current memory so as to modify the input sequence and produce an output sequence. The relation between the input and output sequences should follow enforcement monitoring constraints: soundness and transparency (Section 3.2).

In the following we consider a Streett m-automaton

A Π = (Q A Π , q A Π init , → A Π , {(R 1 , P 1 ), .
. . , (R m , P m )}) and Π the r -property recognized by A Π . Moreover, we evaluate properties only in B 4 , and consequently we abbreviate

[[Π]] B4 (•) by [[Π]](•).
The general monitor synthesis procedure is depicted in Fig. 13. From a "pattern" X corresponding to one of the basic classes of the hierarchy and a DFA A ψ recognizing a finitary property ψ ⊆ Σ * , DFA2S_X yields a Streett automaton recognizing the r -property (X f (ψ), X(ψ)). Then using Streett2VM (resp. Streett2EM ) one is able to obtain a verification (resp. enforcement) monitor for the r -property (X f (ψ), X(ψ)).

Monitor: A general definition

A monitor is a procedure consuming events fed by an underlying program and producing an appraisal in the current state depending on the sequence read so far. Considered monitors are deterministic finite-state machines producing an output in a relevant domain. This domain will be refined for special-purpose monitors (verification and enforcement). For verification monitors, this output function gives a truth-value (a verdict) in B 4 regarding the evaluation of the current sequence relatively to the desired property. For enforcement monitors (EMs), this output function gives an enforcement operation inducing a modification on the input sequence so as to enforce the desired property.

Definition 20 (Monitor).

A monitor A is a 5-tuple

(Q A , q A init , -→ A , X A , Γ A
) defined relatively to a set of events Σ. The finite set Q A denotes the control states and q A init ∈ Q A is the initial state. The complete function -→ A : Q A × Σ → Q A is the transition function. In the following we abbreviate -→ A (q, a) = q ′ by q a -→ A q ′ . The set of values X A depends on the purpose of the monitor (verification or enforcement). The function Γ A : Q A → X A is an output function, producing values in X A from states.

Synthesizing monitors for runtime verification

In the following 12 , we consider monitorable r -properties Π and (φ, ϕ) in MP * (B 4 ).

Definition 21 (Verification monitor). A verification monitor (VM)

A ? is a monitor with X A = B 4 . Such monitors are independent from any specification formalism, and can be easily adapted to the specification formalism from which they are generated. We define, the notion of verification sequence produced by a monitor and what it means to verify a property for a monitor. It amounts to define the verification performed by a VM A ? while reading an input σ ∈ Σ * (produced by P Σ ) and producing a sequence b ∈ B 4 + .

Definition 22 (Sequence verification). The verification function [[A

? ]](•) : Σ * → B 4 +
, defining the verification performed by A ? , produces a verification sequence while reading σ. This verification sequence is defined as follows:

∀σ ∈ Σ * , [[A ? ]](σ) = Γ A ? (q A ? init ) • • • Γ A ? (q n ) (6) with q A ? init σ0 -→ A ? q 1 σ1 -→ A ? • • • q n-1 σn-1
-→ A ? q n and |σ| = n.

Definition 23 (Monitor soundness). A monitor

A ? is sound w.r.t. Π = (φ, ϕ) ∈ MP * (B 4 ) on P Σ , noted Ver (A ? , Π, P Σ ), if ∀σ ∈ Exec(P Σ ) ∩ Σ * , last([[A ? ]](σ)) = [[Π]] B4 (σ).
where

[[•]] B4 is defined in Definition 16.
This definition states that the verification sequence produced by A ? matches the evaluation function of a sequences w.r.t. an r -property.

Using the set P A Π of a Streett automaton A Π , we show how it is possible to obtain a verification monitor for the r -property Π.

Definition 24 (Streett2VM transformation). Given a Streett m-automaton

A Π = (Q A Π , q A Π init , Σ, -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) recognizing Π ∈ MP * (B 4 ), we define the transformation Streett2VM(A Π ) = (Q A Π , q A Π init , → A Π , B 4 , Γ ) s.t. Γ : Q A ? → B 4
produces truthvalues from states depending on the set

P A Π : ∀q ∈ Q A Π , q ∈ Good A Π ⇒ Γ (q) = ⊤, q ∈ Good A Π c ⇒ Γ (q) = ⊤ c , q ∈ Bad A Π c ⇒ Γ (q) = ⊥ c , q ∈ Bad A Π ⇒ Γ (q) = ⊥.
An r -property Π is verifiable on P Σ by a VM A ?Π obtained by the application of Streett2VM on the automaton recognizing Π.

Example 10 (Verification Monitors). In Fig. 14 are represented VMs for the properties introduced in Example 1, specified by Streett automata in Fig. 3, and synthesized with the Streett2VM transformation.

Theorem 9 (Correctness of Streett2VM). Given

A Π recognizing Π, we have:

Π ∈ MP * (B 4 ) ∧ A ?Π = Streett2VM(A Π ) ⇒ Ver (A ?Π , Π, P Σ )
Proof. The proof of this theorem relies on the correctness of the computation performed while obtaining P A Π for A Π (Property 3). ⊓ ⊔

Synthesizing monitors for runtime enforcement

In the remainder, we consider enforceable r -properties (φ, ϕ) and Π ∈ EP , and a Streett m-automaton

A Π = (Q A Π , q A Π init , Σ, -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) recog- nizing Π.
An EM is producing enforcement operations depending on its current state.

Definition 25 (Enforcement monitor). An EM A

! is a 5-tuple (Q A ! , q A ! init , -→ A ! , Ops, Γ ).
Enforcement operations of Ops performed by the EM are aimed to operate a modification of the internal memory and potentially produce an output, i.e., each enforcement operation is a function: The considered enforcement operations allow enforcement monitors either to halt the target program (when the current input sequence irreparably violates the property), or to store the current event in a memory device (when a decision has to be postponed), or to dump the content of the memory device (when the target program went back to a correct behavior), or to switch off the monitor when all possible continuations of the current input sequence are correct w.r.t. the property under scrutiny 13 .

Σ × Σ * → Σ * × Σ * . Then Γ : Q A ↓ → Ops is the output function, producing enforcement operations from states. ⊤ c ⊤ c ⊤ c ⊥ r g r g r g Σ ⊥ c ⊥ c ⊤ ⊥ r g r g Σ Σ ⊤ c ⊥ c ⊥ r g g r Σ ⊥ c ⊥ c ⊤ c ⊤ c ⊥ ⊥ c
Definition 26 (Enforcement operations). We define a set of enforcement operations Ops = {halt, store, dump, off } as follows:

∀e ∈ Σ ∪ {ǫ Σ }, ∀m ∈ Σ * , halt(e, m) = (ǫ Σ , m), store(e, m) = (ǫ Σ , m • e), dump(e, m) = (m • e, ǫ Σ ), off (e, m) = (m • e, ǫ Σ ).
where e designates the input event of the monitor and m the memory device content.

Note that the off and dump operations have the same definitions. From a theoretical perspective, the off is indeed not necessary. However, it has a practical interest.

In order to limit the monitor's impact on the original program (performance wise), it is of interest to know when the monitor is not needed anymore. We define the transformation performed by an EM A ! while reading an input sequence σ ∈ Σ * and producing an output sequence o ∈ Σ * .

Definition 27 (Sequence transformation). The sequence transformation function [[A

! ]](•) : Σ * → Σ * relies on the function [[A ! ]](•, •, •) : Σ * × Q A ! × Σ * → Σ * defin-
ing the transformation performed on the current state and the internal memory content: [[A ! ]](σ, q, m) is the output sequence produced while reading σ from state q and (initial) memory content m.

∀q ∈ Q A ! , ∀m ∈ Σ * , [[A ! ]](ǫ Σ , q, m) = ǫ Σ (7) [[A ! ]](e • σ, q, m) = o • [[A ! ]](σ, q ′ , m ′ ) (8)
with

q e -→ A ! q ′ ∧ Γ (q ′ ) = α ∈ Ops ∧ α(e, m) = (o, m ′ ).
13 Although, dump and off have the same definition, distinguishing them is useful in practice. Indeed, the off operation is intended to be produced when all continuations of the current execution sequence are correct w.r.t. the property. It allows to determine when the EM is not needed anymore. Consequently, it helps reducing the performance impact on the underlying program

The empty sequence ǫ Σ is transformed into itself by A ! , this is the case when the underlying program does not produce any event [START_REF] Chen | MOP: An Efficient and Generic Runtime Verification Framework[END_REF]. An execution sequence e • σ is (incrementally) transformed according to the transition fired by the input e: the current memory content and the input e are applied to the enforcement operation of the arriving-state transition, it induces a new memory content and an output o (8).

We define now the notion of property-enforcement by an EM. The notion of enforcement relates the input sequence produced by the program and given to the EM and the output sequence allowed by the EM (correct w.r.t. the property under consideration) 14 .

Definition 28 (Property-Enforcement). For Π = (φ, ϕ) ∈ EP , we say that A ! enforces Π on P Σ , noted Enf (A ! , Π, P Σ ), iff for any σ ∈ Exec(P Σ ) ∩ Σ * , there exists o ∈ Σ ∞ , s.t. the following constraints hold:

[[A ! ]](σ, q A ! init , ǫ) = o (9) Π(σ) ⇒ σ = o (10) ¬Π(σ) ∧ Pref ≺ (φ, σ) = ∅ ⇒ o = ǫ (11) ¬Π(σ) ∧ Pref ≺ (φ, σ) = ∅ ⇒ o = Max (Pref ≺ (φ, σ)) (12) (9)
, ( 10), [START_REF] Amorim | Efficient monitoring of ω-languages[END_REF], and (12) ensure soundness and transparency of A ! : (9) stipulates that the sequence σ is transformed by A ! into a sequence o; [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF] ensures that if σ already satisfy the property then it is not transformed. [START_REF] Amorim | Efficient monitoring of ω-languages[END_REF] ensures that, when no prefix of σ satisfies the property, the EM outputs nothing (the empty sequence ǫ Σ ). [START_REF] Emerson | Characterizing correctness properties of parallel programs using fixpoints[END_REF] ensures that, if some prefix of σ satisfies the property, o is the longest prefix of σ satisfying the property.

Soundness comes from the fact that the produced sequence o, when different from ǫ Σ , always satisfies the property φ. Transparency is ensured by the fact that correct execution sequences are not changed, and incorrect ones are restricted to their longest correct prefix.

One may remark that it would have been possible to set Max (Pref ≺ (φ, σ)) to ǫ Σ when Pref ≺ (φ, σ) = ∅ and merge the two last constraints. However, we choose to distinguish explicitly the case in which Pref ≺ (φ, σ) = ∅ as it highlights some differences when an EM produces ǫ Σ . Sometimes it corresponds to the only correct prefix of the property. But it can also be an incorrect sequence w.r.t. the property. In practice, when implementing an EM for a system, this sequence can be "tagged" as incorrect 15 .

Finally, since we have to deal with potentially infinite input sequences, the output sequence should be produced in an incremental way 16 : for each current prefix σ of the input sequence read by the EM, the current output o produced should be sound and transparent with respect to Π and σ. This means that deciding whether a finite sequence σ verifies Π or not should be computable in a finite amount of time (and reading only a finite continuation of σ).

We synthesize EMs from Streett automata in the framework of r -properties. This transformation was previously introduced in the form of several transformations [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF]. Here we generalize those transformations into a unique one.

Definition 29 (Streett2EM transformation). The transformation

Streett2EM(A Π ) = (Q A Π , q A Π init , -→ A Π , Ops, Γ ) is defined s.t. Γ : Q A !Π → Ops produces en- forcement operations: ∀q ∈ A Π , q ∈ Good A Π ⇒ Γ (q) = off ; q ∈ Good A Π c ⇒ Γ (q) = dump; q ∈ Bad A Π c ⇒ Γ (q) = store ; q ∈ Bad A Π ⇒ Γ (q) = halt.
Example 11 (Enforcement Monitors). Fig. 15 represents EMs for the properties introduced in Example 1, specified by Streett automata in Fig. 3, and synthesized with the Streett2EM transformation.

An r -property Π ∈ EP is enforceable on P Σ by an EM obtained by the application of Streett2EM on the automaton recognizing Π.

Theorem 10 (Correctness of Streett2EM). Given A Π recognizing Π ∈ EP , we have:

A !Π = Streett2EM(A Π ) ⇒ Enf (A !Π , Π, P Σ ).
Proof. Correctness of the general transformation relies on the correctness (proved in [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF]) of the transformations specific to each class of properties. Indeed, this general transformation reduces to the specific transformation when applied to a specific class of properties. ⊓ ⊔ Such a unified transformation is useful in practice (from an implementation point of view) as it can be applied to any Streett automaton (regardless of the class of the recognized property).

Discussion

One of the important challenges in runtime verification is the practical interest of the specification formalism. An ideal specification language should be easy to use by end-users. Moreover, a desirable feature, advocated by this paper, is the need for addressing both infinite and finite execution sequences. One could reproach the two following facts to the proposed synthesis approach:

-First, several mechanisms are needed: DFAs, Streett automata, and finally verification and enforcement monitors. -Second, one may question the usefulness of the DFA to Streett transformations. Arguably, it would be possible to generate monitors directly for properties specified by Streett automata (written by hand or generated from temporal logic formula).

In our point of view, using the DFA2Streett transformations in the synthesis process has the three following advantages:

-The DFA2Streett transformations complete the picture of the Safety-Progress classification, by providing constructive tools in the automata view that are the counterparts of the language-theoretic operators (A, E, R, P , A f , E f , R f , P f ) in the language view. -The direct translation from a supposed ideal specification formalism to a Streett automaton would be difficult. This formalism would have to address both finite and infinite behaviors, requiring a design expertise. It is likely that such a translation would be error-prone or lead to ambiguous specifications. -One of the underlying arguments for using our approach is that the end-user is only required to specify a finite behavior and indicate the wished pattern (used with the finitary property). Thus, the infinite behavior is comprehended by the user by only seeing patterns like "always", "at least once", "regularly", or "persistently". The user is thus kept from specifying the infinite behavior with Streett automata.

A complex translation is avoided, replaced by two simpler transformations, and the required work from the user seems to be simpler.

Conclusion and future work

Conclusion. We have extended the Safety-Progress classification of properties in a runtime validation context. This hierarchical organization of properties turned out to be a convenient framework for specifying properties purposed to be used at runtime. We addressed in a unified way the problem of monitorability and enforceability of properties at runtime using this general framework. We provided the first exact characterization of monitorable properties according to the classical definition of monitorability proposed by Pnueli and Zaks. We generalized the classical definition of monitorability by parameterizing it by a truth-domain. We introduced a new definition of monitorability based on distinguishability of good and bad execution sequences. This definition is based on positive and negative determinacy as well. However, we believe that it better corresponds to practical needs and tool implementations and fits better in the hierarchy of properties. Moreover, this alternative definition is able to better distinguish equivocal situations that a monitor would have to face off without a finite sequence interpretation. Furthermore, we have delineated the set of enforceable properties w.r.t. the SP classification. This set of properties was characterized independently from any enforcement mechanism. It is thus an upper-bound for the set of properties that could be addressed by any enforcement mechanism. Furthermore, we have given general synthesis procedures to generate runtime and enforcement monitors in this framework.

Future work. The proposed approach raises new research perspectives and open questions. First, it seems interesting to consider this approach in the testing perspective.

A monitor (passively) observes the execution of the program. Notably it has no control on the produced events and their sequencing. In a testing context, the notion of controllable event is introduced. An interesting issue would be to characterize the set of testable properties in the SP framework, as it was initiated in [START_REF] Falcone | More Testable Properties[END_REF]. Note that the definitions of positive and negative determinacy is rather appropriate in this context. Indeed, in a test campaign one is concerned with the set of all execution sequences that can be produced by the underlying program. Notions of positive and negative determinacy seem to be a first approximation of the set of possible future execution sequences of a program. An additional issue to take into consideration is to deal with a reduced observability on the system under scrutiny. In practical situations, the desired property may refer to events out of the observation scope of a monitor. Similarly, it seems interesting to see how it is possible to characterize the set of properties for which other runtime-verification derived techniques can be applied (e.g., runtime reflection [START_REF] Leucker | A brief account of runtime verification[END_REF]).

Another research perspective is to relax the soundness and transparency constraints or consider different definitions of runtime enforcement. Specific enforcement mechanisms shall be designed. For instance, augmented enforcers may enjoy more handling abilities on the sequences submitted in input. It seems interesting to see the impact on the set of enforceable properties.

Furthermore, an interesting question would be to investigate how the automata-view of the SP classification transposes to other sets of properties such as contextfree languages. The classification used in this paper focuses on regular properties. In the quest of expressiveness for specification languages, relying on a classification appears as a good way to delineate monitorable and enforceable properties.

Finally, the question of expressiveness is somehow also related to parametric properties, i.e., the properties expressed using events with formal parameters whose concrete values are obtained at runtime. Lots of runtime verification frameworks now handle parametric properties. Among them, two kinds of approaches can be distinguished in state-of-the-art frameworks:

-RuleR [START_REF] Barringer | Rule systems for run-time monitoring: from eagle to ruler[END_REF] is able to handle expressive parametric specifications thanks to a general approach based on rule rewriting, -MOP [START_REF] Chen | Parametric trace slicing and monitoring[END_REF] has been recently leveraged with the socalled slicing approach to monitor some form of parametric specification in a more efficient way.

It is rather clear that being able to express parametric properties is an asset in runtime verification and is surely desirable from a practical point of view. Now, as runtime verification is always concerned with efficiency, one question is to find the right balance between the gained expressiveness and the induced overhead. That is, a runtime verification framework should be chosen so as to meet the just needed level of expressiveness to specify the requirements. Moreover, another related question is to investigate whether it is more efficient to enhance expressiveness by considering parametric properties or using a more expressive specification formalism.

A Proofs

A.1 Proofs for Section 4

A.1.1 Proof of Property 2: Closure of r -properties

We prove the two facts in order:

1 We have either φ(σ) or ϕ(σ), i.e., all prefixes σ ′ of σ belong to ψ. Necessarily, all prefixes σ ′′ of σ ′ also belong to ψ, that is ψ(σ ′′ ). By definition, that means σ ′ ∈ A f (ψ), i.e., φ(σ ′ ) and Π(σ ′ ). 2 Π(σ) implies that σ has at least one prefix σ 0 σ belonging to ψ: σ ∈ E f (ψ). Then, any continuation of σ built using any finite or infinite sequence σ ′ has at least the same prefix belonging to ψ.

If σ ′ ∈ Σ * , we have σ 0 σ σ•σ ′ and σ•σ ′ ∈ E f (ψ). If σ ′ ∈ Σ ω , we have σ 0 σ ≺ σ • σ ′ and σ • σ ′ ∈ E(ψ). ⊓ ⊔ A.1.2 Proof of Theorem 1: Soundness of the transformations of DFAs to Streett automata Considering a DFA A ψ = (Q A ψ , q A ψ init , → A ψ , F ) (
we omit the superscript of F for the sake of clarity), s.t. L(A ψ ) = ψ, we have to prove that:

A Π = DFA2S _Saf (A ψ ) ⇒ L(A Π ) = (A f (ψ), A(ψ)) A Π = DFA2S _Guar (A ψ ) ⇒ L(A Π ) = (E f (ψ), E(ψ)) A Π = DFA2S _Resp(A ψ ) ⇒ L(A Π ) = (R f (ψ), R(ψ)) A Π = DFA2S _Per (A ψ ) ⇒ L(A Π ) = (P f (ψ), P (ψ))
In the following proofs, for a finite sequence σ of length n, we may use the notion of run of σ on A ψ or on a Streett automaton A Π obtained by the transformations. We note:

-run(σ, A ψ ) = q 0 • • • q n , -run(σ, A Π ) = q ′ 0 • • • q ′ n .
For Safety properties. We show that the r -property accepted by A Π (obtained using DFA2S _Saf ) is exactly (A f (ψ), A(ψ)).

Let σ ∈ Σ ∞ s.t. (A f (ψ), A(ψ))(σ), let us prove that the sequence σ is accepted by A Π . We have two cases: σ is a finite sequence or not.

-Let us consider σ ∈ Σ * s.t. |σ| = n, then by definition of r -properties: σ ∈ A f (ψ), i.e., every prefix of σ belongs to ψ. Let us examine run(σ, A ψ ) = q 0 • • • q n . As L(A ψ ) = ψ, we have ∀i ∈ [0, n], q i ∈ F . By definition of the transformation DFA2S_Saf, we have ∀i ∈ [0, n], q i ∈ P . According to (TSafe1), we have run(σ, A Π ) = q 0 • • • q n . Using the acceptance criterion for finite sequences, σ is accepted by A Π . -Let σ ∈ Σ ω , then by definition of r -properties: σ ∈ A(ψ), i.e., every finite prefix of σ belongs to ψ. Let us suppose that σ is not accepted by A Π . According to the acceptance criterion for infinite sequences (Definition 6), we would have vinf (σ, A Π ) ⊆ P (as A Π is a safety automaton, R = ∅). By definition of the transformation DFA2S _Saf and the shape of the obtained automaton A Π , we have vinf (σ, A Π ) = {sink }. Using (TSafe2), we know that there exists a smallest prefix σ ′ of σ, s.t. the run of σ ′ on A Π reaches the state sink . By the definition of DFA2S _Saf , we can deduce that the run of σ ′ on A ψ ends in a state in F . As L(A ψ ) = ψ, σ ′ / ∈ ψ. We obtain a contradiction with σ ∈ A(ψ), and σ is actually accepted by A Π .

Let σ be a sequence accepted by A Π , let us prove that σ ∈ (A f (ψ), A(ψ)). We distinguish again two cases: σ is a finite sequence or not.

-Let σ ∈ Σ * s.t. |σ| = n, then by definition of the acceptance criterion for finite sequences of Streett automata (Definition 7), we have q ′ n ∈ P . As A Π is a safety automaton, we can deduce that ∀i ∈ [0, n], q ′ i ∈ P . Following the definition of DFA2S _Saf , we find that all the states visited during the run of σ on A ψ are in F : ∀i ∈ [0, n], q i ∈ F (and q i = q ′ i ). By definition of the acceptance criterion for DFAs, we can deduce that every prefix of σ is accepted by A ψ . As L(A ψ ) = ψ, we can deduce that all prefixes of σ belong to ψ, i.e., σ ∈ A f (ψ).

-If σ ∈ Σ ω , then by definition of the acceptance criterion for infinite sequences (Definition 6), we know that vinf (σ, A Π ) ⊆ P . Let us suppose that σ / ∈ A(ψ), by definition of the operator A (see Definition 2), there exists a strict prefix σ ′ of σ not belonging to ψ.

Let n ′ = |σ ′ |. As L(A ψ ) = ψ, the run of σ ′ on A ψ , run(σ ′ , A ψ ) = q 0 • • • q n ′ , satisfies q 0 = q A ψ init ∧ q n ′ / ∈ F .
According to the definition of the transformation DFA2S _Saf and the rule (TSafe2), we have q ′ n ′ = sink / ∈ P . Furthermore, using (TSafe3), every continuation of σ ′ has its run ending in sink . We deduce that vinf (σ, A Π ) = {sink } ⊆ P . Which is a contradiction with the initial hypothesis, and gives us σ ∈ A(ψ).

⊓ ⊔

For Guarantee properties. We show that the sets of sequences accepted by A Π obtained by DFA2S _Guar are exactly (E f (ψ), E(ψ)).

Let σ ∈ Σ ∞ s.t. (E f (ψ), E(ψ))(σ), let us prove that the sequence σ is accepted by A Π . We have two subcases: σ is a finite sequence or not.

- ), we have ∀i ∈ [n ′ , n], q i ∈ R. According to the acceptance criterion for finite sequences, σ is accepted by A Π .

∈ Σ * , σ ′ ≺ σ min ⇒ σ ′ / ∈ ψ. Let us examine run(σ min , A ψ ) = q 0 • • • q n ′ . As L(A ψ ) = ψ, we have ∀i ∈ [0, n ′ -1], q i / ∈ F ∧ q n ′ ∈ F . According to (TGuar2), we have run(σ min , A Π ) = q 0 • • • q n ′ with ∀i ∈ [0, n ′ -1], q i / ∈ R ∧ q n ′ ∈ R. Following (TGuar1
-Let σ ∈ Σ ω , then by definition of r -properties: σ ∈ E(ψ), i.e., (at least) one finite prefix of σ belongs to ψ.

Let us suppose that σ is not accepted by A Π . According to the acceptance criterion for infinite sequences (Definition 6), we have vinf (σ, A Π ) ∩ R = ∅ (as A Π is a guarantee automaton, P = ∅). In other words, we have vinf (σ, A Π ) ⊆ R. As A Π is a guarantee automaton, every state visited by the run of σ on A Π is in R. Indeed, according to the shape of the transition function of guarantee automata, if a state of R is visited, we have vinf (σ, A Π )∩R = ∅. Let us consider now the prefixes of σ. During the run of these prefixes on A Π , none of them visits an R-state. It follows that, according to (TGuar2), none of the runs on A Π of these prefixes visits a state in F . As L(A ψ ) = ψ, we deduce that none of the prefixes of σ belongs to ψ. We obtain a contradiction with σ ∈ E(ψ), and consequently σ is actually accepted by A Π .

Let σ be a sequence accepted by A Π , let us prove that σ ∈ (E f (ψ), E(ψ)). We distinguish two cases: σ is a finite sequence or not.

-Let σ ∈ Σ * s.t. |σ| = n, then by definition of the acceptance criterion for finite sequences (Definition 7), we have q n ∈ R. Let us suppose that σ / ∈ E f (ψ), i.e., none of the prefixes of σ belongs to ψ. As L(A ψ ) = ψ, the run of σ on A ψ satisfies: ∀i ∈ [0, n], q i / ∈ F . Starting from q A ψ init = q A Π init / ∈ R, and using (TGuar2), we find that run(σ,

A Π ) = q ′ 0 • • • q ′ n with ∀i ∈ [0, n], q ′ i / ∈ R
. This is a contradiction with q ′ n ∈ R, and thus σ ∈ E f (ψ). -Let σ ∈ Σ ω , then by definition of the acceptance criterion for infinite sequences (Definition 6), we have vinf (σ, A Π )∩R = ∅. As A Π is a guarantee automaton, it means that vinf (σ, A Π ) ⊆ R. According to the shape of the transition function for guarantee automata, it means that there is a prefix σ ′ of σ on A Π for which the run switches from states in R to states in R. More formally,

∃σ ′ ∈ Σ * , σ ′ ≺ σ ∧ |σ ′ | = n ′ ∧ ∀i ∈ [0, n ′ -1], q ′ i ∈ R ∧ ∀i ≥ n ′ , q ′ i ∈ R.
Let us suppose that σ / ∈ E(ψ), i.e., σ has no prefix belonging to ψ. As L(A ψ ) = ψ, the run of σ on A ψ satisfies: ∀i ∈ N, q i / ∈ F . Similarly to the finitary case, and according to the transformation DFA2S_Guar (TGuar2), it would question the existence of σ ′ . We deduce that σ ∈ E(ψ). ⊓ ⊔ For Response properties. We show that the r -property accepted by A Π , obtained with DFA2S _Resp is exactly

(R f (ψ), R(ψ)). Let σ ∈ Σ ∞ s.t. (R f (ψ), R(ψ))(σ)
, let us prove that the sequence σ is accepted by A Π . We have two subcases: σ is a finite sequence or not.

-Let σ ∈ Σ * , thus σ ∈ R f (ψ). Proving that σ is accepted by A Π amounts to show that the run of σ on A Π , i.e., run(σ, A Π ), ends in a R-state (i.e., q ′ n ∈ R). First of all, let us remark that σ ∈ R f (ψ) gives us ψ(σ). Furthermore, as L(A ψ ) = ψ, we can deduce that q

n ∈ F . As σ ∈ R f (ψ), ∀n ∈ N, ∃σ ′ ∈ Σ * , σ ≺ σ ′ ∧ |σ ′ | ≥ n ∧ ψ(σ ′ ) (cf. Definition 3). Let n ′ = |F | be the number of accepting states of A ψ . Now let us consider the set S = {σ" ∈ Σ * | σ ≺ σ ′′ ∧ |{σ ′ ∈ Σ * | σ ≺ σ ′ ≺ σ ′′ ∧ σ ′ ∈ ψ}| > n ′ }.
This set contains the sequences which are continuations of σ and have at least n ′ prefixes longer than σ and belonging to ψ. As σ ∈ R f (ψ), we know that S = ∅, thus S has a smallest element σ min . Let us examine the run of σ min on A ψ : run(σ, A ψ ) = run(σ, A Π ) = q 0 • • • q |σmin| = q 0 • • • q n • • • q |σmin| . Between q n and q |σmin| , there are at least n ′ + 1 accepting states. As |F | = n ′ , two states between q n and q |σmin| are identical. Moreover, we have ∀i ∈ [n, |σ min |-1], q i → A ψ q i+1 . Which allows us to deduce, using the definition of DFA2S _Resp that q n = q ′ n is tagged as a R-state. According to the acceptance criterion for finite sequences, σ is accepted by A

Π . -Let σ ∈ Σ ω , thus σ ∈ R(ψ), i.e., ∀σ ′ ∈ Σ * , ∃σ ′′ ∈ Σ * , σ ′ ≺ σ ′′ ≺ σ ∧ ψ(σ ′′ ) holds for σ.
Let us examine the run of σ on A Π , we will show that this run visits at least one R-state infinitely often. Indeed, let us consider a prefix σ ′ of σ, we can find an unbounded number of σ ′continuations σ ′′ , s.t. ψ(σ ′′ ). Furthermore, for each of these continuations, it is possible to find an unbounded number of continuations σ ′′′ s.t. ψ(σ ′′′ ). Using L(A ψ ) = A ψ , the runs of the sequences σ ′′ and the sequences σ ′′′ on the automaton A ψ end on a F -state. Using the same reasoning as the one used for finite sequences, the state on which the run of σ ′′ on A Π is a R-state. Thus we can build a series (σ i ) i∈N of σ-prefixes (of strictly growing length) s.t. the run of each σ i ends in a R-state.

Thus an infinite number of prefixes of σ go through a R-state. As |R| ∈ N, there exists a state in R visited infinitely often during the run of σ on A Π . According to the acceptance criterion for infinite sequences, σ is accepted by A Π .

Let σ be a sequence accepted by A Π , let us prove that σ ∈ (R f (ψ), R(ψ)). We distinguish again two cases: σ is a finite sequence or not.

-Let σ ∈ Σ * s.t. |σ| = n, then by definition of the acceptance criterion for finite sequences (Definition 7), we have q ′ n ∈ R. According to the definition of the transformation DFA2S _Resp, we deduce that q n ∈ F and ∃q 0 , . . . , q l ∈ Q A ψ , ∃e 0 , . . . , e l ∈ Σ,

∀j ∈ [0, l -1], q j ei -→ A ψ q j+1 (13) ∃i ∈ [0, l], ∃j ∈ [i, l -1], q j ∈ F ∧ q i = q l ∧ q 0 = q (14)
Thus we can build a series (σ j ) j∈N of σ-continuations s.t. ∀j ∈ N, ψ(σ j ) and σ j is defined as

σ j = σ • e 0 • • • e i • (e i+1 • • • e l-1 •e 0 • • • e i ) j
. This series exhibits strictly growing continuations of σ belonging to ψ. According to the definition of the operator R f , we can deduce that σ ∈ R f (ψ).

-Let σ ∈ Σ ω , then by definition of the acceptance criterion for infinite sequences (Definition 6), we have vinf (σ, A Π )∩R = ∅. Thus, σ has an infinite number of prefixes for which the run ends in a R-state. Using the definition of DFA2S _Resp, we know that all these prefixes are accepted by A ψ (as by definition the ending state of their run is a R-state). Using L(A ψ ) = ψ, we know that all these prefixes belong to ψ and have an unrestricted number of continuations belonging to ψ. We can deduce that σ ∈ R(ψ).

⊓ ⊔

For Persistence properties. We show that the set of sequences accepted by A Π , obtained with DFA2S _Per is exactly (P f (ψ), P (ψ)). Let us remark that, according to the definition of the transformation (the transition function is not changed), we have ∀j ∈

[n -1, n ′ + n ′′ -1], q ′ j -→ A Π q ′ j+1 ∧ q j -→ A ψ q j+1 . Moreover, as Q A Π = Q A ψ ,
we can merge the states q j and q ′ j visited by the runs of σ on A ψ and A Π .

Let σ ∈ Σ ∞ s.t. (P f (ψ), P (ψ))(σ), let us prove that the sequence σ is accepted by A Π . We have two subcases: σ is a finite sequence or not.

-Proving that σ is accepted by A Π amounts to show that the of σ on A Π ends in a P -state (q n ∈ P ). First of all, let us remark that σ ∈ P f (ψ) gives us ψ(σ). Furthermore, as L(A ψ ) = ψ, we can deduce that q n-1 ∈ F . As σ ∈ P f (ψ), there exist σ ′ , µ ∈ Σ * s.t. (cf. Definition 3):

σ σ ′ ∧ (σ ′ • µ * • pref (µ)) ⊆ ψ (15)
Let n ′ = |σ ′ |, and n ′′ = |µ|. Then, the runs of σ ′ and σ ′ • µ on A Π can be expressed:

run(σ ′ , A Π ) = q 0 • • • q n • • • q n ′ run(σ ′ • µ, A Π ) = q 0 • • • q n • • • q n ′ • q n ′ +1 • • • q n ′ +n ′′
According to [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF], we have q n ′ ∈ F . We can show by induction that

run(σ • µ * , A Π ) = q 0 • • • q n ′ • (q n ′ +1 • • • q n ′ +n ′′ ) * .
Moreover, we have ∀j ∈ [n ′ + 1, n ′ + n ′′ ], q ′ j ∈ F and q n ′ +n ′′ -→ A Π q n ′ +1 . We can deduce, following the definition of DFA2S _Per , that q n ∈ P . Indeed, it is sufficient to take l = n ′ + n ′′n and i = n ′ + 1n.

-In order to prove vinf (σ, A Π ) ⊆ P , it is sufficient to see that σ can be expressed σ ′ • µ ω . From this, every prefix of σ longer than σ ′ satisfies ψ, and has its run which stops in a F -state on A ψ . Thus, we exhibit a strongly connected component of F -states which are tagged as P -states by DFA2S_Per. Thus, the states visited infinitely often during the run of σ on A Π are the states of this strongly connected component. Which gives us the expected result.

Let σ be a sequence accepted by A Π , let us prove that σ ∈ (P f (ψ), P (ψ)). We distinguish two subcases: σ is a finite sequence or not.

-Let σ ∈ Σ * s.t. |σ| = n, then by definition of the acceptance criterion for finite sequences of Streett automata (Definition 7), we have q n ∈ P . Then, there exist two cases.

• In the first one, we have on one hand q n ∈ F , and on the other hand ∃n ∈ N \ {0}, ∃q 0 , . . . , q n ∈ Q A ψ s.t.:

-∀j ∈ [0, n -1], q j -→ A ψ q j+1 , and

-∃i ∈ [0, n-1], ∀j ∈ [i, n], q j ∈ F ∧q i = q n ∧q 0 = q n We have ψ(σ) since L(A ψ ) = ψ. Moreover, there exist e 0 , . . . , e n-1 ∈ Σ s.t. ∀j ∈ [0, n-1], q j ej -→ A ψ q j+1 . We can deduce that ψ(σ•e 0 • • • e i ), ψ(σ•e 0 • • • e i •e i+1 ), . . . , ψ(σ • e 0 • • • e n-1 ). Let us note L p = σ ′ • (e 0 • • • e n ) * • e 0 + (e 0 • • • e n ) * • e 0 • e 1 + . . . + (e 0 • • • e n ) * • e 0 • • • e n-1 .
As q i = q n ({q i , . . . , q n } is a strongly connected component), we can prove by induction that L p ⊆ ψ. Furthermore, ∀σ

′ ∈ Σ * ∩ L p , σ • e 0 • • • e i σ ′ ⇒ ψ(σ ′ ). Which proves that σ ∈ P f (ψ). Indeed, it is sufficient to take σ ′ = σ • e 0 • • • e i , and µ = e i+1 • • • e n-1 .
• In the second one, we have q n ∈ F and q n -→ A ψ q n . Thus, ∃e ∈ Σ, q n e -→ A ψ q n . We deduce that ψ(σ) and σ • e * ⊆ ψ, as L(A ψ ) = ψ. Which allows us to deduce easily that σ ∈ P f (ψ).

-Let σ ∈ Σ ω , then by definition of the acceptance criterion for infinite sequences of Streett automata (Definition 6), we have vinf (σ, A Π ) ⊆ P . That is to say, all prefixes of σ from a certain point on have their run which ends in a P -state. As the automaton A Π has a finite number of states, it means that there exists a strongly connected component C, s.t. the run of σ on A Π "stays in". More formally, ∃n, m ∈

N, C = {q ′ 0 , . . . , q ′ n } ⊆ Q A Π ∧ run(σ, A Π ) = q 0 • • • q m • • • ∧ ∀i > m, q i ∈ C. Moreover, as {q ′ 0 , . . . q ′ n } is a SCC, from
′ 0 e0 -→ A Π q ′ 1 e1 -→ A Π • • • en-1 -→ A Π q ′ n en -→ A Π q ′
0 , with e 0 , . . . , e n ∈ Σ. According to the definition of DFA2S _Per , we have the same transitions on A ψ , i.e., q ′ 0 e0

-→ A ψ q ′ 1 e1 -→ A ψ • • • en-1 -→ A ψ q ′ n en -→ A ψ q ′ 0 . Let us note L p = σ ′ • (e 0 • • • e n ) * • (e 0 + e 0 • e 1 + . . . + e 0 • • • e n-1 ) = σ ′ • (e 0 • • • e n ) • pref (e 0 • • • e n-1
-∃µ 1 ∈ Σ * , ∀µ ′ 1 ∈ Σ ∞ , ¬Π 1 (σ • µ 1 • µ ′ 1 ), Π 1 is nega- tively determined by σ • µ 1 , or, -∃µ 1 ∈ Σ * , ∀µ ′ 1 ∈ Σ ∞ , Π 1 (σ • µ 1 • µ ′ 1 ), Π 1 is posi- tively determined by σ • µ 1 .
As Π 2 is also monitorable, it is σ • µ 1 -monitorable, there exists µ 2 s.t. Π 2 is negatively or positively determined by σ•µ 1 •µ 2 . That is we have the two following subcases :

-∃µ 2 ∈ Σ * , ∀µ ′ 2 ∈ Σ ∞ , ¬Π 2 (σ • µ 1 • µ 2 • µ ′ 2 ), Π 2 is negatively determined by σ • µ 1 • µ 2 , or, -∃µ 2 ∈ Σ * , ∀µ ′ 2 ∈ Σ ∞ , Π 2 (σ • µ 1 • µ 2 • µ ′ 2 ), Π 2 is positively determined by σ • µ 1 • µ 2 .
By combination, there exist four cases depending on the facts that Π 1 is positively or negatively determined by σ • µ 1 and Π 2 is negatively or positively determined by σ • µ 1 • µ 2 . We group them into two cases: -Let us distinguish the case where Π 1 is positively determined by σ • µ 1 and Π 2 is positively determined by σ

• µ 1 • µ 2 . Then, by taking µ = σ • µ 1 • µ 2 ,
we have that Π 1 ∧ Π 2 is positively determined by µ. This gives us the expected result. -In the others cases, it suffices to take µ The set of obligation r -properties is the set of all kobligation r -properties for k ∈ N, where a k-obligation is expressed as follows (Lemma 1):

= σ • µ 1 • µ 2 to show that Π 1 ∧ Π 2 is negatively determined by µ. -The proof of Π 1 ∨ Π 2 ∈ MP c is similar. -The proof of ¬Π 1 ∈ MP c is
k i=1 (Safety i ∪ Guarantee i ),
where Safety i and Guarantee i are safety and guarantee r -properties. Let Π ∈ Obligation(Σ), there exists k ∈ N s.t. Π ∈ k-Obligation(Σ). The proof relies on an induction on k and uses the following facts:

-Safety and guarantee properties are monitorable. Here is the proof17 :

-Let Π = (A f (ψ), A(ψ)) be a safety r -property, and σ ∈ Σ * . The proof is done by distinguishing two cases : either there exists a continuation σ ′ ∈ Σ * of σ s.t. ¬Π(σ ′ ), or there does not exist. In the first case, we have ¬A f (ψ)(σ ′ ), i.e., σ ′ does not have all of its prefixes in ψ. Then, the same holds for every continuation σ ′′ of σ

′ : ∀σ ′′ ∈ Σ * , σ ′ σ ′′ ⇒ ¬A f (ψ)(σ ′′ ). It follows that ∀σ ′′ ∈ Σ * , σ σ ′ σ ′′ ⇒ ¬Π(σ ′′ ).
That is to say Π is negatively determined by σ ′ . In the second case, every continuation of σ satisfies Π. That is Π is positively determined by σ • ǫ.

-Let Π = (E f (ψ), E(ψ)) be a guarantee r -property, let us prove that Π is monitorable. We prove this property by reductio ad absurdum. Let suppose the existence of a reactivity r -property Π = (φ, ϕ) defined on Σ which is neither a safety nor a guarantee: Π ∈ Reactivity(Σ) \ (Safety(Σ) ∪ Guarantee(Σ)), and which is monitorable according to Definition 17 with B 3 .

As Π ∈ MP * (B 3 ), by definition we have:

∀σ good ∈ φ, ∀σ bad ∈ φ, [[Π]] B3 (σ good ) = [[Π]] B3 (σ bad )
Let us remark that φ = ∅ and φ = ∅ as Π is neither a safety nor a guarantee. Indeed, if φ = ∅, then Π would be necessarily the r -property false, which is a safety. Likewise, if φ = ∅, i.e., φ = Σ * , Π would be the r -property true which is a safety as well.

Then, we consider two sequences σ good and σ bad in Σ ∞ :

-Let σ good ∈ φ s.t. there exists σ ′ g ∈ Σ ∞ with ¬Π(σ good • σ ′ g ). We know that such a sequence exists since Π / ∈ Guarantee(Σ). This is a consequence of Property 2.

-Let σ bad ∈ φ s.t. there exists σ ′ b ∈ Σ ∞ with Π(σ bad • σ ′ b ). We know that such a sequence exists since Π / ∈ Safety(Σ). This is a consequence of Property 2.

According to the definition of the evaluation function for r -properties in a truth-domain (Definition 16), we have:

[[Π]] B3 (σ good ) = [[Π]] B3 (σ bad ) =?
This is a contradiction with Π ∈ MP * (B 3 ). ⊓ ⊔

A.2.4 Proof of Theorem 3: Multi-valued characterization of alternative monitorability

We prove each of these facts successively. Let Π = (φ, ϕ) be an r -property.

Proof of (i).

-Let Π ∈ Safety(Σ), we show that Π ∈ MP * (B ⊥ 2 ). As Π ∈ Safety(Σ), there exists a finitary property ψ ⊆ Σ * , s.t. Π = (A f (ψ), A(ψ)). Let us consider σ good ∈ φ and σ bad ∈ φ, we want to prove that the evaluations in B ⊥ 2 of these two sequences differ. On one hand, we have Π(σ good ) (since σ good ∈ φ) and thus [[Π]] B ⊥ 2 (σ good ) =?. On the other hand, we have ¬Π(σ bad ) and σ bad / ∈ A f (ψ) (since σ bad / ∈ φ). Using Property 2, we have ∀µ ∈ Σ ∞ , ¬Π(σ bad • µ), i.e.,

[[Π]] B ⊥ 2 (σ bad ) = ⊥. -Let Π ∈ MP * (B ⊥
2 ), we show that Π ∈ Safety(Σ). According to the characterization of safety properties given in Property 1, showing that Π is a safety r -property amounts to show that it verifies Π = (A f (Pref (φ)), A(Pref (ϕ))). This is what we do by showing the inclusion in both ways.

-Π ⊓ Σ * ⊆ A f (Pref (φ)) is immediate as for every sequence σ ∈ Π ⊓ Σ * (i.e., σ ∈ φ), σ has all of its prefixes in Pref (φ). The same holds for Π ⊓Σ ω ⊆ A(Pref (ϕ)). -Let us show that A f (Pref (φ)) ⊆ Π ⊓ Σ * . Let σ ∈ A f (Pref (φ)), we prove that σ ∈ Π ⊓ Σ * . As σ ∈ A f (Pref (φ)), all prefixes of σ belong to Pref (φ).

That is, all prefixes of σ are the prefixes of a sequence in φ. Let σ min be the smallest word in φ which is an continuation of σ. We distinguish two The same reasoning can be conducted to show that A(Pref (ϕ)) ⊆ Π ⊓ Σ ω . Finally, according to the definition of r -properties (Definition 1), we know that Π = (φ, ϕ) can be written Π = (A f (Pref (φ)), A(Pref (ϕ))), which gives us the expected result.

Proof of (ii).

-The reasoning used to prove that Guarantee(Σ) ⊆ MP * (B ⊤ 2 ) is similar to the reasoning used to prove Safety(Σ) ⊆ MP * (B ⊥

2 ). It suffices to show that all bad execution sequences are evaluated to "?". Furthermore, all good execution sequences are evaluated to ⊤. Indeed, once a sequence satisfies a guarantee rproperty, all its continuations also satisfy it.

-Proving that MP * (B ⊤

2 ) ⊆ Guarantee(Σ) can be done, following the reasoning used to prove MP * (B ⊥ is given by Lemma 3.

Proof of (iv). The proof is straightforward by noticing that every r -property can be evaluated by effectively distinguishing good and bad sequences. In others words, any reactivity r -property can be evaluated consistently with B 4 . Indeed, a good sequence σ good is evaluated to ⊤ c or ⊤ according to its continuations. A bad sequence σ bad is evaluated to ⊥ c or ⊥ according to its continuations. As we can see here, the truth values ⊥ c and ⊤ c refine the verdict "?". ⊓ ⊔ A. Proof of q n ∈ Good AΠ ⇔ [[Π]](σ) = ⊤ -Let us suppose that q n ∈ Good A Π . Using the acceptance criterion for finite sequences, we have that σ is accepted by A Π . Furthermore, as A Π specifies Π, we have Π(σ). Now, let us consider µ ∈ Σ + s.t. |σ|+|µ| = n ′ > n and run(σ • µ, A Π ) = q 0 • • • q n ′ -1 . As q n ∈ Good A Π , we deduce ∀k ∈ N, n ≤ k ≤ n ′ -1 ⇒ q k ∈ m i=1 R i ∪ P i and consequently Π(σ • µ). Let us consider µ ∈ Σ ω , one may remark that ∀i ∈ [1, m], vinf (σ• µ, A Π ) ∩ R i = ∅ ∨ vinf (σ • µ, A Π ) ⊆ P i , which implies Π(σ • µ). We have Π(σ) ∧ ∀µ ∈ Σ ∞ , Π(σ • µ), i.e.,

Π ) = q 0 • • • q n • • • q k ⇒ q k ∈ m i=0 R i ∪ P i .
That is to say Reach A Π (q n ) ⊆ m i=1 (R i ∪ P i ), i.e., q n ∈ Good AΠ .

Proof of q n ∈ Good AΠ -Let us suppose that q n ∈ Good AΠ c . Using the acceptance criterion for finite sequences, we have that σ is accepted by A Π . Moreover, as A Π specifies Π, we deduce Π(σ). Now, as Reach A (q) ⊆ m i=1 (R i ∪ P i ), there exists a state q ′ of A Π reachable from q and belonging to m i=1 (R i ∩ P i ). Consequently, there exists µ ∈ Σ * s.t. run(σ • µ) = q 0 • • • q n • • • q ′ . Still following the acceptance criterion we deduce ¬Π(σ • µ), i.e., -Let us suppose that q n ∈ Bad AΠ c . Using the acceptance criterion of finite sequences, we have that σ is not accepted by A Π . Furthermore, as A Π specifies Π, we deduce ¬Π(σ). Now, as Reach A (q) ⊆ m i=1 (R i ∪ P i ), there exists a state q ′ of A Π reachable from q and belonging to m i=1 (R i ∪ P i ). Consequently, there exists µ ∈ Σ * s.t. run(σ • µ) = q 0 • • • q n • • • q ′ . Still following the acceptance criterion, we deduce Π(σ • µ), i.e., [[Π]](σ) = ⊥ c .

-Conversely, the same reasonning can be conducted.

Proof of q n ∈ Bad AΠ ⇔ [[Π]](σ) = ⊥. The proof can be done following the same proof principle that the one used to prove q n ∈ Good AΠ ⇔ [[Π]](σ) = ⊤.

-Let us suppose that q n ∈ Bad A Π . Using the acceptance criterion on finite sequences, we have that σ is not accepted by A Π . Furthermore, as A Π specifies Π, we deduce ¬Π(σ). Now, let us consider µ ∈ Σ + s.t. |σ|+|µ| = n ′ > n and run(σ •µ, A Π ) = q 0 • • • q n ′ -1 . As q n ∈ Bad A Π , we have ∀k ∈ N, n ≤ k ≤ n ′ -1 ⇒ q k ∈ m i=1 R i ∩ P i and consequently ¬Π(σ • µ). Let us consider µ ∈ Σ ω , one may remark that ∀i ∈ [1, m], vinf (σ• µ, A Π ) ∩ R i = ∅ ∧ vinf (σ • µ, A Π ) ⊆ P i , which implies ¬Π(σ • µ). We have ¬Π(σ) ∧ ∀µ ∈ Σ ∞ , ¬Π(σ • µ), i.e., [[Π]](σ) = ⊥.

-Conversely, let us suppose that [[Π]](σ) = ⊥. By definition, it means ∀µ ∈ Σ ∞ , ¬Π(σ • µ). According to the acceptance criterion of Streett automata, we deduce ∀k ≥ n, ∀µ ∈ Σ * , run(σ

• µ, A Π ) = q 0 • • • q n • • • q k ⇒ q k ∈ m i=0 R i ∩ P i .
That is to say Reach A Π (q n ) ⊆ m i=1 (R i ∩ P i ), i.e., q n ∈ Bad AΠ . ⊓ ⊔ A.3 Proofs for Section 6 A.3.1 Proof of Property 4: Equivalence between enforcement criteria Before proving the equivalence between enforcement criteria, we state and prove an intermediate lemma.

Lemma 4. Considering an m-automaton A Π recognizing an r-property Π = (φ, ϕ) and s ∈ S(A Π ) a strongly connected component of A Π . We have:

I s = ∅ ⇔ ∀σ ∈ Σ ω , vinf (σ, A Π ) = s ⇒ ¬ϕ(σ)
The proof is in two steps by proving implications in both ways.

-Suppose I s = ∅ and let us consider σ ∈ Σ ω s.t.

vinf (σ, A Π ) = s. As I s = ∅, then ∃i ∈ I s (⊆ [1, m]), vinf (σ, A Π ) ⊆ R i ∧ vinf (σ, A Π ) ∩ P i = ∅. Then, using the acceptance criterion for infinite sequences, one can deduce that σ is not accepted by A Π . -The other direction is straightforward using the acceptance criterion for infinite sequences (Definition 6). ⊓ ⊔ Now, let us prove Property 4. This proof relies on the computation of strongly connected components of a Streett automaton (SCC), both maximal and non maximal ones. The proof is in two steps by proving implications in both ways.

-(4) ⇒ (5). Let s be a SCC of A Π s.t. I s = ∅. Then using the previous lemma, every sequence s.t. vinf (σ, A Π ) = s is rejected by A Π . As Π is enforceable and satisfies (4), necessarily all prefixes of σ terminating in a state of s are not accepted. Otherwise, there would exist an accepting state (wrt. the acceptance criterion of finite sequences) in s. It would then be possible to build σ ′ ∈ Σ ω with an infinite number of accepting prefixes, i.e., s.t. (4) is not satisfied. -(5) ⇒ (4). Let us consider σ ∈ Σ ω s.t. ¬ϕ(σ). During its run on A Π , σ visits an SCC s infinitely often. As ¬ϕ(σ), using the previous lemma, we have I s = ∅. Using (5), ∃i ∈ I s , vinf (σ, A Π ) ⊆ P i (and we already know vinf (σ, A Π ) ⊆ R i ). Let us consider σ ′ ∈ Σ * s.t. σ ′ ≺ σ, the run of σ ′ on A Π is s.t. ∃q 1 , . . . , q n ∈ Q A Π , run(σ ′ , A Π ) = q A Π init •q 1 • • • q n •{q ∈ vinf (σ, A Π )} * . Consequently, we have ∀σ ′ ≺ σ, |σ ′ | ≥ n ⇒ run(σ, A Π ) = q A Π init • • • q, with q ∈ R i ∧ q ∈ P i . Using the acceptance criterion for finite sequences, we have that σ ′ is not accepted by A Π . ⊓ ⊔ A.3.2 Proof of Theorem 8: Enforceable m-reactivity properties are response properties We show that any enforceable m-reactivity property Π is indeed a response property. The proof is based on the automata view, showing that the (m-reactivity) automaton A Π associated to Π can be transformed into a response automaton A Π ′ recognizing the same language. Let us consider A Π = (Q A Π , q A Π init , Σ, -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) the Streett automaton associated to an enforceable property Π. We now consider the response automaton A Π ′ = (Q A Π , q A Π init , Σ, -→ A Π , {(R ′ 1 , ∅), . . . , (R ′ m , ∅)}) with R ′ i = R i ∪ P i for i in [1, m]. We now show that a sequence σ of Σ ∞ is accepted by A Π if and only if it is accepted by A Π ′ . We distinguish two cases according to whether σ is a finite or an infinite sequence.

-For a finite sequence σ, it is an accepting sequence of A Π if and only if its run terminates either in a R i -state or in a P i -state for i in [1, m]. Consequently its run also terminates in a R ′ i -state of A Π ′ for i in [1, m], and therefore it is an accepting sequence of A Π ′ . -For an infinite sequence σ, note that the sets vinf (σ, A Π ) and vinf (σ, A Π ′ ) coincide. Let us assume first that σ is an accepting sequence of A Π , namely m i=1 vinf (σ, A Π ) ∩ R i = ∅ ∨ vinf (σ, A Π ) ⊆ P i .

Since R ′ i ⊆ R i and R ′ i ⊆ P i we have

m i=1 vinf (σ, A Π ) ∩ R ′ i = ∅.
Consequently, σ is an accepting sequence of A Π ′ . Now, let us assume that σ is a non-accepting sequence of A Π . Since Π is enforceable, then, according to Property 4, there exists i ∈ [1, m] such that vinf (σ, A Π ) ⊆ R i and vinf (σ, A Π ) ⊆ P i . Thus, we can deduce vinf (σ, A Π ) ⊆ (R i ∩P i ) and, consequently, vinf (σ, A Π ′ ) ⊆ R ′ i . Therefore, σ is a non-accepting sequence of A Π ′ . ⊓ ⊔

Fig. 1 .

 1 Fig. 1. Principle of runtime verification

Fig. 2 .

 2 Fig. 2. Principle of runtime enforcement

ΣFig. 3 .Fig. 4 .

 34 Fig. 3. Examples of Streett automata

Fig. 8 .

 8 Fig. 8. The Safety-Progress classification of r -properties

Fig. 7 .

 7 Fig. 7. Characterization of states for basic classes

Fig. 9 .Fig. 10 .

 910 Fig. 9. Non-monitorable response property -R = {1}, P = ∅

Definition 15 ( 3 . 5 (

 1535 Parameterized classical monitorability). For a truth-domain B s.t. B ∩ {⊥, ⊤} = ∅, an r -property Π is: σ-monitorable with B, if there exist b ∈ B and a (finite) µ ∈ Σ * s.t. b = ⊥ and Π is negatively determined by σ • µ, or b = ⊤ and Π is positively determined by σ • µ; -monitorable with B if it is σ-monitorable with B for every σ ∈ Σ * . For a truth-domain B, we will note MP (B) the set of monitorable properties, according to the definition of parameterized classical monitorability. We now tackle the question of how the underlying considered truth-domain may influence the class of monitorable properties, according to a truth-domain derived from B 3 . Remark 4 (MP c = MP (B 3 )). The previous parameterized definition of classical monitorability amounts to the classical definition given by Pnueli and Zaks when instantiated with B Remark Finer truth-domains). According to Definition 15, we can notice that adding further truth-values to B 3 has no influence on the set of monitorable properties. That is: ∀B : B ⊃ B 3 ⇒ MP (B) = MP (B 3 ).

Fig. 12 .

 12 Fig. 12. Non-enforceable persistence r -property

Fig. 14 .

 14 Fig. 14. Examples of Verification Monitors

Fig. 15 .

 15 Fig. 15. Examples of Enforcement Monitors

  cases. If σ min = σ, then σ ∈ Π. Else (σ ≺ σ min ), as σ min ∈ φ, we have[[Π]] B ⊥ 2 (σ min ) =?; and consequently [[Π]] B ⊥ 2 (σ) =? (otherwise, we could not have [[Π]] B ⊥ 2 (σ min ) =?). Using Π ∈ MP * (B ⊥ 2 ), we obtain σ ∈ φ and consequently σ ∈ Π.

  2 ) ⊆ Safety(Σ), by showing that if Π ∈ MP * (B ⊤ 2 ), then Π verifies Π = E f (Pref (φ)), E(Pref (ϕ)) . Proof of (iii) -The proof of Safety(Σ) ∪ Guarantee(Σ) ⊆ MP * (B 3 )is straightforward by noticing that:-MP * (B ⊥ 2 ) ⊂ MP * (B 3 ), -and MP * (B ⊤ 2 ) ⊂ MP * (B 3). -The fact that MP * (B 3 ) ⊆ Safety(Σ) ∪ Guarantee(Σ)

2 . 5

 25 Proof of Property 3: Correspondence between Streett automata states and B 4 In this proof, [[Π]] stands for [[Π]] B4 . Let us consider an execution sequence σ ∈ Σ * of length n.

  [[Π]](σ) = ⊤. -Conversly, let us suppose that [[Π]](σ) = ⊤. By definition, it means ∀µ ∈ Σ ∞ , Π(σ • µ). According to the acceptance criterion of Streett automata, we deduce ∀k ≥ n, ∀µ ∈ Σ * , run(σ • µ, A

c⇔

  [[Π]](σ) = ⊤ c .The proof is straightforward by examining the acceptance criterion for finite sequences.

  [[Π]](σ) = ⊤ c .-Conversely, the same reasonning can be used to prove the seeked result.Proof of q n ∈ Bad AΠ c ⇔ [[Π]](σ) = ⊥ c .Similarly, the proof is straightforward by examining the acceptance criterion for finite sequences of Streett automata.

  consists of all finite words σ s.t. all prefixes of σ belong to ψ. One can observe that A f (ψ) is the largest prefix-closed subset of ψ. E f (ψ) consists of all finite words σ s.t. some prefixes of σ belong to ψ. One can observe that E f (ψ) = ψ • Σ * . R f (ψ) consists of all finite words σ s.t. ψ(σ) and there exists an infinite number of continuations σ ′ of σ also belonging to ψ. P f (ψ) consists of all finite words σ belonging to ψ s.t. there exists a continuation σ ′ of σ s.t. σ ′ persistently has continuations σ ′′ staying in ψ (i.e., σ ′ • σ ′′ belongs to ψ).

Table 1 .

 1 Ways to specify properties according to the views

		Language view	Automata view
	Finite seq	∈ X f (ψ)	Finite seq criterion
		(Def. 2)	(Def. 7)
	Infinite seq	∈ X(ψ)	Infinite seq criterion
		(Def. 3)	(Def. 6)

Table 2 .

 2 Recognizing criteria according to the considered view

  2.1. Let us consider two r -properties Π 1 , Π 2 ∈ MP c . -The proof of Π 1 ∧Π 2 ∈ MP c consists in showing that Π 1 ∧ Π 2 is σ-monitorable for any sequence σ ∈ Σ * . Let σ ∈ Σ * , let us exhibit an extension µ ∈ Σ * s.t. Π 1 ∧Π 2 is negatively or positively determined by σ•µ. As Π 1 is monitorable, there exists a sequence µ 1 s.t. Π 1 is positively or negatively determined by σ • µ 1 . Then, as Π 2 is monitorable, there exists a sequence µ 2 s.t. Π 1 ∧ Π 2 is negatively or positively determined by σ • µ 1 • µ 2 . Then, one has to analyze the different Boolean combinations to obtain the expected result. -The proof of Π 1 ∨ Π 2 ∈ MP c is similar. -The proof of ¬Π 1 ∈ MP c is straightforward by noticing that for any sequence σ ∈ Σ * , if Π 1 is positively (resp. negatively) determined by σ, then ¬Π is negatively (resp. positively) determined by σ. ⊓ ⊔

  monitorable, and thus B 3 -monitorable; but not B ⊤ 2 -monitorable. -The property Π 2 specified by A Π2 is B ⊤ 2 -monitorable and B ⊥ 2 -monitorable, and thus B 3 -monitorable. -The property Π 3 specified by A Π3 is B ⊥ 2 -monitorable, and thus B 3 -monitorable, but not B ⊤ 2 -monitorable. -The property Π 4 specified by A Π4 is B ⊥ 2 -monitorable, and thus B 3 -monitorable, but not B ⊤ 2 -monitorable.

Theorem 5 (Automata view of alternative monitorability). The r-property Π recognized by the Streett m-automaton

  Let us consider σ ∈ Σ * s.t. |σ| = n, then by definition of r -properties: σ ∈ E f (ψ), i.e., σ has at least one prefix which belongs to ψ. Let us consider S sat = {σ ′ ∈ Σ * | σ ′ σ∧σ ′ ∈ ψ}, the set of prefixes of σ which belong to ψ. As σ ∈ E f (ψ), we can deduce that S sat = ∅, S sat has thus a smallest element σ min . Let n ′ = |σ min |. We have, by definition of σ min , ∀σ ′

  every state of C it is possible to reach any state of C. Let us suppose, without loss of generality, that q

  ). The sequence σ can be expressed σ ′ • (e 0 • • • e n ) ω with the fact that for every sequence σ ′′ ∈ L p which is a continuation of σ ′ , the run of σ ′′ ends in a P -state. Which implies that the runs of these same sequences σ ′′ on A ψ end in a F -state. As L(A ψ ) = ψ, we deduce that ∀σ ′′ ∈ L p , σ ′ σ ′′ ≺ σ ⇒ ψ(σ ′′ ).Let us consider two r -properties Π 1 , Π 2 ∈ MP c .

	Which allows to deduce, using the definition of the op-
	erator P (see Section 4.2), that σ ∈ P (ψ).
	⊓ ⊔
	A.2 Proofs for Section 5
	A.2.1 Proof of Lemma 2: Closure of monitorable
	properties under boolean operations

-Proof of Π 1 ∧ Π 2 ∈ MP c . It consists in showing that Π 1 ∧ Π 2 is σ-monitorable for any sequence σ ∈ Σ * . Let σ ∈ Σ * ,

let us exhibit an extension µ ∈ Σ * s.t. Π 1 ∧Π 2 is negatively or positively determined by σ •µ. As Π 1 is monitorable, there exists µ 1 s.t. Π 1 is negatively or positively determined by σ • µ 1 , that is we have the two following subcases:

This is the distinction, made by Schneider[START_REF] Schneider | Enforceable security policies[END_REF], between properties and (general) policies. The set of properties (defined over single execution sequences) is a subset of the set of policies (defined over sets of execution sequences).

Using a pair of sets makes the distinction between the finitary and infinitary parts of the property more explicit.

The interested reader may consult[START_REF] Havelund | Verify your runs[END_REF] (resp.[START_REF] Falcone | You should better enforce than verify[END_REF]) for more information on runtime verification (resp. runtime enforcement).

In the following, the term property will stand for regular property.

There exist several equivalent definitions of Streett automata dedicated to the recognition of infinite sequences. We choose here to follow the definition used in[START_REF] Chang | The Safety-Progress Classification[END_REF].

In[START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF], guarantee properties are named co-safety properties.

Seen in the logical view, this property can be defined by the temporal logic formula p ∨ ♦q.

This property can be expressed in an event-based LTL as (req ⇒ ♦ack ).

An alternative interpretation could consist in correcting an erroneous sequence by adding extra events.

Note that those criteria differ from the existence of bad prefixes. Bad prefixes are sequences which cannot be extended to correct (finite or infinite) ones, i.e., sequences that determine negatively the underlying property.

The synthesis of Verification Monitors is presented for rproperties in MP * (B 4 ) and can be adapted in a straightforward manner for other sets of monitorable properties using the results in Section 5.

In the general case, the comparison between input and output sequences is performed up to some equivalence relation ≈⊆ Σ ∞ × Σ ∞ . Note that the considered equivalence relation should preserve the r -property under consideration.

This latter case is avoided in[START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF] by assuming that properties under consideration always contain ǫ Σ .

From a more general perspective, we can see this limitation from a runtime verification point of view. Verifying infinitary properties at runtime on a produced execution sequence, in essence, should be done by checking finite prefixes of the current sequence.

Yliès Falcone et al.: What can you Verify and Enforce at Runtime ?

The proof can also be done by examining the syntactic restriction applying to an automaton recognizing a safety or a guarantee property: for all σ ∈ Σ * , there exists a continuation µ s.t. this property is negatively or positively determined by σ • µ. For instance, in a safety automaton, for each state there exists a path which leads either to a terminal strongly connected component of states in which the property is satisfied or in a terminal strongly connected component in which the property is not satisfied.

Acknowledgements. The authors of the paper would like to gratefully thank Howard Barringer, Klaus Havelund, Thierry Jéron, Hervé Marchand, and the anonymous reviewers for their helpful remarks.