On topologies for (hyper)properties Michele Pasqua and Isabella Mastroeni University of Verona - Dipartimento di Informatica Strada le Grazie 15, 37134, Verona, Italy (michele.pasqua|isabella.mastroeni)@univr.it Abstract. Usually, systems properties are defined in terms of the infi- nite executions which satisfy it. In this work we explore what happens if we allow finite executions in properties definitions. In particular, we give a topological interpretation of the safety/liveness classification in the do- mains of: only finite, only infinite and mixed executions. Then we extend our reasoning to hyperproperties, namely sets of sets of executions (or sets of properties). Also in this case we give a topological interpretation of the hypersafety/hyperliveness classification in the three domains. 1 Introduction In the field of security, with verification is intended the general process of check- ing whether a system complies with a policy, i.e., a formal description of what systems are allowed and are not allowed to do (with respect to the policy). Ver- ification can only figure out whether a system performs not allowed behaviors. When the security mechanism has the power also to affect the system execu- tion in order to guarantee a policy, then we say that the mechanism enforce it. Hence, enforcement guarantees that the system under control behaves like a safe system. In order to perform verification/enforcing, it is necessary to have a model of the system and a way for formalizing the policy we need to check. Usually, sys- tems are modeled by means of the set of their execution traces, namely histories of states, for a given formalization of systems states, reached during computa- tion. This system model induces a corresponding policy formalization in terms of set of execution traces satisfying the policy, i.e., in terms of trace properties. A trace property is a system property that can be checked on each trace, for in- stance a system is deadlock free if each execution is deadlock free. Unfortunately not all policies fall in this category (e.g., information flows), hence hyperprop- erties [3] were introduced. An hyperproperty is a set of sets of execution traces and it allows us to specify relations between executions, modeling in this way properties of sets of executions, as it happens in information flow when we can detect a flow only by comparing different executions. Another aspect to take in consideration is how to represent systems histories. Despite the fact that, in general, systems at some point in time may stop their execution, in the literature the majority of works represent histories as infinite sequences of states. This is justified by the fact that systems are supposed to potentially run forever, and by the fact that a terminating computation can be represented as an infinite one repeating the last state infinitely many times. The verification/enforcing of trace properties over infinite sequences is well founded and it has a strong background, theoretical and practical. In particular it relies on the well known classification of trace properties: safety and liveness. Informally, the first model the fact that “nothing bad will happen” and the second model the fact that “something good will eventually happen”. Despite its simplicity, this classification allows us to describe, by using topological ar- guments, a generic trace property as the disjunction of a safety property and a liveness property [1]. This is very appealing since, in order to check a generic trace property, it is sufficient to check its safety and its liveness parts. When introducing hyperproperties in [3], the authors also give a topological characterization of hypersafety and hyperliveness, namely the sets of sets coun- terparts of safety and liveness, which allow to decompose a generic hyperproperty in its hypersafety and hyperliveness parts. In this work, we explore what happens if we consider finite executions in properties definitions, namely if we take in consideration also the cases where histories are only finite sequences, only infinite sequences and mixed sequences (finite and infinite). We noted, for example, that the notion of “safety” is slightly different in these three cases. For doing so we propose a topological interpretation to the safety/liveness classification, parametric on the type of admitted histories. Furthermore, we extend this reasoning to hyperproperties, giving a topological interpretation also to the hypersafety/hyperliveness classification. 2 Background and notations Given an alphabet (a set of symbols) Σ, we denote with Σ n the set of sequences def of S symbols in Σ of length n ∈ N and with  the empty sequence. Then Σ ∗+ = n ω+ n>0 Σ is the set of non-empty finite sequences, Σ is the set of non-empty ∞+ def ∗+ ω+ infinite sequences and Σ = Σ ∪Σ is the set of all non-empty sequences. We write Σ ∗ , Σ ω and Σ ∞ to indicate the finite Σ ?+ ∪ {}, infinite Σ ω+ ∪ {} and all Σ ∞+ ∪ {} sequences, respectively. The concatenation of sequences σ ∈ Σ ∗ and σ 0 ∈ Σ ∞ is the sequence σσ 0 ∈ Σ . Sequence σ ∈ Σ ∗ is a prefix of σ 00 ∈ Σ ∞ , in symbols σ  σ 00 , if exists ∞ σ 0 ∈ Σ ∞ such that σσ 0 = σ 00 . When we deal with sets of sequences, we can extend the definition of prefix to sets as follows. A set of sequences X ⊆ Σ ∗ is a prefixset of Y ⊆ Σ ∞ , in symbols X E Y , if for all σ ∈ X exists σ 0 ∈ Y such that σ  σ 0 [3]. A set of infinite sequences {σ0 , σ1 , . . . } converges to the limit sequence σ if the length of the maximal prefix common to each σk and to σ goes to infinity as k goes to infinity [2]. For example, {an bω | n ≥ 0} converges to aω , in fact the sequence of longest prefixes common to aω and to σk = ak bω (i.e., ak ) gets increasingly longer with k. Given a set X, we denote with |X| its cardinality, i.e., its size, and with ℘(X) its powerset, i.e., the set of all its subsets. Given a function f : X → − X def and Y ⊆ X, we denote with f [Y ] = {f (x) | x ∈ Y } the direct image of f on Y def and with f ↑ = λY . {f (x) | x ∈ Y } the image-lift to sets of f . In the following, S we use uppercase letters X, Y, Z, . . . to denote sets of sequences and we use uppercase calligraphic letters X , Y, Z, . . . to denote sets of sets of sequences. Topologies A topology over a set X consists in a family of subsets of X which defines its open sets. OXS ⊆ ℘(X) is a family of open sets iff it is closed under union (i.e., ∀Y ⊆ OX . Y ∈ OX ), it is closed under binary S intersection (i.e., Y1 , Y2 ∈ OX ⇒ Y1 ∩ Y2 ∈ OX ) and it includes X (i.e., OX = X). The dual of an open set is a closed set, so a family of open sets defines automatically a family of closed sets, namely CX = {X \ O | O ∈ OX }. Given Y ⊆ X: – the interior of Y , written ι(Y ), is the largest open set contained in Y , i.e., [ ι(Y ) = {O ∈ OX | O ⊆ Y } – the closure of Y , written ρ(Y ), is the smallest closed set containing Y , i.e., \ ρ(Y ) = {C ∈ CX | Y ⊆ C} A set D ⊆ X is said dense iff ρ(D) = X, so in a topology there is also a family of dense sets, i.e., DX = {D ⊆ X | ρ(D) = X}. Every element of ℘(X) can be specified as the intersection of a closed set and a dense set. We have not found any explicit proof in the literature, so we give a simple one here. Note that the proof also provides a way for retrieving the closed and the dense sets whose intersection is the given element of ℘(X). Theorem 1 (Decomposition). ∀Y ∈ ℘(X) (∃C ∈ CX , D ∈ DX . Y = C ∩ D). Proof. Y = ρ(Y ) ∩ Y = (ρ(Y ) ∩ Y ) ∪ ∅ = (ρ(Y ) ∩ Y ) ∪ (ρ(Y ) ∩ (X \ ρ(Y ))) = ρ(Y ) ∩ (Y ∪ (X \ ρ(Y ))). But ρ(Y ) ∈ CX and Y ∪ (X \ ρ(Y )) ∈ DX . In fact ρ(Y ∪ (X \ ρ(Y ))) ⊇ ρ(Y ) ∪ ρ(X \ ρ(Y )) ⊇ ρ(Y ) ∪ (X \ ρ(Y )) = X. t u A function κ : ℘(X) → − ℘(X) is a Kuratowski Closure Operator (KCO) iff all the following hold: 1. κ(∅) = ∅ 2. ∀Y ⊆ X . Y ⊆ κ(Y ) 3. ∀Y1 , Y2 ⊆ X . κ(Y1 ∪Y2 ) = κ(Y1 )∪κ(Y2 ) [this implies Y1 ⊆ Y2 ⇒ κ(Y1 ) ⊆ κ(Y2 )] 4. ∀Y ⊆ X . κ(κ(Y )) = κ(Y ) A KCO over ℘(X) induces a topology on X where the KCO is the closure of X [6]. So, in order to define a topology on X, it is sufficient to specify its closed sets, namely a closure (or a KCO) over ℘(X). 2.1 Properties vs hyperpropertis If systems are modeled with execution traces, the evolution of a system is de- scribed in terms of some objects ς ∈ Σ, called states. So a system behavior is represented by a non-empty set of sequences over Σ (i.e., its execution traces). A trace property is a set of sequences and a traceset property, also called hyper- property [3], is a set of sets of sequences or, equivalently, a set of trace properties. A set of sequences X satisfies a property P iff X ⊆ P . A set of sequences X satisfies an hyperproperty HP iff X ∈ HP. The trace property ∅, or false, is the one which cannot be satisfied, by any system, i.e., @X . X ( false (∅ is not a system). Dually, the trace property which contains all the possible sequences, called true, is the one which is satisfied by every system, i.e., ∀X . X ⊆ true. Analogously, we can define falseh and trueh for hyperproperties as {false} and ℘(true), respectively [3]. In the security context, a policy is a boolean predicate over systems, i.e., it checks if systems exhibit allowed or a not allowed behaviors. Some policies can be expressed as trace properties, like access control, and others cannot, like non- interference. In this latter case it is necessary to specify it as an hyperproperty. Intuitively, a property is defined exclusively in terms of individual executions and, in general, do not specify a relation between different executions of the system. Instead, an hyperproperty specifies the set of systems allowed by the policy, and so it has the power to express relations between executions. In [3] it is stated that in order to formalize policies, it is sufficient to consider hyperprop- erties. This means that hyperproperties are able to define every possible security policy (for systems modeled as set of states sequences). It is worth noting that in order to disprove whether a system fulfills a trace property it is necessary to show one trace, which is the counterexample. Analo- gously, in order to disprove that a system fulfills an hyperproperty is necessary to show a set of traces (potentially all system traces). 3 (Hyper)safety and (hyper)liveness dichotomy In the literature, among all, there are two particular kinds of trace properties: the safety and the liveness. Informally, the first model the fact that “nothing bad will happen” and the second model the fact that “something good will eventually happen”. In other words, a system violates a safety property if it eventually performs the “bad thing” and a system violates a liveness property if it never performs the “good thing”. It is clear that, if a system do not satisfy a safety property, the violation must occur during its execution and hence the violation must arise in a finite amount of time. Due to this fact, safety properties are identified as the ones which can be monitored, i.e., checked at runtime. For liveness properties things are more complicated because the checker must observe the system execution entirely, hence it needs a, possibly infinite, amount of time. Finite executions can be seen as particular cases of infinite ones: we can repeat infinitely many times the final state of a finite execution in order to obtain an infinite execution equivalent to the finite one. This has led researchers to model system executions and trace properties as set of infinite sequences of (systems) states. This choice has also two other important motivations: reasoning about properties can be done with well studied formalisms modeling semantics by considering infinite sequences (like linear temporal logics and Büchi automata), and it allows us to give a topological characterization of trace properties. It turns out that safety properties corresponds to the closed sets in the Cantor topology over infinite sequences and liveness properties corresponds to the dense sets. Hence, by using the decomposition theorem (Thm. 1), we can specify an arbitrary property as the intersection of a safety and a liveness one. This means that we can reduce the check of a generic trace property to the check of its safety and liveness parts. While properties over finite traces can be easily expressed as infinite se- quences, in practice we deal with systems which exhibit finite behaviors. So it is natural to wonder what happens if we allow finite sequences in properties definition. Something in this direction was already done [8], but only for safety properties. In this section, we give a properties characterization on the following execution domains: only finite ℘(Σ ∗ ), only infinite ℘(Σ ω ) and mixed ℘(Σ ∞ ). 3.1 Safety Let us start with safety first and denote by Safety∗ , Safetyω and Safety∞ the safety properties over finite, infinite and mixed executions, respectively. In [1], Alpern and Schneider define safety properties S on ℘(Σ ω ) in a refutational way: if σ ∈/ S then there is a finite sequence σ 0  σ such that σ 0 σ 00 ∈ / S for every 00 σ ∈ Σ ω . This means that, if an infinite execution violates the property, then the bad thing must have been occurred in one of its finite prefixes and the violation cannot ever be recovered in the future. An alternative, and equivalent, definition due to Roşu [8] is the following: for a safety property S ∈ ℘(Σ ω ), σ ∈ S iff pref(σ) ⊆ pref↑ (S), where pref : Σ ∞ → − ℘(Σ ∗ ) is the function 0 00 ∞ 0 00 λσ . {σ | ∃σ ∈ Σ . σ σ = σ} returning the set of prefixes of a given sequence. Furthermore, Roşu in [8] discusses the known definitions of safety properties over finite, infinite and mixed executions, and their equivalence with the following: – Safety∗ = {S ∈ ℘(Σ ∗ ) | S = pref↑ (S)} def – Safetyω = {S ∈ ℘(Σ ω ) | σ ∈ S ⇔ pref(σ) ⊆ pref↑ (S)} def – Safety∞ = {S ∈ ℘(Σ ∞ ) | σ ∈ S ⇔ pref(σ) ⊆ S} def Although safety properties essentially capture the fact that, in order to disprove the property, it is sufficient to show a finite counterexample, the definitions of safety on finite, infinite and mixed sequences are different. For finite sequences it is sufficient the prefix-closure, namely a safety on Σ ∗ must contain all the prefixes of its sequences. The same definition cannot be applied to Σ ω , indeed none of its prefixes are in the property. In this case we have to reason “at the limit” and say that a safety on Σ ω contains all its limit sequences, namely the infinite sequences which approximate the prefixes. Finally, as expected, the safety on Σ ∞ combine both aspects of finite and infinite sequences. 3.2 Liveness To the best of our knowledge, there are no works reasoning about liveness prop- erties over finite and mixed executions. One can think that it is not meaningful to define liveness on finite executions, but we believe it is not the case. Take as example termination, i.e., the set of systems executions which do not run forever. Clearly this properties is liveness, where the good thing is exactly termination. We can model this property on finite sequences only, as the set Σ ∗ . So, let us denote with Liveness∗ , Livenessω and Liveness∞ the liveness properties over fi- nite, infinite and mixed executions, respectively. The original definition of Alpern and Schneider [1] involves infinite sequences only, and it states that a property L ∈ ℘(Σ ω ) is a liveness property iff for every finite sequence σ ∈ Σ ∗ there exists an infinite sequence σ 0 ∈ Σ ω such that σσ 0 is in L. This means that every finite execution can be extended to an infinite one satisfying the property. We believe that this intuition can be easily adapted to finite and mixed sequences as well. Definition 1. Given y ∈ {∗, ω, ∞}: Livenessy = {L ∈ ℘(Σ y ) | ∀σ ∈ Σ ∗ ∃σ 0 ∈ L . σ  σ 0 } def Liveness properties capture the fact that in order to disprove the property is nec- essary to show an infinite counterexample. It is worth noting that our definition of liveness on infinite executions is indeed equivalent to the one of Alpern and Schneider. Moreover, ∀σ ∈ Σ ∗ ∃σ 0 ∈ L . σ  σ 0 is equivalent to Σ ∗ ⊆ pref↑ (L). Finally, we can note that, as usual, the trace property false is a safety property for ℘(Σ ∗ ), ℘(Σ ω ) and ℘(Σ ∞ ) but it is a liveness one for none of them. Analogously, Σ ∗ ∈ Safety∗ ∩ Liveness∗ , Σ ω ∈ Safetyω ∩ Livenessω and Σ ∞ ∈ Safety∞ ∩ Liveness∞ (here Σ ∗ , Σ ω and Σ ∞ are the true trace property). 3.3 Hypersafety In their seminal paper [3], Clarkson and Schneider introduce hyperproperties and they extend the safety/liveness dichotomy on sets of sets of sequences. Their work, as well as all other works about hyperproperties, deals with infinite exe- cutions only. In this section, we mimic what we have done for properties in the hyper case. Let us denote by HyperSafety∗ , HyperSafetyω and HyperSafety∞ the safety hyperproperties over finite, infinite and mixed executions, respectively. In [3] the authors define hypersafety in a refutational way: if X ∈ / HS then there is a finite set of finite sequences O E X such that every possible X 0 ∈ ℘(Σ ω ) which extends O (i.e., O E X 0 ) is not in HS. This is basically the concept of safety lifted to sets, where the “bad thing” is exactly the set O. Here we define hypersafety for finite, infinite and mixed executions, lifting to sets the definitions of safety, where spref : ℘(Σ ∞ ) → − ℘(℘(Σ ∗ )) is the function λX . {Y | Y E X} = 0 0 {Y | ∀σ ∈ Y ∃σ ∈ X . σ  σ } returning the set of prefixsets of X. Note that spref do not constrain prefixsets to have finite size, indeed in our definitions we allow the “bad thing” set to be infinite. – HyperSafety∗ = {HS ∈ ℘(℘(Σ ∗ )) | HS = spref↑ (HS)} def – HyperSafetyω = {HS ∈ ℘(℘(Σ ω )) | X ∈ HS ⇔ spref(X) ⊆ spref↑ (HS)} def – HyperSafety∞ = {HS ∈ ℘(℘(Σ ∞ )) | X ∈ HS ⇔ spref(X) ⊆ HS} def Hypersafety essentially capture the fact that, in order to disprove the property, it is sufficient to show a counterexample-set of finite traces. Hence, also in the hyper level, we have the link between safety properties and the concept of mon- itorability. In fact, as a safety property can be disproved at runtime observing one execution until the “bad thing” happens, an hypersafety can be disproved at runtime observing a set of executions until the “bad thing” happens. Note that, this set can have an unbounded (or infinite) number of elements hence, in general, the monitorability of an hypersafety is unfeasible. But there are some exceptions. For k-hypersafety, i.e., safety hyperproperties for which the bad thing never involves more than k traces (see [3] for details), the set of traces which need to be monitored can be restricted to k (i.e., a finite number of) elements. In order to characterize hypersafety for finite sequences, it is sufficient the prefixset-closure, namely an hypersafety on Σ ∗ must contain all the prefixsets of its sequences. The same definition cannot be applied to Σ ω , indeed none of its prefixsets are in the property. In this case, again, we have to reason “at the limit” and say that an hypersafety on Σ ω contains all its sets of limit sequences, namely the sets of infinite sequences which approximate the prefixsets. Finally, as expected, the hypersafety on Σ ∞ combine both aspects of finite and infinite sequences. Furthermore, it is worth noting that our definition of hypersafety on infinite executions is indeed equivalent to the one of Clarkson and Schneider, if we constrain spref to collect only finite prefixsets. 3.4 Hyperliveness Let us now denote by HyperLiveness∗ , HyperLivenessω and HyperLiveness∞ the liveness hyperproperties over finite, infinite and mixed executions, respectively. In [3], the original definition states that an hyperproperty HL ∈ ℘(℘(Σ ω )) is hyperliveness iff for every finite set of finite sequences O ∈ ℘(Σ ∗ ) it exists a set of infinite sequences X ∈ ℘(Σ ω ), which extends O (i.e., O E X), such that X is in HL. Also in this case, the definition is basically the concept of liveness lifted to sets. Here we give an alternative definition, which turns out to be parameterizable on finite, infinite and mixed executions, has it happens for properties case. As we have done for hypersafety, in our definitions we relax the constraint that the observable O needs to be a finite set. Definition 2. Given y ∈ {∗, ω, ∞}: HyperLivenessy = {HL ∈ ℘(℘(Σ y )) | ∀O ∈ ℘(Σ ∗ ) ∃X ∈ HL . O E X} Hyperliveness captures the fact that, in order to disprove the property, it is necessary to show a set of infinite counterexamples. It is worth noting that our definition of hyperliveness on infinite executions is indeed equivalent to the one of Clarkson and Schneider if we constrain every O to be finite. Furthermore, the condition ∀O ∈ ℘(Σ ∗ ) ∃X ∈ HL . O E X is equivalent to: ℘(Σ ∗ ) ⊆ spref↑ (HL). Finally, we can note that, as expected, the hyperproperty falseh is hy- persafety for ℘(℘(Σ ∗ )), ℘(℘(Σ ω )) and ℘(℘(Σ ∞ )) but it is hyperliveness for none of them. Analogously, ℘(Σ ∗ ) ∈ HyperSafety∗ ∩ HyperLiveness∗ , ℘(Σ ω ) ∈ HyperSafetyω ∩ HyperLivenessω and ℘(Σ ∞ ) ∈ HyperSafety∞ ∩ HyperLiveness∞ (here ℘(Σ ∗ ), ℘(Σ ω ) and ℘(Σ ∞ ) are the trueh hyperproperty). 4 Topologies for properties and hyperproperties When dealing with infinite computations there is a topological interpretation of safety and liveness, also for the hyper case (see [3]). In this section, we give topological characterizations of safety/liveness properties and hyperproperties which take in consideration finite and mixed computations other than infinite ones. For doing so, we define a KCO for each domain (finite, infinite, mixed for properties and finite, infinite, mixed for hyperproperties) and then we prove that safety and liveness are closed and dense sets, respectively, in the topology induced by the KCO. 4.1 Properties def The function PrefCl : ℘(Σ ∗ ) →− ℘(Σ ∗ ), defined as PrefCl = λX . pref↑ (X), is a closure on ℘(Σ ∗ ) (indeed it is a KCO). So we have a topology on Σ ∗ , where: – CΣ ∗ = PrefCl ↑ (℘(Σ ∗ )) = {X ⊆ Σ ∗ | X = PrefCl(X)} are the closed sets – DΣ ∗ = {X ⊆ Σ ∗ | PrefCl(X) = Σ ∗ } are the dense sets Proposition 1. Safety∗ = CΣ ∗ and Liveness∗ = DΣ ∗ . Proof. Since elements X ∈ Safety∗ are prefix-closed, i.e., X = pref↑ (X), Safety∗ is equal to CΣ ∗ by definition. As we already noted, ∀σ ∈ Σ ∗ ∃σ 0 ∈ X . σ  σ 0 is equivalent to Σ ∗ ⊆ pref↑ (X). But pref↑ (X) ⊆ Σ ∗ , for every X ∈ ℘(Σ ∗ ). Hence PrefCl(X) = Σ ∗ , i.e., X ∈ DΣ ∗ , iff X ∈ Liveness∗ . t u Hence, exploiting the decomposition theorem (Thm. 1) we have that: ∀P ∈ ℘(Σ ∗ ) . (∃S ∈ Safety∗ , L ∈ Liveness∗ . P = S ∩ L) ω Let lim − ℘(Σ ω ) the function λX . {σ ∈ Σ ω | ∀σ 0 ∈ Σ ∗ . (σ 0  σ ⇒ : ℘(Σ ω ) → 0 ↑ σ ∈ pref (X))} returning the set of limit sequences of X. The function LimCl : def ω ℘(Σ ω ) →− ℘(Σ ω ), defined as LimCl = λX . lim (X), is a closure on ℘(Σ ω ) (indeed it is a KCO). So we have a topology on Σ ω , where: – CΣ ω = LimCl ↑ (℘(Σ ω )) = {X ⊆ Σ ω | X = LimCl(X)} are the closed sets – DΣ ω = {X ⊆ Σ ω | LimCl(X) = Σ ω } are the dense sets Proposition 2. Safetyω = CΣ ω and Livenessω = DΣ ω . Proof. Our definitions of safety and liveness (on Σ ω ) are equivalent to the one of [1] and LimCl is the limit operator of [5], so our characterization is equivalent to the usual topological definition of safety and liveness properties over Σ ω . tu Hence, exploiting the decomposition theorem (Thm. 1) we have that: ∀P ∈ ℘(Σ ω ) . (∃S ∈ Safetyω , L ∈ Livenessω . P = S ∩ L) Let lim∞ : ℘(Σ ∞ ) → − ℘(Σ ∞ ), defined as λX . X ∪ {σ ∈ Σ ω | ∀σ 0 ∈ Σ ∗ . (σ 0  σ ⇒ ω σ 0 ∈ X)}1 , the version on mixed sequences of lim. The function LimPrefCl : def ℘(Σ ∞ ) →− ℘(Σ ∞ ), defined as LimPrefCl = λX . lim ◦ pref↑ (X), is a closure on ∞ ℘(Σ ) (indeed it is a KCO). So we can define a topology on Σ ∞ , where: ∞ – CΣ ∞ = LimPrefCl ↑ (℘(Σ ∞ )) = {X ⊆ Σ ∞ | X = LimPrefCl(X)} are the closed sets – DΣ ∞ = {X ⊆ Σ ∞ | LimPrefCl(X) = Σ ∞ } are the dense sets Proposition 3. Safety∞ = CΣ ∞ and Liveness∞ = DΣ ∞ . Proof. Note that LimPrefCl(X) = pref↑ (X) ∪ {σ ∈ Σ ω | ∀σ 0 ∈ Σ ∗ . (σ 0  σ ⇒ σ 0 ∈ pref↑ (X)} = pref↑ (X) ∪ {σ ∈ Σ ω | pref(σ) ⊆ pref↑ (X)}. Safety case. First we prove CΣ ∞ ⊆ Safety∞ . Let X ∈ CΣ ∞ . For all σ ∈ X we have that σ ∈ pref↑ (X) or σ ∈ {σ ∈ Σ ω | pref(σ) ⊆ pref↑ (X)} and, both cases, imply pref(σ) ⊆ X. In fact: σ ∈ pref↑ (X) ⇒ pref(σ) ⊆ pref↑ (X) ⊆ X σ ∈ {σ ∈ Σ ω | pref(σ) ⊆ pref↑ (X)} ⇒ pref(σ) ⊆ pref↑ (X) ⊆ X For all σ ∈ / X we have that σ ∈ / pref↑ (X) and σ ∈ / {σ ∈ Σ ω | pref(σ) ⊆ pref↑ (X)}. If σ is finite then σ ∈ / pref↑ (X) implies pref(σ) 6⊆ pref↑ (X), since σ ∈ pref(σ). Otherwise pref(σ) 6⊆ pref↑ (X) is obvious. Note that pref↑ (X) = X ∩ Σ ∗ hence, in both cases, we have pref(σ) 6⊆ X. All this means that X ∈ Safety∞ . Now we prove Safety∞ ⊆ CΣ ∞ . Let X ∈ Safety∞ . For all σ ∈ X we have that pref(σ) ⊆ X and hence pref(σ) ⊆ pref↑ (X). If σ is finite then σ ∈ pref↑ (X) otherwise σ ∈ {σ ∈ Σ ω | pref(σ) ⊆ pref↑ (X)}, so σ ∈ LimPrefCl(X). So X ∈ CΣ ∞ . Liveness case. First we prove DΣ ∞ ⊆ Liveness∞ . So let X ∈ DΣ ∞ . From the fact that LimPrefCl(X) = Σ ∞ it follows that pref↑ (X) = Σ ∗ . This implies Σ ∗ ⊆ pref↑ (X) and hence X ∈ Liveness∞ . Now we prove Liveness∞ ⊆ DΣ ∞ . Let X ∈ Liveness∞ . We have Σ ∗ ⊆ pref↑ (X) and hence pref↑ (X) = Σ ∗ . The set {σ ∈ Σ ω | ∀σ 0 ∈ Σ ∗ . (σ 0  σ ⇒ σ 0 ∈ pref↑ (X)} is equal to Σ ω since for every σ ∈ Σ ω and σ 0 ∈ Σ ∗ we have that σ 0 6 σ or σ 0 ∈ pref↑ (X) = Σ ∗ . So LimPrefCl(X) = Σ ∗ ∪ Σ ω = Σ ∞ and hence X ∈ DΣ ∞ t u Hence, exploiting the decomposition theorem (Thm. 1) we have that: ∀P ∈ ℘(Σ ∞ ) . (∃S ∈ Safety∞ , L ∈ Liveness∞ . P = S ∩ L) 1 ∞ lim (X) is the Eilenberg-limit [4] of X, i.e., the set {σ ∈ Σ ω | |pref(σ) ∩ X| = ∞}. 4.2 Hyperproperties def − ℘(℘(Σ ∗ )), defined as SprefCl = λX . spref↑ (X ), Function SprefCl : ℘(℘(Σ ∗ )) → ∗ is a closure on ℘(℘(Σ )) (indeed it is a KCO). So we can define a topology on ℘(Σ ∗ ), where: – C℘(Σ ∗ ) = SprefCl ↑ (℘(℘(Σ ∗ ))) = {X ⊆ ℘(Σ ∗ ) | X = SprefCl(X )} are the closed sets – D℘(Σ ∗ ) = {X ⊆ ℘(Σ ∗ ) | SprefCl(X ) = ℘(Σ ∗ )} are the dense sets Proposition 4. HyperSafety∗ = C℘(Σ ∗ ) and HyperLiveness∗ = D℘(Σ ∗ ) . Proof. Elements X ∈ HyperSafety∗ are prefixset-closed, i.e., X = spref↑ (X ), so HyperSafety∗ is equal to C℘(Σ ∗ ) by definition. As we already noted, ∀X ∈ ℘(Σ ∗ ) ∃X 0 ∈ X . X E X 0 is equivalent to ℘(Σ ∗ ) ⊆ spref↑ (X ). But spref↑ (X ) ⊆ ℘(Σ ∗ ), for all X ∈ ℘(℘(Σ ∗ )). Hence SprefCl(X ) = ℘(Σ ∗ ), i.e., X ∈ D℘(Σ ∗ ) , iff X ∈ HyperLiveness∗ . t u Hence, exploiting the decomposition theorem (Thm. 1) we have that: ∀HP ∈ ℘(℘(Σ ∗ )) . (∃HS ∈ HyperSafety∗ , HL ∈ HyperLiveness∗ . HP = HS ∩ HL) ω Let slim − ℘(℘(Σ ω )) be λX . {Y ∈ ℘(Σ ω ) | ∀Y 0 ∈ ℘(Σ ∗ ) . (Y 0 E : ℘(℘(Σ ω )) → Y ⇒ Y 0 ⊆ spref↑ (X ))} returning the sets of limit sequences of X . The function def ω SlimCl : ℘(℘(Σ ω )) → − ℘(℘(Σ ω )), defined as SlimCl = λX . slim (X ), is a closure on ℘(℘(Σ )) (indeed it is a KCO). So we can define a topology on ℘(Σ ω ), where: ω – C℘(Σ ω ) = SlimCl ↑ (℘(℘(Σ ω ))) = {X ⊆ ℘(Σ ω ) | X = SlimCl(X )} are the closed sets – D℘(Σ ω ) = {X ⊆ ℘(Σ ω ) | SlimCl(X ) = ℘(Σ ω )} are the dense sets Proposition 5. HyperSafetyω = C℘(Σ ω ) and HyperLivenessω = D℘(Σ ω ) . ω Proof. Note that slim (X ) = {Y ∈ ℘(Σ ω ) | spref(Y ) ⊆ spref↑ (X )}. Hypersafety case. First we prove C℘(Σ ω ) ⊆ HyperSafetyω . Let X ∈ C℘(Σ ω ) . For all X ∈ X we have spref(X) ⊆ spref↑ (X ) and hence X ∈ HyperSafetyω . For all X ∈ / X exists Y ∈ ℘(Σ ∗ ) such that Y E X ∧ Y 6⊆ spref↑ (X ), hence spref(X) 6⊆ spref↑ (X ) and so X ∈ / HyperSafetyω . Now we prove HyperSafetyω ⊆ ω C℘(Σ ω ) . Let X ∈ HyperSafety . For all X ∈ X we have spref(X) ⊆ spref↑ (X ) which implies X ⊆ {Y ∈ ℘(Σ ω ) | spref(Y ) ⊆ spref↑ (X )}. For all X ∈ / X we have spref(X) 6⊆ spref↑ (X ) which implies X ∈ / {Y ∈ ℘(Σ ω ) | spref(Y ) ⊆ spref↑ (X )}. Hence X = SlimCl(X ) and so X ∈ C℘(Σ ω ) . Hyperliveness case. First we prove D℘(Σ ω ) ⊆ HyperLivenessω . So let X ∈ D℘(Σ ω ) . From SlimCl(X ) = ℘(Σ ω ) it follows that {Y ∈ ℘(Σ ω ) | spref(Y ) ⊆ spref↑ (X )} is equal to ℘(Σ ω ). This means that spref(Σ ω ) ⊆ spref↑ (X ), which implies that ℘(Σ ∗ ) ⊆ spref↑ (X ). So X ∈ HyperLivenessω . Now we prove HyperLivenessω ⊆ D℘(Σ ω ) . Let X ∈ HyperLivenessω , then ℘(Σ ∗ ) ⊆ spref↑ (X ). This implies that ∀Y ∈ ℘(Σ ω ) we have spref(Y ) ⊆ spref↑ (X ), namely {Y ∈ ℘(Σ ω ) | spref(Y ) ⊆ spref↑ (X )} = ℘(Σ ω ). Hence SlimCl(X ) = ℘(Σ ω ) and X ∈ C℘(Σ ω ) . t u Hence, exploiting the decomposition theorem (Thm. 1) we have that: ∀HP ∈ ℘(℘(Σ ω )) . (∃HS ∈ HyperSafetyω , HL ∈ HyperLivenessω . HP = HS ∩ HL) Let slim : ℘(℘(Σ ∞ )) → − ℘(℘(Σ ∞ )), defined as λX . X ∪ {Y ∈ ℘(Σ ∞ ) | ∀Y 0 ∈ ∞ ∗ 0 0 ω ℘(Σ ) . (Y E Y ⇒ Y ∈ X )}, the version on mixed sequences of slim . Note that here Y is a subset of finite and infinite sequences, not only of the infinite one, so we maintain the power to express mixed sets. The function SlimSprefCl : def ℘(℘(Σ ∞ )) →− ℘(℘(Σ ∞ )), defined as SlimSprefCl = λX . slim ∞ ◦ spref↑ (X ), is a closure on ℘(℘(Σ )) (it is a KCO). We have a topology on ℘(Σ ∞ ), where: ∞ – C℘(Σ ∞ ) = SlimSprefCl ↑ (℘(℘(Σ ∞ ))) = {X ⊆ ℘(Σ ∞ ) | X = SlimSprefCl(X )} are the closed sets – D℘(Σ ∞ ) = {X ⊆ ℘(Σ ∞ ) | SlimSprefCl(X ) = ℘(Σ ∞ )} are the dense sets Proposition 6. HyperSafety∞ = C℘(Σ ∞ ) and HyperLiveness∞ = D℘(Σ ∞ ) . Proof. Note: SlimSprefCl(X ) = spref↑ (X )∪{Y ∈ ℘(Σ ∞ ) | ∀Y 0 ∈ ℘(Σ ∗ ) . (Y 0 E Y ⇒ Y 0 ∈ spref↑ (X )} = {Y ∈ ℘(Σ ∞ ) | spref(Y ) ⊆ spref↑ (X )}, since if X is in spref↑ (X) then all Y E X are in spref↑ (X) too. Hypersafety case. First we prove C℘(Σ ∞ ) ⊆ HyperSafety∞ . Let X ∈ C℘(Σ ∞ ) . For all X ∈ X we have that X ∈ {Y ∈ ℘(Σ ∞ ) | spref(Y ) ⊆ spref↑ (X )} and hence spref(X) ⊆ X . In fact, X ∈ {Y ∈ ℘(Σ ∞ ) | spref(Y ) ⊆ spref↑ (X )} implies spref(X) ⊆ spref↑ (X ) ⊆ X . For all X ∈ / X we have that X ∈/ {Y ∈ ℘(Σ ∞ ) | spref(Y ) ⊆ spref↑ (X )}. This implies that spref(X) 6⊆ spref↑ (X ) = X ∩ ℘(Σ ∗ ), hence spref(X) 6⊆ X . Hence X ∈ HyperSafety∞ . Now we prove HyperSafety∞ ⊆ C℘(Σ ∞ ) . Let X ∈ HyperSafety∞ . For all X ∈ X we have spref(X) ⊆ spref↑ (X ) and so X ∈ SlimSprefCl(X ). For all X ∈ / X we have spref(X) 6⊆ spref↑ (X ) and so X 6∈ SlimSprefCl(X ). Hence X ∈ C℘(Σ ∞ ) . Hyperliveness case. First we prove D℘(Σ ∞ ) ⊆ HyperLiveness∞ . So let X ∈ D℘(Σ ∞ ) . From the fact that SlimSprefCl(X ) = ℘(Σ ∞ ) it follows that spref↑ (X ) = ℘(Σ ∗ ). This implies ℘(Σ ∗ ) ⊆ spref↑ (X ) and hence X ∈ HyperLiveness∞ . Now we prove HyperLiveness∞ ⊆ D℘(Σ ∞ ) . Let X ∈ HyperLiveness∞ . Then we have ℘(Σ ∗ ) ⊆ spref↑ (X ) and hence spref↑ (X ) = ℘(Σ ∗ ). Now we can note that the set {Y ∈ ℘(Σ ∞ ) | ∀Y 0 ∈ ℘(Σ ∗ ) . (Y 0 E Y ⇒ Y 0 ∈ spref↑ (X )} is equal to ℘(Σ ∞ ) since for every Y ∈ ℘(Σ ∞ ) and Y 0 ∈ ℘(Σ ∗ ) we have that Y 0 6E Y or Y 0 ∈ spref↑ (X ) ⊆ ℘(Σ ∗ ). So SlimSprefCl(X ) = ℘(Σ ∞ ) and X ∈ D℘(Σ ∞ ) . t u Hence, exploiting the decomposition theorem (Thm. 1) we have that: ∀HP ∈ ℘(℘(Σ ∞ )) . (∃HS ∈ HyperSafety∞ , HL ∈ HyperLiveness∞ . HP = HS ∩ HL) 5 Conclusions and related works In this work we have investigated the definition of systems properties in a para- metric setting. The first parameter distinguishes if the properties are trace prop- erties or hyperproperties. The first are simpler to check (they can be verified observing single executions) but they lose the power to express policies which specify relations between executions. The second parameter concerns what kind of executions properties are able to express: only finite, only infinite or mixed (finite and infinite). We have analyzed how the well known safety/liveness clas- sification of properties changes in relation with the latter two parameters. Some work in this direction was already done by Roşu [8], but only for the safety part and only for trace properties. The beauty of the safety/liveness classification is its topological interpreta- tion, which allows us to decompose every property in its safety part and its liveness part. This means that we can decompose the verification process in two, more simpler, parts as well. To the best of our knowledge, this topologies were specified only for trace properties on infinite executions [7] and for hyper- properties on infinite executions [3]. Our work gives a topological interpretation also for the others combinations: trace properties on finite and on mixed exe- cutions, hyperproperties on finite and on mixed executions. We proved that in each combinations the safety/hypersafety are the closed sets in the correspond- ing topology and the liveness/hyperliveness are the dense sets. This means that the “decomposition method” can be applied in all six cases, not only in the infinite executions ones. As a future work, it would be interesting to extend our work to the safety/ progress classification [2], which is orthogonal to the safety/liveness but it gives a fine-grained characterization of not-safety properties. References 1. Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 1985. 2. E. Chang, Z. Manna, and A. Pnueli. The safety-progress classification. Technical report, Stanford University, Dept. of Computer Science, 1992. 3. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157–1210, sep 2010. 4. Samuel Eilenberg. Automata, Languages, and Machines. Academic Press, Inc., Orlando, FL, USA, 1974. 5. E. Allen Emerson. Alternative semantics for temporal logics. Theoretical Computer Science, 26(1):121–130, 1983. 6. K. Kuratowski. Topology: Volume I. ZAMM - Journal of Applied Mathematics and Mechanics, 47(8):560–560, 1967. 7. Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag New York, Inc., New York, NY, USA, 1995. 8. Grigore Roşu. On safety properties and their monitoring. Scientific Annals of Computer Science, 22(2):327–365, dec 2012.