my forest
adding many ltp notes
+271
-18
+31
-11
trees/ltp/ltp-0001.tree
+31
-11
trees/ltp/ltp-0001.tree
···
1
1
\taxon{Research Notebook}
2
-
\title{Linear-time Temporal Properties}
2
+
\title{Linear-time temporal properties}
3
3
\author{liamoc}
4
4
\transclude{ltp-0002}
5
5
\transclude{ltp-0003}
6
+
\subtree{
7
+
\title{Concerning safety properties}
6
8
\transclude{ltp-0004}
9
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000B}}
10
+
\transclude{ltp-000A}
11
+
\transclude{ltp-0009}
12
+
\transclude{ltp-000E}
13
+
\transclude{ltp-0008}
14
+
}
15
+
\subtree{
16
+
\title{Concerning guarantee properties}
7
17
\transclude{ltp-0005}
8
-
\p{The [famous paper](alpern-schneider-1985) of [[alpern]] and [[schneider]] defines a topology where the closed sets are safety properties, and the open sets are the guarantee properties. The closure operator #{\overline{X}} therefore gives the smallest safety property #{\supseteq X}, and the interior operator #{\underline{X}} gives the largest guarantee property #{\subseteq X}. }
9
-
\p{This space is a metric space, using the standard prefix-agreement metric that one might use for a Baire or Cantor space: }
10
-
##{
11
-
\begin{array}{l}
12
-
d : \Sigma^\omega \times \Sigma^\omega \rightarrow \mathbb{R} \\
13
-
d(\sigma,\rho) = 2^{-\sup\{ i \mid \sigma_{0\dots{}i} = \rho_{0\dots{}i}\}} \\
14
-
\\
15
-
\qquad\text{where}\ 2^{-\infty} = 0
16
-
\end{array}}
17
-
\p{[[alpern]] and [[schneider]] then go on to prove that all properties are the intersection of \em{safety} and \em{liveness} (i.e. \em{dense} sets, #{\overline{X} = \Sigma^\omega})}
18
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000D}}
19
+
\transclude{ltp-000C}
20
+
\transclude{ltp-000G}
21
+
\transclude{ltp-000H}
22
+
\transclude{ltp-000F}
23
+
}
24
+
\subtree{
25
+
\title{Properties as a topological space}
26
+
\scope{\put\transclude/metadata{true}\transclude{ltp-0007}}
27
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000I}}
28
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000J}}
29
+
\transclude{ltp-000M}
30
+
}
31
+
\subtree{
32
+
\title{Concerning liveness properties}
33
+
\transclude{ltp-0006}
34
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000K}}
35
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000L}}
36
+
% closure properties go here?
37
+
}
+4
-2
trees/ltp/ltp-0002.tree
+4
-2
trees/ltp/ltp-0002.tree
···
1
1
\taxon{Definition}
2
-
\title{The space #{\Sigma^\omega}}
2
+
\import{ltp-macros}
3
+
\title{Traces and behaviours}
3
4
\author{liamoc}
4
-
\p{Let the set of all possible \em{states} be #{\Sigma}. Then, the set of all possible \em{behaviours} —infinite sequences of states — is #{\Sigma^\omega}. Note that we do not require that #{\Sigma} is finite.}
5
+
\p{Let the set of all possible \em{states} be #{\Sigma}. Note that we do not require that #{\Sigma} is finite. Then, #{\ftraces} is the set of finite sequences of states. We denote the empty sequence as #{\varepsilon}. The concatenation of two sequences #{t} and #{u} is written #{tu}. }
6
+
\p{The set of all \em{behaviours} — \em{infinite} sequences of states — is #{\itraces}. We define #{\sigma{}t = \sigma} when the sequence #{\sigma} is infinite. }
5
7
\p{We shall model terminating systems, which have finite behaviours, as behaviours that infinitely repeat their final state.}
+2
-1
trees/ltp/ltp-0003.tree
+2
-1
trees/ltp/ltp-0003.tree
···
1
1
\title{Properties}
2
2
\taxon{Definition}
3
+
\import{ltp-macros}
3
4
\author{liamoc}
4
-
\p{A property, being a specification of a system, can be thought of as simply a set of behaviours, i.e. a subset of [the space #{\Sigma^\omega}](ltp-0002). A property is \em{satisfied} by a system if all behaviours exhibited by the system are contained within the set. It is \em{violated} by a system if there exists a behaviour exhibited by the system that is not contained within the set. }
5
+
\p{A property, being a specification of a system, can be thought of as simply a set of behaviours, i.e. a subset of [the space #{\itraces{}}](ltp-0002). A property is \em{satisfied} by a system if all behaviours exhibited by the system are contained within the set. It is \em{violated} by a system if there exists a behaviour exhibited by the system that is not contained within the set. }
+1
-1
trees/ltp/ltp-0004.tree
+1
-1
trees/ltp/ltp-0004.tree
···
1
1
\taxon{Definition}
2
2
\author{liamoc}
3
-
\title{Safety Properties}
3
+
\title{Safety properties}
4
4
\p{A \em{safety} [property](ltp-0003) says that a bad thing does not happen. The "bad thing" in this case is some finite, observable event. In other words, safety properties are those [properties](ltp-0003) whose \em{violation} can be established by examining only a \em{finite} prefix of the behaviour.}
5
5
\p{For example, the safety property "The state #{\mathtt{a}} is never reached" is violated by any finite prefix containing the state #{\mathtt{a}}.}
+5
-3
trees/ltp/ltp-0005.tree
+5
-3
trees/ltp/ltp-0005.tree
···
1
+
\import{ltp-macros}
1
2
\taxon{Definition}
2
3
\author{liamoc}
3
-
\title{Guarantee Properties}
4
-
\p{A \em{guarantee} [property](ltp-0003) is the complement of a [safety property](ltp-0004). A guarantee property says that a good thing happens eventually. As with safety properties, the "good thing" is some finite, observable event. In other words, guarantee properties are those [properties](ltp-0003) whose \em{satisfaction} can be established by examining only a \em{finite} prefix of the behaviour.}
5
-
\p{For example, the guarantee property "The state #{\mathtt{a}} is eventually reached" is satisfied by any finite prefix containing the state #{\mathtt{a}}.}
4
+
\title{Guarantee properties}
5
+
\p{A \em{guarantee} (or \em{cosafety}) [property](ltp-0003) is the complement of a [safety property](ltp-0004). A guarantee property says that a good thing happens eventually. As with safety properties, the "good thing" is some finite, observable event. In other words, guarantee properties are those [properties](ltp-0003) whose \em{satisfaction} can be established by examining only a \em{finite} prefix of the behaviour.}
6
+
\p{For example, the guarantee property "The state #{\mathtt{a}} is eventually reached" is satisfied by any finite prefix containing the state #{\mathtt{a}}.}
7
+
\p{[[lamport]] [originally called](lamport-1977) these \em{liveness} properties, but we use [the more popular definition](ltp-0006) of that term from [Alpern and Schneider](alpern-schneider-1985). }
+6
trees/ltp/ltp-0006.tree
+6
trees/ltp/ltp-0006.tree
···
1
+
\taxon{Definition}
2
+
\import{ltp-macros}
3
+
\author{liamoc}
4
+
\title{Liveness properties}
5
+
\p{A \em{liveness} [property](ltp-0003) says that a good thing happens eventually, but unlike [guarantee properties](ltp-0005), the "good thing" need not be some finite, observable event. Rather, liveness properties are those [properties](ltp-0003) whose violation \em{cannot} be established by examining only a \em{finite} prefix of the behaviour. In other words, #{P} is a liveness property iff for any finite prefix #{t \in \ftraces}, there exists an infinite extension #{\sigma \in \itraces} such that #{t\sigma} is in the property #{P}.}
6
+
\p{For example, the property "Every #{\mathtt{r}}equest state is eventually followed by an #{\mathtt{a}}nswer state" is a liveness property: No matter how many unanswered #{\mathtt{r}}equests are in a finite prefix, we could always see the #{\mathtt{a}}nswer in the future. }
+5
trees/ltp/ltp-0007.tree
+5
trees/ltp/ltp-0007.tree
···
1
+
\taxon{Construction}
2
+
\import{ltp-macros}
3
+
\meta{source}{(from [[alpern-schneider-1985]])}
4
+
\title{Behaviours as topology}
5
+
\p{The [space #{\itraces{}}](ltp-0002) forms a topology where [safety properties](ltp-0004) are the closed sets and [guarantee properties](ltp-0005) are the open sets. This follows from \ref{ltp-000C}, \ref{ltp-000G}, and \ref{ltp-000F} (or, equivalently, from \ref{ltp-000A}, \ref{ltp-0009} and \ref{ltp-0008}).}
+7
trees/ltp/ltp-0008.tree
+7
trees/ltp/ltp-0008.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Safety properties are closed under intersection}
6
+
\p{For a (possibly infinite) collection of properties #{P_{i \in I}}, if every #{P_i} is a [safety property](ltp-0004) then #{\bigcap_{i \in I} P_i} is a [safety property](ltp-0004). }
7
+
\proofblock{ Let #{ P_{i \in I}} be a (possibly infinite) family of [safety properties](ltp-0004) and let #{P = \bigcap_{i \in I} P_i}. Take any behaviour #{\sigma \notin P}. Then there exists some #{j \in I} such that #{\sigma \notin P_j}. Since #{P_j} is a [safety property](ltp-0004), there is a finite prefix #{u} of #{\sigma} such that no extension of #{u} lies in #{P_j}. But then no extension of #{u} can lie in #{\bigcap_{i \in I} P_i}, because membership in the intersection requires membership in #{P_j}, which is already ruled out. Hence #{u} is a [bad prefix](ltp-000B) for #{P}, so #{P} is a [safety property](ltp-0004).}
+10
trees/ltp/ltp-0009.tree
+10
trees/ltp/ltp-0009.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Safety properties are closed under finite union}
6
+
\p{The union of any two [safety properties](ltp-0004) is a [safety property](ltp-0004). }
7
+
\proofblock{
8
+
\p{Let #{P} and #{Q} be [safety properties](ltp-0004). Take any violating behaviour #{\sigma \notin P \cup Q}. Then, #{\sigma \notin P} and #{\sigma \notin Q}. Since #{P} and #{Q} are safety properties, there exist finite prefixes #{t} and #{u} of #{\sigma} such that no extension of #{t} is in #{P} and no extension of #{u} is in #{Q}. Let #{v} be the longer of #{t} and #{u}; then #{v} is still a prefix of #{\sigma}. Any extension of #{v} is also an extension of both [bad prefixes](ltp-000B) #{t} and #{u}, so it is in neither in #{P} nor #{Q}, and hence not in #{P \cup Q}. Thus the violation of #{P} can be established just by examining the [bad prefix](ltp-000B) #{v}, so #{P \cup Q} is a [safety property](ltp-0004).
9
+
}
10
+
}
+11
trees/ltp/ltp-000A.tree
+11
trees/ltp/ltp-000A.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Trivial properties are safety properties}
6
+
\p{The empty property #{\emptyset} and the [property](ltp-0003) #{\itraces} are both [safety properties](ltp-0004).}
7
+
\proofblock{
8
+
\p{The property #{\itraces} has no violating [behaviours](ltp-0002), so vacuously all violations can be established by finite prefixes.}
9
+
\p{For the property #{\emptyset}, all [behaviours](ltp-0002) are violating, so the empty prefix #{\varepsilon} is a [bad prefix](ltp-000B).
10
+
}
11
+
}
+8
trees/ltp/ltp-000B.tree
+8
trees/ltp/ltp-000B.tree
···
1
+
\taxon{Definition}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\meta{source}{(from [[kupferman-vardi-2001]])}
5
+
\title{Bad prefixes}
6
+
\p{For a [property](ltp-0003) #{P}, the \em{bad prefixes} of #{P} are those finite prefixes #{t \in \ftraces} from which the violation of #{P} can be established, i.e. #{\forall \sigma \in \itraces.\ t\sigma \notin P}.}
7
+
\p{A [property](ltp-0003) #{P} is a [safety property](ltp-0004) iff all violating [behaviours](ltp-0002) are extensions of bad prefixes.
8
+
}
+9
trees/ltp/ltp-000C.tree
+9
trees/ltp/ltp-000C.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Trivial properties are guarantee properties}
6
+
\p{The empty property #{\emptyset} and the [property](ltp-0003) #{\itraces} are both [guarantee properties](ltp-0005).}
7
+
\proofblock{
8
+
\p{Follows from \ref{ltp-000A} as the complement of any [safety property](ltp-0004) is a [guarantee property](ltp-0005).}
9
+
}
+8
trees/ltp/ltp-000D.tree
+8
trees/ltp/ltp-000D.tree
···
1
+
\taxon{Definition}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\meta{source}{(from [[kupferman-vardi-2001]])}
5
+
\title{Good prefixes}
6
+
\p{For a [property](ltp-0003) #{P}, the \em{good prefixes} of #{P} are those finite prefixes #{t \in \ftraces} from which the satisfaction of #{P} can be established, i.e. #{\forall \sigma \in \itraces.\ t\sigma \in P}.}
7
+
\p{A [property](ltp-0003) #{P} is a [guarantee property](ltp-0005) iff all satisfying [behaviours](ltp-0002) are extensions of good prefixes.
8
+
}
+6
trees/ltp/ltp-000E.tree
+6
trees/ltp/ltp-000E.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Safety properties are not closed under infinite union}
6
+
\p{Consider the family of properties #{P_{i \in \mathbb{N}} = \{ \sigma \in \itraces \mid \sigma_i = \texttt{a}\}}, i.e. the property where the #{i}th state is #{\texttt{a}}. Each #{P_i} is a [safety property](ltp-0004), as all violating behaviours are extensions of [bad prefixes](ltp-000B) of length #{i}. Their union #{\bigcup_{i \in \mathbb{N}} P_i}, however, is not a [safety property](ltp-0004), as any finite prefix can be extended to a [good prefix](ltp-000D) by appending an #{\texttt{a}}-state, and therefore cannot be a [bad prefix](ltp-000D). }
+7
trees/ltp/ltp-000F.tree
+7
trees/ltp/ltp-000F.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Guarantee properties are closed under union}
6
+
\p{For a (possibly infinite) collection of properties #{P_{i \in I}}, if every #{P_i} is a [guarantee property](ltp-0005) then #{\bigcup_{i \in I} P_i} is a [guarantee property](ltp-0005). }
7
+
\proofblock{ \p{Let #{ P_{i \in I}} be a (possibly infinite) family of [guarantee properties](ltp-0005). Then each #{\compl{P_i}} is a [safety property](ltp-0004) and therefore #{\bigcap_{i \in I} \compl{P_i}} is a [safety property](ltp-0004) by \ref{ltp-0008}. Its complement #{\compl{(\bigcap_{i \in I} \compl{P_i})} = \bigcup_{i \in I} P_i} is therefore a [guarantee property](ltp-0005).}}
+10
trees/ltp/ltp-000G.tree
+10
trees/ltp/ltp-000G.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Guarantee properties are closed under finite intersection}
6
+
\p{The intersection of any two [guarantee properties](ltp-0005) is a [guarantee property](ltp-0005). }
7
+
\proofblock{
8
+
\p{Let #{P} and #{Q} be [guarantee properties](ltp-0005). Then #{\compl{P}} and #{\compl{Q}} are [safety properties](ltp-0004). By \ref{ltp-0009} their union #{\compl{P} \cup \compl{Q}} is a [safety property](ltp-0004) and thus its complement #{\compl{(\compl{P} \cup \compl{Q})} = P \cap Q} is a [guarantee property](ltp-0005).
9
+
}
10
+
}
+6
trees/ltp/ltp-000H.tree
+6
trees/ltp/ltp-000H.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{Guarantee properties are not closed under infinite intersection}
6
+
\p{Consider the family of properties #{P_{i \in \mathbb{N}} = \{ \sigma \in \itraces \mid \sigma_i \neq \texttt{a}\}}, i.e. the property where the #{i}th state is not #{\texttt{a}}. Each #{P_i} is a [guarantee property](ltp-0005), as all satisfying behaviours are extensions of [good prefixes](ltp-000D) ending in a non-#{\mathtt{a}} state of length #{i}. Their intersection #{\bigcap_{i \in \mathbb{N}} P_i}, however, is not a [guarantee property](ltp-0005), as any finite prefix can be extended to a [bad prefix](ltp-000B) by appending an #{\texttt{a}}-state, and therefore cannot be a [good prefix](ltp-000D). }
+9
trees/ltp/ltp-000I.tree
+9
trees/ltp/ltp-000I.tree
···
1
+
\taxon{Definition}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Guarantee kernel}
5
+
\meta{source}{(from [[amjad-vanglabbeek-oconnor-2026]])}
6
+
\p{Given a [property](ltp-0003) #{P \subseteq \itraces}, the \em{guarantee kernel} of #{P}, written #{\gk{P}}, is the largest subset of #{P} which is a [guarantee property](ltp-0005). That is, #{\gk{P}} is the set of all infinite extensions of the [good prefixes](ltp-000D) of #{P}. }
7
+
\p{It follows that #{P} is a [guarantee property](ltp-0005) iff #{\gk{P} = P}.}
8
+
\p{This is a kernel operator, so it is co-extensive (#{\gk{P} \subseteq P}), idempotent (#{\gk{\gk{P}} = \gk{P}}), and monotonic (#{P \subseteq R} implies #{\gk{P} \subseteq \gk{R}}). }
9
+
\p{[Topologically speaking](ltp-0007), the guarantee kernel is the \em{interior operator}.}
+9
trees/ltp/ltp-000J.tree
+9
trees/ltp/ltp-000J.tree
···
1
+
\taxon{Definition}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Safety closure}
5
+
\meta{source}{(from [[alpern-schneider-1985]])}
6
+
\p{Given a [property](ltp-0003) #{P \subseteq \itraces}, the \em{safety closure} of #{P}, written #{\sc{P}}, is the smallest superset of #{P} which is a [safety property](ltp-0004). It is the dual of the [guarantee kernel](ltp-000I), so #{\gk{\compl{P}} = \compl{\sc{P}}}. This means that the safety closure of #{P} contains all behaviours which cannot be shown to violate #{P} by a finite [bad prefix](ltp-000B).}
7
+
\p{It follows that #{P} is a [safety property](ltp-0004) iff #{\sc{P} = P}.}
8
+
\p{This is a closure operator, so it is extensive (#{\sc{P} \supseteq P}), idempotent (#{\sc{\sc{P}} = \sc{P}}), and monotonic (#{P \subseteq R} implies #{\sc{P} \subseteq \sc{R}}). }
9
+
\p{[Topologically speaking](ltp-0007), the safety closure is the (limit-)\em{closure}.}
+9
trees/ltp/ltp-000K.tree
+9
trees/ltp/ltp-000K.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Liveness properties are dense}
5
+
\meta{source}{(from [[alpern-schneider-1985]])}
6
+
\p{In the [topology of properties](ltp-0007), a property #{P} is a [liveness property](ltp-0006) iff #{P} is dense. In other words, when the [safety closure](ltp-000J) #{\sc{P} = \itraces}.}
7
+
\proofblock{
8
+
\p{ If #{\sigma \in \sc{P}} that means no finite prefix of #{\sigma} can be used to rule out #{P}, i.e. every prefix of #{\sigma} can be extended in some way to a behaviour in #{P}. If #{\sc{P} = \itraces}, this means that \em{every} finite prefix can be extended to a behaviour in #{P}, which is exactly the definition of a [liveness property](ltp-0006).
9
+
}}
+18
trees/ltp/ltp-000L.tree
+18
trees/ltp/ltp-000L.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Safety-liveness decomposition}
5
+
\meta{source}{(from [[alpern-schneider-1985]])}
6
+
\p{Every [property](ltp-0003) is the intersection of a [safety](ltp-0004) and a [liveness](ltp-0006) property.}
7
+
\proofblock{
8
+
\p{Let #{P} be a property. Then, let #{L} = #{\compl{(\sc{P} \setminus P)}}. Then: }
9
+
##{\begin{array}{lcl}
10
+
L \cap \sc{P} & = & \compl{(\sc{P} \setminus P)} \cap \sc{P} \\
11
+
& = & (\compl{\sc{P}} \cup P) \cap \sc{P} \\
12
+
& = & (\compl{\sc{P}} \cap \sc{P}) \cup (P \cap \sc{P}) \\
13
+
& = & \emptyset \cup (P \cap \sc{P}) \\
14
+
& = & P
15
+
\end{array}}
16
+
\p{The set #{\sc{P}} is clearly [closed](ltp-000J) and therefore a [safety property](ltp-0004). It remains to show that #{L} is [dense](ltp-000K) (and therefore a [liveness property](ltp-0006)). }
17
+
\p{Assume for contradiction that #{A = \compl{(\sc{P}\setminus P)}} is not [dense](ltp-000K), so there exists #{\sigma \in \itraces} such that #{\sigma \notin \sc{A}}. By our definition of [safety closure](ltp-000J), some finite prefix #{u} of #{\sigma} is a [bad prefix](ltp-000B) of #{A}, meaning no extension of #{u} lies in #{A}. Hence every extension of #{u} lies in #{\sc{P} \setminus P}, i.e. every extension of #{u} lies in #{\sc{P}} but not in #{P}. Because every extension of #{u} lies in #{\sc{P}}, #{u} cannot finitely refute #{P}, so every extension of #{u} must be extendable to some trace in #{P}, contradicting that no extension of #{u} lies in #{P}. Therefore no such #{u} exists, so every [behaviour](ltp-0002) #{\sigma} is in #{\sc{A}}, and #{A} is [dense](ltp-000K).
18
+
}}
+16
trees/ltp/ltp-000M.tree
+16
trees/ltp/ltp-000M.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\author{liamoc}
5
+
\title{A metric space of properties}
6
+
\p{The [topological space of properties](ltp-0007) is a metric space by the following metric, standard for Cantor or Baire spaces:}
7
+
##{d(\sigma,\rho) = \begin{cases} 0 & \text{if}\ \sigma = \rho \\
8
+
2^{-\startverb\!\stopverb\sup\{\ \ell\ \mid\ \forall i < \ell.\ \sigma_i = \rho_i\}} & \text{otherwise}\end{cases}}
9
+
\p{The function #{d} is a valid metric as #{d(\sigma,\rho) = 0} iff #{\sigma = \rho}, #{d} is symmetric, and the triangle inequality holds: ##{d(\sigma,\rho) \leq d(\sigma,\tau) + d(\tau,\rho)}}
10
+
\proofblock{
11
+
It suffices to show that a [property](ltp-0003) #{P} is a [guarantee property](ltp-0005) (i.e. [open](ltp-0007)) iff #{P} is open in the metric topology, i.e. #{\forall \sigma \in P.\ \exists \varepsilon > 0.\ \{ \rho \mid d(\sigma,\rho) < \varepsilon \} \subseteq P }.
12
+
\ul{
13
+
\li{#{\implies\startverb\!:\stopverb} Assume #{P} is a [guarantee property](ltp-0005). Let #{\sigma \in P}. Then, because #{P} is guarantee, there must exist some finite prefix #{p} of #{\sigma} which is [good](ltp-000D) for #{P}, i.e. all extensions of #{p} are in #{P}. Set #{r = |p| - 1} and #{\varepsilon = 2^{-r}}. Then the metric ball of radius #{\varepsilon}, i.e. #{\{ u \mid d(t,u) < \varepsilon \}}, is the set of all infinite extensions of #{p}, because #{d(\sigma,\rho) < 2^{-r}} iff #{\sigma} and #{\rho} agree for a prefix of length #{r + 1} — that is, #{p}. Since #{\sigma} was arbitrary, this shows that #{\forall \sigma \in P.\ \exists \varepsilon > 0.\ \{ \rho \mid d(\sigma,\rho) < \varepsilon \} \subseteq P} as required.}
14
+
\li{#{\impliedby\startverb\!:\stopverb} Assume #{P} is open in the metric topology, i.e. that #{\forall \sigma \in P.\ \exists \varepsilon > 0.\ \{ \rho \mid d(\sigma,\rho) < \varepsilon \} \subseteq P}. We shall show that #{P} is a [guarantee property](ltp-0005), by showing that it is contained in its [guarantee kernel](ltp-000I) #{P \subseteq \gk{P}}. Assume #{\sigma \in P}. Let #{\varepsilon > 0} be such that #{\{ \rho \mid d(\sigma,\rho) < \varepsilon \} \subseteq P }. By the Archimedean property, there must be some natural number #{r} such that #{2^{-r} < \varepsilon}. The ball of radius #{2^{-r}}, i.e. #{\{ \rho \mid d(\sigma,\rho) < 2^{-r} \}} is therefore contained within the ball of radius #{\varepsilon}, which, by our openness assumption, must in turn be contained within #{P}. Because #{d(\sigma,\rho) < 2^{-r}} iff #{\sigma} and #{\rho} agree for a prefix of length #{r + 1}, let #{p} be a prefix of #{\sigma} of length #{r + 1}. Then the ball of radius #{2^{-r}} is exactly all infinite extensions of #{p}. As our openness assumption says that this ball is a subset of #{P}, all infinite extensions of #{p} are therefore in #{P} and thus #{p} is a [good prefix](ltp-000D) of #{P}. This shows, as #{\sigma} was arbitrary, that all #{\sigma \in P} are the extension of some [good prefix](ltp-000D), and therefore that #{\sigma \in \gk{P}}. Therefore #{P \subseteq \gk{P}} and {P} is a [guarantee property](ltp-0005).}
15
+
}
16
+
}
+6
trees/ltp/ltp-macros.tree
+6
trees/ltp/ltp-macros.tree
+6
trees/people/kupferman.tree
+6
trees/people/kupferman.tree
+10
trees/people/lamport.tree
+10
trees/people/lamport.tree
+6
trees/people/vardi.tree
+6
trees/people/vardi.tree
+5
trees/places/fmsd.tree
+5
trees/places/fmsd.tree
+4
trees/places/huji.tree
+4
trees/places/huji.tree
+3
trees/places/ieeetse.tree
+3
trees/places/ieeetse.tree
+3
trees/places/msr.tree
+3
trees/places/msr.tree
+4
trees/places/rice.tree
+4
trees/places/rice.tree
+1
trees/refs/alpern-schneider-1985.tree
+1
trees/refs/alpern-schneider-1985.tree
+11
trees/refs/amjad-vanglabbeek-oconnor-2026.tree
+11
trees/refs/amjad-vanglabbeek-oconnor-2026.tree
+8
trees/refs/kupferman-vardi-2001.tree
+8
trees/refs/kupferman-vardi-2001.tree