Usually, systems properties are de ned in terms of the in nite executions which satisfy it. In this work we explore what happens if we allow nite executions in properties de nitions. In particular, we give a topological interpretation of the safety/liveness classi cation in the domains of: only nite, only in nite 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 classi cation in the three domains.
In the eld of security, with veri cation is intended the general process of checking 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). Veri cation can only gure out whether a system performs not allowed behaviors. When the security mechanism has the power also to a ect the system execution 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 veri cation/enforcing, it is necessary to have a model of the system and a way for formalizing the policy we need to check. Usually, systems are modeled by means of the set of their execution traces, namely histories of states, for a given formalization of systems states, reached during computation. 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 instance a system is deadlock free if each execution is deadlock free. Unfortunately not all policies fall in this category (e.g., information ows), hence hyperproperties [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 ow when we can detect a ow only by comparing di erent 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 in nite sequences of states. This is justi ed by the fact that systems are supposed to potentially run forever, and by the fact that a terminating computation can be represented as an in nite one repeating the last state in nitely many times.
The veri cation/enforcing of trace properties over in nite sequences is well founded and it has a strong background, theoretical and practical. In particular it relies on the well known classi cation of trace properties: safety and liveness. Informally, the rst model the fact that \nothing bad will happen" and the second model the fact that \something good will eventually happen". Despite its simplicity, this classi cation allows us to describe, by using topological arguments, 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 su cient 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 counterparts 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 nite executions in properties de nitions, namely if we take in consideration also the cases where histories are only nite sequences, only in nite sequences and mixed sequences ( nite and in nite). We noted, for example, that the notion of \safety" is slightly di erent in these three cases. For doing so we propose a topological interpretation to the safety/liveness classi cation, parametric on the type of admitted histories. Furthermore, we extend this reasoning to hyperproperties, giving a topological interpretation also to the hypersafety/hyperliveness classi cation. 2
Given an alphabet (a set of symbols) , we denote with n the set of sequences of symbols in of length n 2 N and with the empty sequence. Then + =def S n is the set of non-empty nite sequences, !+ is the set of non-empty 1+ =def + n>0 in nite sequences and [ !+ is the set of all non-empty sequences. We write , ! and 1 to indicate the nite ?+ [ f g, in nite !+ [ f g and all 1+ [ f g sequences, respectively.
The concatenation of sequences 2 and 0 2 1 is the sequence 0 2 1. Sequence 2 is a pre x of 00 2 1, in symbols 00, if exists 0 2 1 such that 0 = 00. When we deal with sets of sequences, we can extend the de nition of pre x to sets as follows. A set of sequences X is a pre xset of Y 1, in symbols X E Y , if for all 2 X exists 0 2 Y such that 0 [3]. A set of in nite sequences f 0; 1; : : : g converges to the limit sequence if the length of the maximal pre x common to each k and to goes to in nity as k goes to in nity [2]. For example, fanb! j n 0g converges to a!, in fact the sequence of longest pre xes common to a! and to k = akb! (i.e., ak) gets increasingly longer with k.
Given a set X, we denote with jXj 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 and Y X, we denote with f [Y ] =def ff (x) j x 2 Y g the direct image of f on Y { the closure of Y , written (Y ), is the smallest closed set containing Y , i.e., (Y ) = [fO 2 OX j O (Y ) = \fC 2 CX j Y
Y g Cg and with f " =def Y : Sff (x) j x 2 Y g the image-lift to sets of f . In the following, 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.
A topology over a set X consists in a family of subsets of X which de nes its open sets. OX }(X) is a family of open sets i it is closed under union (i.e., 8Y OX : S Y 2 OX ), it is closed under binary intersection (i.e., Y1; Y2 2 OX ) Y1 \ Y2 2 OX ) and it includes X (i.e., S OX = X). The dual of an open set is a closed set, so a family of open sets de nes automatically a family of closed sets, namely CX = fX n O j O 2 OX g. Given Y X:
{ the interior of Y , written (Y ), is the largest open set contained in Y , i.e., A set D X is said dense i (D) = X, so in a topology there is also a family of dense sets, i.e., DX = fD X j (D) = Xg. Every element of }(X) can be speci ed 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). 8Y 2 }(X) (9C 2 CX ; D 2 DX : Y = C \ D). Proof. Y = (Y ) \ Y = ( (Y ) \ Y ) [ ? = ( (Y ) \ Y ) [ ( (Y ) \ (X n (Y ))) = (Y ) \ (Y [ (X n (Y ))). But (Y ) 2 CX and Y [ (X n (Y )) 2 DX . In fact (Y [ (X n (Y ))) (Y ) [ (X n (Y )) (Y ) [ (X n (Y )) = X. tu A function : }(X) ! }(X) is a Kuratowski Closure Operator (KCO) i all the following hold: (Y1) (Y2)] A KCO over }(X) induces a topology on X where the KCO is the closure of X [6]. So, in order to de ne a topology on X, it is su cient to specify its closed sets, namely a closure (or a KCO) over }(X). 2.1
If systems are modeled with execution traces, the evolution of a system is described in terms of some objects & 2 , 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 hyperproperty [3], is a set of sets of sequences or, equivalently, a set of trace properties. A set of sequences X satis es a property P i X P . A set of sequences X satis es an hyperproperty HP i X 2 HP. The trace property ?, or false, is the one which cannot be satis ed, 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 satis ed by every system, i.e., 8X : X true. Analogously, we can de ne falseh and trueh for hyperproperties as ffalseg 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 noninterference. In this latter case it is necessary to specify it as an hyperproperty. Intuitively, a property is de ned exclusively in terms of individual executions and, in general, do not specify a relation between di erent executions of the system. Instead, an hyperproperty speci es 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 su cient to consider hyperproperties. This means that hyperproperties are able to de ne every possible security policy (for systems modeled as set of states sequences).
It is worth noting that in order to disprove whether a system ful lls a trace property it is necessary to show one trace, which is the counterexample. Analogously, in order to disprove that a system ful lls 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 rst 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 nite amount of time. Due to this fact, safety properties are identi ed 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 in nite, amount of time.
Finite executions can be seen as particular cases of in nite ones: we can repeat in nitely many times the nal state of a nite execution in order to obtain an in nite execution equivalent to the nite one. This has led researchers to model system executions and trace properties as set of in nite 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 in nite sequences (like linear temporal logics and Buchi 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 in nite 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 nite traces can be easily expressed as in nite
sequences, in practice we deal with systems which exhibit nite behaviors. So it
is natural to wonder what happens if we allow nite sequences in properties
de nition. 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 nite }( ), only in nite }( !) and mixed }(
Let us start with safety rst and denote by Safety , Safety! and Safety1 the
safety properties over nite, in nite and mixed executions, respectively. In [1],
Alpern and Schneider de ne safety properties S on }( !) in a refutational way:
if 2= S then there is a nite sequence 0 such that 0 00 2= S for every
00 2 !. This means that, if an in nite execution violates the property, then
the bad thing must have been occurred in one of its nite pre xes and the
violation cannot ever be recovered in the future. An alternative, and equivalent,
de nition due to Rosu [8] is the following: for a safety property S 2 }( !),
2 S i pref( ) pref"(S), where pref : 1 ! }( ) is the function
: f 0 j 9 00 2 1 : 0 00 = g returning the set of pre xes of a given sequence.
Furthermore, Rosu in [8] discusses the known de nitions of safety properties over
nite, in nite and mixed executions, and their equivalence with the following:
{ Safety =def fS 2 }( ) j S = pref"(S)g
{ Safety! =def fS 2 }( !) j 2 S , pref( )
{ Safety1 =def fS 2 }(
Sg Although safety properties essentially capture the fact that, in order to disprove the property, it is su cient to show a nite counterexample, the de nitions of safety on nite, in nite and mixed sequences are di erent. For nite sequences it is su cient the pre x-closure, namely a safety on must contain all the pre xes of its sequences. The same de nition cannot be applied to !, indeed none of its pre xes 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 in nite sequences which approximate the pre xes. Finally, as expected, the safety on 1 combine both aspects of nite and in nite sequences. 3.2
To the best of our knowledge, there are no works reasoning about liveness properties over nite and mixed executions. One can think that it is not meaningful to de ne liveness on nite 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 nite sequences only, as the set . So, let us denote with Liveness , Liveness! and Liveness1 the liveness properties over nite, in nite and mixed executions, respectively. The original de nition of Alpern and Schneider [1] involves in nite sequences only, and it states that a property L 2 }( !) is a liveness property i for every nite sequence 2 there exists an in nite sequence 0 2 ! such that 0 is in L. This means that every nite execution can be extended to an in nite one satisfying the property. We believe that this intuition can be easily adapted to nite and mixed sequences as well. De nition 1. Given y 2 f ; !; 1g:
Livenessy =def fL 2 }( y) j 8 2 9 0 2 L : 0g Liveness properties capture the fact that in order to disprove the property is necessary to show an in nite counterexample. It is worth noting that our de nition of liveness on in nite executions is indeed equivalent to the one of Alpern and Schneider. Moreover, 8 2 9 0 2 L : 0 is equivalent to pref"(L).
Finally, we can note that, as usual, the trace property false is a safety
property for }( ), }( !) and }(
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 in nite executions only. In this section, we mimic what we have done for properties in the hyper case.
Let us denote by HyperSafety , HyperSafety! and HyperSafety1 the safety
hyperproperties over nite, in nite and mixed executions, respectively. In [3]
the authors de ne hypersafety in a refutational way: if X 2= HS then there is
a nite set of nite sequences O E X such that every possible X0 2 }( !)
which extends O (i.e., O E X0) 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 de ne
hypersafety for nite, in nite and mixed executions, lifting to sets the de nitions
of safety, where spref : }(
{ HyperSafety =def fHS 2 }(}( )) j HS = spref"(HS)g
{ HyperSafety! =def fHS 2 }(}( !)) j X 2 HS , spref(X)
{ HyperSafety1 =def fHS 2 }(}(
HSg Hypersafety essentially capture the fact that, in order to disprove the property, it is su cient to show a counterexample-set of nite traces. Hence, also in the hyper level, we have the link between safety properties and the concept of monitorability. 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 in nite) 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 nite number of) elements.
In order to characterize hypersafety for nite sequences, it is su cient the pre xset-closure, namely an hypersafety on must contain all the pre xsets of its sequences. The same de nition cannot be applied to !, indeed none of its pre xsets 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 in nite sequences which approximate the pre xsets. Finally, as expected, the hypersafety on 1 combine both aspects of nite and in nite sequences. Furthermore, it is worth noting that our de nition of hypersafety on in nite executions is indeed equivalent to the one of Clarkson and Schneider, if we constrain spref to collect only nite pre xsets. 3.4
Let us now denote by HyperLiveness , HyperLiveness! and HyperLiveness1 the liveness hyperproperties over nite, in nite and mixed executions, respectively. In [3], the original de nition states that an hyperproperty HL 2 }(}( !)) is hyperliveness i for every nite set of nite sequences O 2 }( ) it exists a set of in nite sequences X 2 }( !), which extends O (i.e., O E X), such that X is in HL. Also in this case, the de nition is basically the concept of liveness lifted to sets. Here we give an alternative de nition, which turns out to be parameterizable on nite, in nite and mixed executions, has it happens for properties case. As we have done for hypersafety, in our de nitions we relax the constraint that the observable O needs to be a nite set.
De nition 2. Given y 2 f ; !; 1g:
HyperLivenessy = fHL 2 }(}( y)) j 8O 2 }( ) 9X 2 HL : O E Xg Hyperliveness captures the fact that, in order to disprove the property, it is necessary to show a set of in nite counterexamples. It is worth noting that our de nition of hyperliveness on in nite executions is indeed equivalent to the one of Clarkson and Schneider if we constrain every O to be nite. Furthermore, the condition 8O 2 }( ) 9X 2 HL : O E X is equivalent to: }( ) spref"(HL).
Finally, we can note that, as expected, the hyperproperty falseh is
hypersafety for }(}( )), }(}( !)) and }(}(
When dealing with in nite 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 nite and mixed computations other than in nite ones. For doing so, we de ne a KCO for each domain ( nite, in nite, mixed for properties and nite, in nite, 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
The function PrefCl : }( ) ! }( ), de ned as PrefCl =def X : pref"(X), is a closure on }( ) (indeed it is a KCO). So we have a topology on , where: { C { D = PrefCl"(}( )) = fX = fX j PrefCl(X) = j X = PrefCl(X)g are the closed sets g are the dense sets Proposition 1. Safety = C
and Liveness = D .
Proof. Since elements X 2 Safety are pre x-closed, i.e., X = pref"(X), Safety is equal to C by de nition. As we already noted, 8 2 9 0 2 X : is equivalent to pref"(X). But pref"(X) , for every X 2 }( Hence PrefCl(X) = , i.e., X 2 D , i X 2 Liveness . Hence, exploiting the decomposition theorem (Thm. 1) we have that: 8P 2 }( ) : (9S 2 Safety ; L 2 Liveness : P = S \ L) Let li!m : }( !) ! }( !) the function X : f 2 ! j 8 0 2 : ( 0 ) 0 2 pref"(X))g returning the set of limit sequences of X. The function LimCl : }( !) ! }( !), de ned as LimCl =def X : li!m(X), is a closure on }( !) (indeed it is a KCO). So we have a topology on !, where: { C ! = LimCl"(}( !)) = fX { D ! = fX ! j LimCl(X) = ! j X = LimCl(X)g are the closed sets !g are the dense sets Proposition 2. Safety! = C ! and Liveness! = D ! .
Proof. Our de nitions 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 de nition of safety and liveness properties over !. tu
Hence, exploiting the decomposition theorem (Thm. 1) we have that:
8P 2 }( !) : (9S 2 Safety!; L 2 Liveness! : P = S \ L)
Let li1m : }(
are the closed sets { D 1 = fX 1 j LimPrefCl(X) = 1 j X = LimPrefCl(X)g
Proposition 3. Safety1 = C 1 and Liveness1 = D 1 . Proof. Note that LimPrefCl(X) = pref"(X) [ f 2 0 2 pref"(X)g = pref"(X) [ f 2 ! j pref( ) ! j 8 0 2 pref"(X)g.
: ( 0 ) Safety case. First we prove C 1 have that 2 pref"(X) or 2 f 2 cases, imply pref( ) X. In fact:
! j pref( ) pref"(X)g and, both 2 pref"(X) ) pref( ) 2 f 2 ! j pref( ) pref"(X)
X pref"(X)g ) pref( ) pref"(X)
X For all 2= X we have that 2= pref"(X) and 2= f 2 ! j pref( ) pref"(X)g. If is nite then 2= pref"(X) implies pref( ) 6 pref"(X), since 2 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 2 Safety1. Now we prove Safety1 C 1 . Let X 2 Safety1. For all 2 X we have that pref( ) X and hence pref( ) pref"(X). If is nite then 2 pref"(X) otherwise 2 f 2 ! j pref( ) pref"(X)g, so 2 LimPrefCl(X). So X 2 C 1 .
Liveness case. First we prove D 1 Liveness1. So let X 2 D 1 . From the
fact that LimPrefCl(X) = 1 it follows that pref"(X) = . This implies
pref"(X) and hence X 2 Liveness1. Now we prove Liveness1 D 1 .
Let X 2 Liveness1. We have pref"(X) and hence pref"(X) = . The
set f 2 ! j 8 0 2 : ( 0 ) 0 2 pref"(X)g is equal to ! since for
every 2 ! and 0 2 we have that 0 6 or 0 2 pref"(X) = . So
LimPrefCl(X) = ! = 1 and hence X 2 D 1 tu
[
Hence, exploiting the decomposition theorem (Thm. 1) we have that:
1 li1m (X) is the Eilenberg-limit [4] of X, i.e., the set f 2
8P 2 }(
are the closed sets { D}( ) = fX }( ))) = fX }(
) j X = SprefCl(X )g ) j SprefCl(X ) = }( )g are the dense sets Proposition 4. HyperSafety = C}( ) and HyperLiveness = D}( ). Proof. Elements X 2 HyperSafety are pre xset-closed, i.e., X = spref"(X ), so HyperSafety is equal to C}( ) by de nition. As we already noted, 8X 2 }( ) 9X0 2 X : X E X0 is equivalent to }( ) spref"(X ). But spref"(X ) }( ), for all X 2 }(}( )). Hence SprefCl(X ) = }( ), i.e., X 2 D}( ), i X 2 HyperLiveness . tu Hence, exploiting the decomposition theorem (Thm. 1) we have that: 8HP 2 }(}( )) : (9HS 2 HyperSafety ; HL 2 HyperLiveness : HP = HS \ HL) Let sli!m : }(}( !)) ! }(}( !)) be X : fY 2 }( !) j 8Y 0 2 }( ) : (Y 0 E Y ) Y 0 spref"(X ))g returning the sets of limit sequences of X . The function SlimCl : }(}( !)) ! }(}( !)), de ned as SlimCl =def X : sli!m(X ), is a closure on }(}( !)) (indeed it is a KCO). So we can de ne a topology on }( !), where: { C}( !) = SlimCl"(}(}( !))) = fX }( !) j X = SlimCl(X )g are the closed sets { D}( !) = fX }( !) j SlimCl(X ) = }( !)g are the dense sets Proposition 5. HyperSafety! = C}( !) and HyperLiveness! = D}( !). Proof. Note that sli!m(X ) = fY 2 }( !) j spref(Y ) spref"(X )g.
Hypersafety case. First we prove C}( !) HyperSafety!. Let X 2 C}( !). For all X 2 X we have spref(X) spref"(X ) and hence X 2 HyperSafety!. For all X 2= X exists Y 2 }( ) such that Y E X ^ Y 6 spref"(X ), hence spref(X) 6 spref"(X ) and so X 2= HyperSafety!. Now we prove HyperSafety! C}( !). Let X 2 HyperSafety!. For all X 2 X we have spref(X) spref"(X ) which implies X fY 2 }( !) j spref(Y ) spref"(X )g. For all X 2= X we have spref(X) 6 spref"(X ) which implies X 2= fY 2 }( !) j spref(Y ) spref"(X )g. Hence X = SlimCl(X ) and so X 2 C}( !).
Hyperliveness case. First we prove D}( !) HyperLiveness!. So let X 2 D}( !).
From SlimCl(X ) = }( !) it follows that fY 2 }( !) j spref(Y ) spref"(X )g
is equal to }( !). This means that spref( !) spref"(X ), which implies that
}( ) spref"(X ). So X 2 HyperLiveness!. Now we prove HyperLiveness!
D}( !). Let X 2 HyperLiveness!, then }( ) spref"(X ). This implies that
8Y 2 }( !) we have spref(Y ) spref"(X ), namely fY 2 }( !) j spref(Y )
spref"(X )g = }( !). Hence SlimCl(X ) = }( !) and X 2 C}( !). tu
8HP 2 }(}( !)) : (9HS 2 HyperSafety!; HL 2 HyperLiveness! : HP = HS \ HL)
Let sli1m : }(}(
are the closed sets
{ D}(
Hypersafety case. First we prove C}(
In this work we have investigated the de nition of systems properties in a parametric setting. The rst parameter distinguishes if the properties are trace properties or hyperproperties. The rst are simpler to check (they can be veri ed 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 nite, only in nite or mixed ( nite and in nite). We have analyzed how the well known safety/liveness classi cation of properties changes in relation with the latter two parameters. Some work in this direction was already done by Rosu [8], but only for the safety part and only for trace properties.
The beauty of the safety/liveness classi cation is its topological interpretation, which allows us to decompose every property in its safety part and its liveness part. This means that we can decompose the veri cation process in two, more simpler, parts as well. To the best of our knowledge, this topologies were speci ed only for trace properties on in nite executions [7] and for hyperproperties on in nite executions [3]. Our work gives a topological interpretation also for the others combinations: trace properties on nite and on mixed executions, hyperproperties on nite and on mixed executions. We proved that in each combinations the safety/hypersafety are the closed sets in the corresponding 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 in nite executions ones.
As a future work, it would be interesting to extend our work to the safety/ progress classi cation [2], which is orthogonal to the safety/liveness but it gives a ne-grained characterization of not-safety properties.