7.5: A topos of behavior types

Now that we have discussed logic in a sheaf topos, we return to our motivating example, a topos of behavior types. We begin by discussing the topological space on which behavior types will be sheaves, a space called the interval domain.

Remark 7.75. Note that above, we were thinking very intuitively about time, e.g. when we discussed people being worried about the news. Now we will be thinking about time in a different way, but there is no need to change your answers or reconsider the intuitive thinking done above.

7.5.1 The interval domain

The interval domain \(\mathbb{I}\)\(\mathbb{R}\) is a specific topological space, which we will use to model intervals of time.

In other words, we will be interested in the category Shv(\(\mathbb{I}\)\(\mathbb{R}\)) of sheaves on the interval domain.

To give a topological space, one must give a pair (X, Op), where X is a set of ‘points’ and Op is a topology on X; see Definition 7.25.

The set of points for \(\mathbb{I}\)\(\mathbb{R}\) is that of all finite closed intervals

\(\mathbb{I}\)\(\mathbb{R}\) := {[d, u] \(\subseteq\) \(\mathbb{R}\) | d ≤ u}.

For a < b in \(\mathbb{R}\), let o\(_{[a,b]}\) denote theset o\(_{[a,b]}\) := {[d,u] \(\in\) \(\mathbb{I}\)\(\mathbb{R}\)| a < d ≤ u < b}; these are called basic open sets. The topology Op is determined by these basic open sets in that a subset U is open if it is the union of some collection of basic open sets.

Thus for example, o\(_{[0,5]}\) is an open set: it contains every [d, u] contained in the open interval {x \(\in\) \(\mathbb{R}\) | 0 < x < 5}. Similarly o\(_{[4,8]}\) is an open set, but note that o\(_{[0,5]}\) \(\bigcup\) o\(_{[4,8]}\) \(\neq\) o\(_{[0,8]}\). Indeed, the interval [2, 6] is in the right-hand side but not the left.

Exercise 7.76

1. Explain why [2, 6] \(\in\) o\(_{[0,8]}\).

2. Explain why [2, 6] \(\not \in\) o\(_{[0,5]}\) \(\bigcup\) o\(_{[4,8]}\). ♦

Let Op denote the open sets of IR, as described above, and let BT := Shv(\(\mathbb{I}\)\(\mathbb{R}\), Op) denote the topos of sheaves on this space.

We call it the topos of behavior types. There is an important subspace of \(\mathbb{I}\)\(\mathbb{R}\), namely the usual space of real numbers \(\mathbb{R}\).

We see \(\mathbb{R}\) as a subspace of \(\mathbb{I}\)\(\mathbb{R}\) via the isomorphism

\(\mathbb{R}\) \(\cong\) {[d, u] \(\in\) \(\mathbb{I}\)\(\mathbb{R}\) | d = u}.

We discussed the usual topology on \(\mathbb{R}\) in Example 7.26, but we also get a topology on \(\mathbb{R}\) because it is a subset of \(\mathbb{I}\)\(\mathbb{R}\); i.e. we have the subspace topology as described in Exercise 7.32. These agree, as the reader can check.

Exercise 7.77

Show that a subset U \(\subseteq\) \(\mathbb{R}\) is open in the subspace topology of \(\mathbb{R}\) \(\subseteq\) \(\mathbb{I}\)\(\mathbb{R}\) iff U ∩ \(\mathbb{R}\) is open in the usual topology on \(\mathbb{R}\) defined in Example 7.26. ♦

7.5.2 Sheaves on \(\mathbb{I}\)\(\mathbb{R}\)

We cannot go into much depth about the sheaf topos BT = Shv(\(\mathbb{I}\)\(\mathbb{R}\), Op), for reasons of space; we refer the interested reader to Section 7.6. In this section we will briefly discuss what it means to be a sheaf on \(\mathbb{I}\)\(\mathbb{R}\), giving a few examples including that of the subobject classifier.

What is a sheaf on \(\mathbb{I}\)\(\mathbb{R}\)? A sheaf S on the interval domain (\(\mathbb{I}\)\(\mathbb{R}\),Op) is a functor S : Op\(^{op}\) → Set: it assigns to each open set U a set S(U); how should we interpret this? An element s \(\in\) S(U) is something that says is an “event that takes place throughout the interval U.” Given this U-event s together with an open subset of V \(\subseteq\) U, there is a V-event s|\(_{V}\) that tells us what s is if we regard it as an event taking place throughout V.

If U = \(\bigcup_{i \in I} U_{i}\) and we can find matching U\(_{i}\)-events (s\(_{i}\)) for each i \(\in\) I, then the sheaf condition (Definition 7.35) says that they have a unique gluing, i.e.

a U-event s \(\in\) S(U) that encompasses all of them: s|(_{U_{i}}}\) = s\(_{i}\) for each i \(\in\) I. We said in Section 7.5.1 that every open set U \(\subseteq\) \(\mathbb{I}\)\(\mathbb{R}\) can be written as the union of basic open sets o\(_{[a,b]}\).

This implies that any sheaf S is determined by its values S(o\(_{[a,b]}\)) on these basic open sets. The sheaf condition furthermore implies that these vary continuously in a certain sense, which we can express formally as

\(S\left(o_{[a, b]}\right) \cong \lim _{\epsilon>0} S\left(o_{[a-\epsilon, b+\epsilon]}\right)\)

However, rather than get into the details, we describe a few sorts of sheaves that may be of interest.

Example 7.78

For any set A there is a sheaf A \(\in\) Shv(\(\mathbb{I}\)\(\mathbb{R}\)) that assigns to each open set U the set A(U) := A. This allows us to refer to integers, or real numbers, or letters of an alphabet, as though they were behaviors. What sort of behavior is 7 \(\in\) N? It is the sort of behavior that never changes: it’s always seven. Thus A is called the constant sheaf on A.

Example 7.79

Fix any topological space (X, Op\(_{X}\)). Then there is a sheaf F\(_{X}\) of local functions from \(\mathbb{I}\)\(\mathbb{R}\) to X.

That is, for any open set U \(\in\) Op\(_{\mathbb{I}\mathbb{R}}\), we assign the set F\(_{X}\)(U) := {f : U → X | f is continuous}. There is also the sheaf G\(_{X}\) of local functions on the subspace \(\mathbb{R}\) \(\subseteq\) \(\mathbb{I}\)\(\mathbb{R}\). That is, for any open set U \(\in\) Op\(_{\mathbb{I}\mathbb{R}}\), we assign the set G\(_{X}\)(U) := {f : U ∩ \(\mathbb{R}\) → X | f is continuous}.

Exercise 7.80

Let’s check that Example 7.78 makes sense. Fix any topological space (X, Op\(_{X}\)) and any subset R \(\subseteq\) \(\mathbb{I}\)\(\mathbb{R}\) of the interval domain.

Define H\(_{X}\)(U) := {f : U ∩ R → X | f is continuous}.

1. Is H\(_{X}\) a presheaf? If not, why not; if so, what are the restriction maps?
2. Is H\(_{X}\) a sheaf? Why or why not? ♦

Example 7.81

Another source of examples comes from the world of open hybrid dynamical systems. These are machines whose behavior is a mixture of continuous movements—generally imagined as trajectories through a vector field—and discrete jumps. These jumps are imagined as being caused by signals that spontaneously arrive. Over any interval of time, a hybrid system has certain things that it can do and certain things that it cannot. Although we will not make this precise here, there is a construc- tion for converting any hybrid system into a sheaf on IR; we will give references in Section 7.6.

We refer to sheaves on \(\mathbb{I}\)\(\mathbb{R}\) as behavior types because almost any sort of behavior one can imagine is a behavior type. Of course, a complex behavior type such as the way someone acts when they are in love would be extremely hard to write down. But the idea is straightforward: for any interval of time, say a three-day interval (d, d + 3), let L(d, d + 3) denote these to fall possible behaviors a person who is inlove could possibly do. Obviously it’s a big, unwieldy set, and no one would want to make precise. But to the extent that one can imagine that sort of behavior as occurring through time, they could imagine the corresponding sheaf.

The subobject classifier as a sheaf on IR. In any sheaf topos, the subobject classifier Ω is itself a sheaf. It is responsible for the truth values in the topos.

As we said in Section 7.4.1, when it comes to sheaves on a topological space (X, Op), truth values are open subsets U \(\in\) Op.

BT is the topos of sheaves on the space (\(\mathbb{I}\)\(\mathbb{R}\), Op), as defined in Section 7.5.1. As always, the subobject classifier Ω assigns to any U \(\in\) Op the set of open subsets of U, so these are the truth values. But what do they mean? The idea is that every proposition, such as “Bob likes the weather” returns an open set U, as if to respond that Bob likes the weather “...throughout time period U.” Let’s explore this just a bit more. Suppose Bob likes the weather throughout the interval (0, 5) and throughout the interval (4, 8). We would probably conclude that Bob likes the weather throughout the interval (0, 8). But what about the more ominous statement “a single pair of eyes has remained watching position p.” Then just because it’s true on (0, 5) and on (4, 8), does not imply that it’s been true on (0, 8): there may have been a change of shift, where one watcher was relieved from their post by another watcher. As another example, consider the statement “the stock market did not go down by more than 10 points.” This might be true on (0, 5) and true on (4, 8) but not on (0, 8). In order to capture the semantics of statements like these statements that take time to evaluate we must use the space \(\mathbb{I}\)\(\mathbb{R}\) rather than the space \(\mathbb{R}\).

7.5.3 Safety proofs in temporal logic

We now have at least a basic idea of what goes into a proof of safety, say for autonomous vehicles, or airplanes in the national airspace system. In fact, the underlying ideas of this chapter came out of a project between MIT, Honeywell Inc., and NASA [SSV18]. The background for the project was that the National Airspace System consists of many different systems interacting: interactions between airplanes, each of which is an interaction between physics, humans, sensors, and actuators, each of which is an interaction between still more basic parts. The same sort of story would hold for a fleet of autonomous vehicles, as in the introduction to this chapter.

Suppose that each of the systems at any level is guaranteed to satisfy some property. For example, perhaps we can assume that an engine is either out of gas, has a broken fuel line, or is following the orders of a human driver or pilot. If there is a rupture in the fuel line, the sensors will alert the human within three seconds, etc. Each of the components interact with a number of different variables. In the case of airplanes, a pilot interacts with the radio, the positions of the dials, the position of the thruster, and the visual data in front of her. The component here the pilot is guaranteed to keep these variables in some relation: “if I see something, I will say something” or “if the dials are in position bad_pos, I will engage the thruster within 1 second.” We call these guarantees behavior contracts.

All of the above can be captured in the topos BT of behavior types. The variables are behavior types: the altimeter is a variable whose value θ \(\in\) \(\mathbb{R}\)\(_{≥0}\) is changing continuously with respect to time. The thruster is also a continuously-changing variable whose value is in the range [0, 1], etc.

The guaranteed relationships behavior contracts are given by predicates on variables. For example, if the pilot will always engage the thruster within one second of the display dials being in position bad_pos, this can be captured by a predicate p : dials × thrusters → Ω. While we have not written out a formal language for p, one could imagine the predicate p(D, T) for D : dials and T : thrusters as

\(\begin{aligned}
\forall(t: \mathbb{R}) . @_{t} &\left(\operatorname{bad}_{-} \operatorname{pos}(D)\right) \Rightarrow \\
& \exists(r: \mathbb{R}) \cdot(0<r<1) \wedge \forall\left(r^{\prime}: \mathbb{R}\right) \cdot 0 \leq r^{\prime} \leq 5 \Rightarrow @_{t+r+r^{\prime}}(\text { engaged }(T)) .
\end{aligned}\) (7.82)

Here @\(_{t}\) is a modality, as we discussed in Definition 7.69; in fact it turns out to be one of type 3. from Proposition 7.71, but we cannot go into that. For a proposition q, the statement @\(_{t}\)(q) says that q is true in some small enough neighborhood around t. So (7.82) says “starting within one second of whenever the dials say that we are in a bad position, I’ll engage the thrusters for five seconds.”

Given an actual playing-out-of-events over a time period U, i.e. actual section D \(\in\) dials(U) and section T \(\in\) thrusters(U), the predicate Eq. (7.82) will hold on certain parts of U and not others, and this is the truth value of p. Hopefully the pilot upholds her behavior contract at all times she is flying, in which case the truth value will be true throughout that interval U. But if the pilot breaks her contract over certain intervals, then this fact is recorded in Ω.

The logic allows us to record axioms like that shown in Eq. (7.82) and then reason from them: e.g. if the pilot and the airplane, and at least one of the three radars upholds its contract then safe separation will be maintained. We cannot give further details here, but these matters have been worked out in detail in [SS18]; see Section 7.6.