From 8c5950ca592a525732570b63b3f108ecc9717796 Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Sun, 12 Apr 2026 01:51:22 +1000 Subject: [PATCH] adding many ltp notes --- theme | 2 +- trees/ltp/ltp-0001.tree | 42 ++++++++++++++----- trees/ltp/ltp-0002.tree | 6 ++- trees/ltp/ltp-0003.tree | 3 +- trees/ltp/ltp-0004.tree | 2 +- trees/ltp/ltp-0005.tree | 8 ++-- trees/ltp/ltp-0006.tree | 6 +++ trees/ltp/ltp-0007.tree | 5 +++ trees/ltp/ltp-0008.tree | 7 ++++ trees/ltp/ltp-0009.tree | 10 +++++ trees/ltp/ltp-000A.tree | 11 +++++ trees/ltp/ltp-000B.tree | 8 ++++ trees/ltp/ltp-000C.tree | 9 ++++ trees/ltp/ltp-000D.tree | 8 ++++ trees/ltp/ltp-000E.tree | 6 +++ trees/ltp/ltp-000F.tree | 7 ++++ trees/ltp/ltp-000G.tree | 10 +++++ trees/ltp/ltp-000H.tree | 6 +++ trees/ltp/ltp-000I.tree | 9 ++++ trees/ltp/ltp-000J.tree | 9 ++++ trees/ltp/ltp-000K.tree | 9 ++++ trees/ltp/ltp-000L.tree | 18 ++++++++ trees/ltp/ltp-000M.tree | 16 +++++++ trees/ltp/ltp-macros.tree | 6 +++ trees/people/kupferman.tree | 6 +++ trees/people/lamport.tree | 10 +++++ trees/people/vardi.tree | 6 +++ trees/places/fmsd.tree | 5 +++ trees/places/huji.tree | 4 ++ trees/places/ieeetse.tree | 3 ++ trees/places/msr.tree | 3 ++ trees/places/rice.tree | 4 ++ trees/refs/alpern-schneider-1985.tree | 1 + .../refs/amjad-vanglabbeek-oconnor-2026.tree | 11 +++++ trees/refs/kupferman-vardi-2001.tree | 8 ++++ trees/refs/lamport-1977.tree | 7 ++++ 36 files changed, 272 insertions(+), 19 deletions(-) create mode 100644 trees/ltp/ltp-0006.tree create mode 100644 trees/ltp/ltp-0007.tree create mode 100644 trees/ltp/ltp-0008.tree create mode 100644 trees/ltp/ltp-0009.tree create mode 100644 trees/ltp/ltp-000A.tree create mode 100644 trees/ltp/ltp-000B.tree create mode 100644 trees/ltp/ltp-000C.tree create mode 100644 trees/ltp/ltp-000D.tree create mode 100644 trees/ltp/ltp-000E.tree create mode 100644 trees/ltp/ltp-000F.tree create mode 100644 trees/ltp/ltp-000G.tree create mode 100644 trees/ltp/ltp-000H.tree create mode 100644 trees/ltp/ltp-000I.tree create mode 100644 trees/ltp/ltp-000J.tree create mode 100644 trees/ltp/ltp-000K.tree create mode 100644 trees/ltp/ltp-000L.tree create mode 100644 trees/ltp/ltp-000M.tree create mode 100644 trees/ltp/ltp-macros.tree create mode 100644 trees/people/kupferman.tree create mode 100644 trees/people/lamport.tree create mode 100644 trees/people/vardi.tree create mode 100644 trees/places/fmsd.tree create mode 100644 trees/places/huji.tree create mode 100644 trees/places/ieeetse.tree create mode 100644 trees/places/msr.tree create mode 100644 trees/places/rice.tree create mode 100644 trees/refs/amjad-vanglabbeek-oconnor-2026.tree create mode 100644 trees/refs/kupferman-vardi-2001.tree create mode 100644 trees/refs/lamport-1977.tree diff --git a/theme b/theme index 3bdbca1..f4c0bce 160000 --- a/theme +++ b/theme @@ -1 +1 @@ -Subproject commit 3bdbca15641aac49d886d1d07ff0f218a8b3363f +Subproject commit f4c0bce2888561ae19b025921c6e85ec8c6eb4fa diff --git a/trees/ltp/ltp-0001.tree b/trees/ltp/ltp-0001.tree index a98e6e1..ab1e291 100644 --- a/trees/ltp/ltp-0001.tree +++ b/trees/ltp/ltp-0001.tree @@ -1,17 +1,37 @@ \taxon{Research Notebook} -\title{Linear-time Temporal Properties} +\title{Linear-time temporal properties} \author{liamoc} \transclude{ltp-0002} \transclude{ltp-0003} +\subtree{ + \title{Concerning safety properties} \transclude{ltp-0004} +\scope{\put\transclude/metadata{true}\transclude{ltp-000B}} +\transclude{ltp-000A} +\transclude{ltp-0009} +\transclude{ltp-000E} +\transclude{ltp-0008} +} +\subtree{ + \title{Concerning guarantee properties} \transclude{ltp-0005} -\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}. } -\p{This space is a metric space, using the standard prefix-agreement metric that one might use for a Baire or Cantor space: } -##{ - \begin{array}{l} - d : \Sigma^\omega \times \Sigma^\omega \rightarrow \mathbb{R} \\ - d(\sigma,\rho) = 2^{-\sup\{ i \mid \sigma_{0\dots{}i} = \rho_{0\dots{}i}\}} \\ - \\ - \qquad\text{where}\ 2^{-\infty} = 0 -\end{array}} -\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})} \ No newline at end of file +\scope{\put\transclude/metadata{true}\transclude{ltp-000D}} +\transclude{ltp-000C} +\transclude{ltp-000G} +\transclude{ltp-000H} +\transclude{ltp-000F} +} +\subtree{ + \title{Properties as a topological space} + \scope{\put\transclude/metadata{true}\transclude{ltp-0007}} + \scope{\put\transclude/metadata{true}\transclude{ltp-000I}} + \scope{\put\transclude/metadata{true}\transclude{ltp-000J}} + \transclude{ltp-000M} +} +\subtree{ + \title{Concerning liveness properties} + \transclude{ltp-0006} + \scope{\put\transclude/metadata{true}\transclude{ltp-000K}} + \scope{\put\transclude/metadata{true}\transclude{ltp-000L}} + % closure properties go here? +} diff --git a/trees/ltp/ltp-0002.tree b/trees/ltp/ltp-0002.tree index 4b63972..d01e639 100644 --- a/trees/ltp/ltp-0002.tree +++ b/trees/ltp/ltp-0002.tree @@ -1,5 +1,7 @@ \taxon{Definition} -\title{The space #{\Sigma^\omega}} +\import{ltp-macros} +\title{Traces and behaviours} \author{liamoc} -\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.} +\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}. } +\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. } \p{We shall model terminating systems, which have finite behaviours, as behaviours that infinitely repeat their final state.} \ No newline at end of file diff --git a/trees/ltp/ltp-0003.tree b/trees/ltp/ltp-0003.tree index be798fe..6bffec7 100644 --- a/trees/ltp/ltp-0003.tree +++ b/trees/ltp/ltp-0003.tree @@ -1,4 +1,5 @@ \title{Properties} \taxon{Definition} +\import{ltp-macros} \author{liamoc} -\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. } \ No newline at end of file +\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. } \ No newline at end of file diff --git a/trees/ltp/ltp-0004.tree b/trees/ltp/ltp-0004.tree index f1d402f..62ea94b 100644 --- a/trees/ltp/ltp-0004.tree +++ b/trees/ltp/ltp-0004.tree @@ -1,5 +1,5 @@ \taxon{Definition} \author{liamoc} -\title{Safety Properties} +\title{Safety properties} \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.} \p{For example, the safety property "The state #{\mathtt{a}} is never reached" is violated by any finite prefix containing the state #{\mathtt{a}}.} \ No newline at end of file diff --git a/trees/ltp/ltp-0005.tree b/trees/ltp/ltp-0005.tree index 8e87da6..fa11591 100644 --- a/trees/ltp/ltp-0005.tree +++ b/trees/ltp/ltp-0005.tree @@ -1,5 +1,7 @@ +\import{ltp-macros} \taxon{Definition} \author{liamoc} -\title{Guarantee Properties} -\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.} -\p{For example, the guarantee property "The state #{\mathtt{a}} is eventually reached" is satisfied by any finite prefix containing the state #{\mathtt{a}}.} \ No newline at end of file +\title{Guarantee properties} +\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.} +\p{For example, the guarantee property "The state #{\mathtt{a}} is eventually reached" is satisfied by any finite prefix containing the state #{\mathtt{a}}.} +\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). } \ No newline at end of file diff --git a/trees/ltp/ltp-0006.tree b/trees/ltp/ltp-0006.tree new file mode 100644 index 0000000..6fd5f63 --- /dev/null +++ b/trees/ltp/ltp-0006.tree @@ -0,0 +1,6 @@ +\taxon{Definition} +\import{ltp-macros} +\author{liamoc} +\title{Liveness properties} +\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}.} +\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. } \ No newline at end of file diff --git a/trees/ltp/ltp-0007.tree b/trees/ltp/ltp-0007.tree new file mode 100644 index 0000000..d6f1ed8 --- /dev/null +++ b/trees/ltp/ltp-0007.tree @@ -0,0 +1,5 @@ +\taxon{Construction} +\import{ltp-macros} +\meta{source}{(from [[alpern-schneider-1985]])} +\title{Behaviours as topology} +\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}).} \ No newline at end of file diff --git a/trees/ltp/ltp-0008.tree b/trees/ltp/ltp-0008.tree new file mode 100644 index 0000000..c0e3d32 --- /dev/null +++ b/trees/ltp/ltp-0008.tree @@ -0,0 +1,7 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Safety properties are closed under intersection} +\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). } +\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).} diff --git a/trees/ltp/ltp-0009.tree b/trees/ltp/ltp-0009.tree new file mode 100644 index 0000000..8c115d5 --- /dev/null +++ b/trees/ltp/ltp-0009.tree @@ -0,0 +1,10 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Safety properties are closed under finite union} +\p{The union of any two [safety properties](ltp-0004) is a [safety property](ltp-0004). } +\proofblock{ +\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). + } +} diff --git a/trees/ltp/ltp-000A.tree b/trees/ltp/ltp-000A.tree new file mode 100644 index 0000000..bfa8748 --- /dev/null +++ b/trees/ltp/ltp-000A.tree @@ -0,0 +1,11 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Trivial properties are safety properties} +\p{The empty property #{\emptyset} and the [property](ltp-0003) #{\itraces} are both [safety properties](ltp-0004).} +\proofblock{ +\p{The property #{\itraces} has no violating [behaviours](ltp-0002), so vacuously all violations can be established by finite prefixes.} +\p{For the property #{\emptyset}, all [behaviours](ltp-0002) are violating, so the empty prefix #{\varepsilon} is a [bad prefix](ltp-000B). +} +} diff --git a/trees/ltp/ltp-000B.tree b/trees/ltp/ltp-000B.tree new file mode 100644 index 0000000..5318dac --- /dev/null +++ b/trees/ltp/ltp-000B.tree @@ -0,0 +1,8 @@ +\taxon{Definition} +\import{dt-macros} +\import{ltp-macros} +\meta{source}{(from [[kupferman-vardi-2001]])} +\title{Bad prefixes} +\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}.} +\p{A [property](ltp-0003) #{P} is a [safety property](ltp-0004) iff all violating [behaviours](ltp-0002) are extensions of bad prefixes. +} diff --git a/trees/ltp/ltp-000C.tree b/trees/ltp/ltp-000C.tree new file mode 100644 index 0000000..537365b --- /dev/null +++ b/trees/ltp/ltp-000C.tree @@ -0,0 +1,9 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Trivial properties are guarantee properties} +\p{The empty property #{\emptyset} and the [property](ltp-0003) #{\itraces} are both [guarantee properties](ltp-0005).} +\proofblock{ +\p{Follows from \ref{ltp-000A} as the complement of any [safety property](ltp-0004) is a [guarantee property](ltp-0005).} +} diff --git a/trees/ltp/ltp-000D.tree b/trees/ltp/ltp-000D.tree new file mode 100644 index 0000000..8a54986 --- /dev/null +++ b/trees/ltp/ltp-000D.tree @@ -0,0 +1,8 @@ +\taxon{Definition} +\import{dt-macros} +\import{ltp-macros} +\meta{source}{(from [[kupferman-vardi-2001]])} +\title{Good prefixes} +\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}.} +\p{A [property](ltp-0003) #{P} is a [guarantee property](ltp-0005) iff all satisfying [behaviours](ltp-0002) are extensions of good prefixes. +} diff --git a/trees/ltp/ltp-000E.tree b/trees/ltp/ltp-000E.tree new file mode 100644 index 0000000..351e606 --- /dev/null +++ b/trees/ltp/ltp-000E.tree @@ -0,0 +1,6 @@ +\taxon{Counterexample} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Safety properties are not closed under infinite union} +\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). } \ No newline at end of file diff --git a/trees/ltp/ltp-000F.tree b/trees/ltp/ltp-000F.tree new file mode 100644 index 0000000..f275cc7 --- /dev/null +++ b/trees/ltp/ltp-000F.tree @@ -0,0 +1,7 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Guarantee properties are closed under union} +\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). } +\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).}} \ No newline at end of file diff --git a/trees/ltp/ltp-000G.tree b/trees/ltp/ltp-000G.tree new file mode 100644 index 0000000..6aee495 --- /dev/null +++ b/trees/ltp/ltp-000G.tree @@ -0,0 +1,10 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Guarantee properties are closed under finite intersection} +\p{The intersection of any two [guarantee properties](ltp-0005) is a [guarantee property](ltp-0005). } +\proofblock{ +\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). + } +} diff --git a/trees/ltp/ltp-000H.tree b/trees/ltp/ltp-000H.tree new file mode 100644 index 0000000..f0cfe0b --- /dev/null +++ b/trees/ltp/ltp-000H.tree @@ -0,0 +1,6 @@ +\taxon{Counterexample} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{Guarantee properties are not closed under infinite intersection} +\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). } \ No newline at end of file diff --git a/trees/ltp/ltp-000I.tree b/trees/ltp/ltp-000I.tree new file mode 100644 index 0000000..27f8de7 --- /dev/null +++ b/trees/ltp/ltp-000I.tree @@ -0,0 +1,9 @@ +\taxon{Definition} +\import{dt-macros} +\import{ltp-macros} +\title{Guarantee kernel} +\meta{source}{(from [[amjad-vanglabbeek-oconnor-2026]])} +\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}. } +\p{It follows that #{P} is a [guarantee property](ltp-0005) iff #{\gk{P} = P}.} +\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}}). } +\p{[Topologically speaking](ltp-0007), the guarantee kernel is the \em{interior operator}.} \ No newline at end of file diff --git a/trees/ltp/ltp-000J.tree b/trees/ltp/ltp-000J.tree new file mode 100644 index 0000000..1b62d83 --- /dev/null +++ b/trees/ltp/ltp-000J.tree @@ -0,0 +1,9 @@ +\taxon{Definition} +\import{dt-macros} +\import{ltp-macros} +\title{Safety closure} +\meta{source}{(from [[alpern-schneider-1985]])} +\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).} +\p{It follows that #{P} is a [safety property](ltp-0004) iff #{\sc{P} = P}.} +\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}}). } +\p{[Topologically speaking](ltp-0007), the safety closure is the (limit-)\em{closure}.} \ No newline at end of file diff --git a/trees/ltp/ltp-000K.tree b/trees/ltp/ltp-000K.tree new file mode 100644 index 0000000..6fdc9aa --- /dev/null +++ b/trees/ltp/ltp-000K.tree @@ -0,0 +1,9 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\title{Liveness properties are dense} +\meta{source}{(from [[alpern-schneider-1985]])} +\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}.} +\proofblock{ +\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). +}} \ No newline at end of file diff --git a/trees/ltp/ltp-000L.tree b/trees/ltp/ltp-000L.tree new file mode 100644 index 0000000..7e41103 --- /dev/null +++ b/trees/ltp/ltp-000L.tree @@ -0,0 +1,18 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\title{Safety-liveness decomposition} +\meta{source}{(from [[alpern-schneider-1985]])} +\p{Every [property](ltp-0003) is the intersection of a [safety](ltp-0004) and a [liveness](ltp-0006) property.} +\proofblock{ +\p{Let #{P} be a property. Then, let #{L} = #{\compl{(\sc{P} \setminus P)}}. Then: } +##{\begin{array}{lcl} +L \cap \sc{P} & = & \compl{(\sc{P} \setminus P)} \cap \sc{P} \\ +& = & (\compl{\sc{P}} \cup P) \cap \sc{P} \\ +& = & (\compl{\sc{P}} \cap \sc{P}) \cup (P \cap \sc{P}) \\ +& = & \emptyset \cup (P \cap \sc{P}) \\ +& = & P +\end{array}} +\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)). } +\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). +}} diff --git a/trees/ltp/ltp-000M.tree b/trees/ltp/ltp-000M.tree new file mode 100644 index 0000000..7f04742 --- /dev/null +++ b/trees/ltp/ltp-000M.tree @@ -0,0 +1,16 @@ +\taxon{Theorem} +\import{dt-macros} +\import{ltp-macros} +\author{liamoc} +\title{A metric space of properties} +\p{The [topological space of properties](ltp-0007) is a metric space by the following metric, standard for Cantor or Baire spaces:} +##{d(\sigma,\rho) = \begin{cases} 0 & \text{if}\ \sigma = \rho \\ + 2^{-\startverb\!\stopverb\sup\{\ \ell\ \mid\ \forall i < \ell.\ \sigma_i = \rho_i\}} & \text{otherwise}\end{cases}} +\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)}} +\proofblock{ + 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 }. + \ul{ + \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.} + \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).} +} +} \ No newline at end of file diff --git a/trees/ltp/ltp-macros.tree b/trees/ltp/ltp-macros.tree new file mode 100644 index 0000000..8b17f96 --- /dev/null +++ b/trees/ltp/ltp-macros.tree @@ -0,0 +1,6 @@ +\def\itraces{\Sigma^\omega} +\def\ftraces{\Sigma^\ast} +\def\fitraces{\Sigma^\infty} +\def\compl[body]{\body^\complement} +\def\gk[body]{\underline{\body}} +\def\sc[body]{\overline{\body}} \ No newline at end of file diff --git a/trees/people/kupferman.tree b/trees/people/kupferman.tree new file mode 100644 index 0000000..f7ae9d4 --- /dev/null +++ b/trees/people/kupferman.tree @@ -0,0 +1,6 @@ +\title{Orna Kupferman} +\taxon{Person} +\meta{external}{https://www.cs.huji.ac.il/~ornak/} +\meta{institution}{[[huji]]} +\meta{orcid}{0000-0003-4699-6117} +\meta{position}{Professor} \ No newline at end of file diff --git a/trees/people/lamport.tree b/trees/people/lamport.tree new file mode 100644 index 0000000..5af4ab9 --- /dev/null +++ b/trees/people/lamport.tree @@ -0,0 +1,10 @@ +\title{Leslie Lamport} +\taxon{Person} +\meta{external}{https://lamport.azurewebsites.net/} +\meta{institution}{[[msr]]} +\meta{orcid}{0000-0002-9756-1327} +\meta{position}{Distinguished Scientist (Retired)} + + + + diff --git a/trees/people/vardi.tree b/trees/people/vardi.tree new file mode 100644 index 0000000..d53d203 --- /dev/null +++ b/trees/people/vardi.tree @@ -0,0 +1,6 @@ +\title{Moshe Vardi} +\taxon{Person} +\meta{external}{https://www.cs.rice.edu/~vardi/} +\meta{institution}{[[rice]]} +\meta{orcid}{0000-0002-0661-5773} +\meta{position}{Karen Ostrum George Distinguished Service Professor} diff --git a/trees/places/fmsd.tree b/trees/places/fmsd.tree new file mode 100644 index 0000000..de9e39c --- /dev/null +++ b/trees/places/fmsd.tree @@ -0,0 +1,5 @@ +\title{Formal Methods in System Design} +\taxon{Journal} +\meta{external}{https://link.springer.com/journal/10703} + +\p{Formal Methods in System Design is a journal dedicated to presenting the latest advancements in formal methods for hardware and software system design.} diff --git a/trees/places/huji.tree b/trees/places/huji.tree new file mode 100644 index 0000000..b12b596 --- /dev/null +++ b/trees/places/huji.tree @@ -0,0 +1,4 @@ +\title{Hebrew University} +\taxon{Institution} +\meta{venue}{Jerusalem} +\meta{external}{https://huji.ac.il} diff --git a/trees/places/ieeetse.tree b/trees/places/ieeetse.tree new file mode 100644 index 0000000..add6aa1 --- /dev/null +++ b/trees/places/ieeetse.tree @@ -0,0 +1,3 @@ +\title{IEEE Transactions on Software Engineering} +\taxon{Journal} +\meta{external}{https://www.computer.org/csdl/journal/ts} \ No newline at end of file diff --git a/trees/places/msr.tree b/trees/places/msr.tree new file mode 100644 index 0000000..ec05005 --- /dev/null +++ b/trees/places/msr.tree @@ -0,0 +1,3 @@ +\title{Microsoft Research} +\taxon{Institution} +\meta{external}{https://www.microsoft.com/en-us/research/} \ No newline at end of file diff --git a/trees/places/rice.tree b/trees/places/rice.tree new file mode 100644 index 0000000..b250f25 --- /dev/null +++ b/trees/places/rice.tree @@ -0,0 +1,4 @@ +\title{Rice University} +\taxon{Institution} +\meta{external}{https://www.rice.edu/} +\meta{venue}{Houston, Texas} \ No newline at end of file diff --git a/trees/refs/alpern-schneider-1985.tree b/trees/refs/alpern-schneider-1985.tree index 2d7385f..4b1bac8 100644 --- a/trees/refs/alpern-schneider-1985.tree +++ b/trees/refs/alpern-schneider-1985.tree @@ -1,5 +1,6 @@ \author{alpern} \author{schneider} +\taxon{Reference} \meta{venue}{[[ipl]], Volume 21, Issue 4} \tag{refereed} \date{1985-10-07} diff --git a/trees/refs/amjad-vanglabbeek-oconnor-2026.tree b/trees/refs/amjad-vanglabbeek-oconnor-2026.tree new file mode 100644 index 0000000..b0bffe7 --- /dev/null +++ b/trees/refs/amjad-vanglabbeek-oconnor-2026.tree @@ -0,0 +1,11 @@ +\title{The Infinite, in Finite Time} +\taxon{Reference} +\meta{venue}{To appear} +\author{rayhana} +\author{rvg} +\author{liamoc} +\date{2026} +%\meta{doi}{10.4204/EPTCS.412.4} +\tag{temporal-logic} +\tag{semantics} +%\tag{refereed} diff --git a/trees/refs/kupferman-vardi-2001.tree b/trees/refs/kupferman-vardi-2001.tree new file mode 100644 index 0000000..2def0ea --- /dev/null +++ b/trees/refs/kupferman-vardi-2001.tree @@ -0,0 +1,8 @@ +\title{Model Checking of Safety Properties} +\taxon{Reference} +\meta{venue}{[[fmsd]] 19 291–314} +\author{kupferman} +\author{vardi} +\meta{doi}{10.1023/A:1011254632723} +\date{2001-11} +\tag{refereed} \ No newline at end of file diff --git a/trees/refs/lamport-1977.tree b/trees/refs/lamport-1977.tree new file mode 100644 index 0000000..e853728 --- /dev/null +++ b/trees/refs/lamport-1977.tree @@ -0,0 +1,7 @@ +\title{Proving the Correctness of Multiprocess Programs} +\taxon{Reference} +\meta{venue}{[[ieeetse]] 3 125–143} +\meta{doi}{10.1109/TSE.1977.229904} +\author{lamport} +\date{1977-03} +\tag{refereed} \ No newline at end of file -- 2.51.2