7.1: How can we prove our machine is safe?

Imagine you are trying to design a system of interacting components. You wouldn’t be doing this if you didn’t have a goal in mind: you want the system to do something, to behave in a certain way. In other words, you want to restrict its possibilities to a smaller set: you want the car to remain on the road, you want the temperature to remain in a particular range, you want the bridge to be safe for trucks to pass. Out of all the possibilities, your system should only permit some.

Since your system is made of components that interact in specified ways, the possible behavior of the whole in any environment is determined by the possible behaviors of each of its components in their local environments, together with the precise way in which they interact.1 In this chapter, we will discuss a logic wherein one can describe general types of behavior that occur over time, and prove properties of a larger-scale system from the properties and interaction patterns of its components.

For example, suppose we want an autonomous vehicle to maintain a distance of some safe \(\in\) \(\mathbb{R}\) from other objects. To do so, several components must interact: a sensor that approximates the real distance by an internal variable S′, a controller that uses S′ to decide what action A to take, and a motor that moves the vehicle with an acceleration based on A. This in turn affects the real distance S, so there is a feedback loop.

Consider the following model diagram:

In the diagram shown, the distance S is exposed by the exterior interface. This just means we imagine S as being a variable that other components of a larger system may want to interact with. We could have exposed no variables (making it a closed system) or we could have exposed A and/or S′ as well.

In order for the system to ensure S ≥ safe, we need each of the components to ensure a property of its own. But what are these components, ‘sensor, controller, motor’, and what do they do?

One way to think about any of the components is to open it up and see how it is put together; with a detailed study we may be able to say what it will do. For example, just as S was exposed in the diagram above, one could imagine opening up the ‘sensor’ component box in Eq. (7.1) and seeing an interaction between subcomponents

This ability to zoom in and see a single unit as being composed of others is important for design. But at the end of the day, you eventually need to stop diving down and simply use the properties of the components in front of you to prove properties of the composed system. Have no fear: everything we do in this chapter will be fully compositional, i.e. compatible with opening up lower-level subsystems and using the fractal-like nature of composition. However at a given time, your job is to design the system at a given level, taking the component properties of lower-level systems as given.

We will think of each component in terms of the relationship it maintains (through time) between the changing values on its ports. “Whenever I see a flash, I will increase pressure on the button”: this is a relationship I maintain through time between the changing values on my eye port and my finger port. We will make this more precise soon, but fleshing out the situation in Eq. (7.1) should help. The sensor maintains a relationship between S and S′, e.g. that the real distance S and its internal representationS′ differ by no more than 5cm. The controller maintains a relationship between S′ and the action signal A, e.g. that if at any time S < safe, then within one second it will emit the signal A = go. The motor maintains a relationship between A and S, e.g. that A dictates the second derivative of S by the formula

\(((A=\mathrm{go}) \Rightarrow \ddot{S}>1) \wedge((A=\mathrm{stop}) \Rightarrow \ddot{S}=0)\) (7.2)

If we want to prove properties of the whole interacting system, then the relation- ships maintained by each component need to be written in a formal logical language, something like what we saw in Eq. (7.2). From that basis, we can use standard proof techniques to combine properties of subsystems into properties of the whole. This is our objective in the present chapter.

We have said how component systems, wired together in some arrangement, create larger-scale systems. We have also said that, given the wiring arrangement, the be- havioral properties of the component systems dictate the behavioral properties of the whole. But what exactly are behavioral properties?

In this chapter, we want to give a formal language and semantics for a very gen- eral notion of behavior. Mathematics is itself a formal language; the usual style of mathematical modeling is to use any piece of this vast language at any time and for any reason. One uses “human understanding” to ensure that the different models are fitting together in an appropriate way when different systems are combined. The present work differs in that we want to find a domain-specific language for modeling behavior, any sort of behavior, and nothing but behavior. Unlike in the wide world of math, we want a setting where the only things that can be discussed are behaviors.

For this, we will construct what is called a topos, which is a special kind of category. Our topos, let’s call it BT, will have behavior types roughly speaking, sets whose elements can change through time—as its objects. An amazing fact about toposes2 is that they come with an internal language that looks very much like the usual formal language of mathematics itself. Thus one can define graphs, groups, topological spaces, etc. in any topos. But in BT, what we call graphs will actually be graphs that change through time, and similarly what we call groups and spaces will actually be groups and spaces that change through time.

The topos BT not only has an internal language, but also a mathematical semantics using the notion of sheaves. Technically, a sheaf is a certain sort of functor, but one can imagine it as a space of possibilities, varying in a controlled way; in our case it will be a space of possible behaviors varying in a certain notion of time. Every property we prove in our logic of behavior types will have meaning in this category of sheaves.

When discussing systems and components—such as sensors, controllers, motors, etc.—we mentioned behavior types; these will be the objects in the topos BT. Every wire in the picture below will stand for a behavior type, and every box X will stand for a behavioral property, a relation that X maintains between the changing values on its ports.

For example we could imagine that

• S (wire): The behavior of S over a time-interval [a, b] is that of all continuous real-valued functions [a, b] → \(\mathbb{R}\).

• A (wire): The behavior of A over a time-interval [a, b] is all piecewise constant functions, taking values in the finite set such as {go, stop}.

• controller (box): the relation {(S′, A) | Eq. (7.2)}, i.e. all behavioral pairs (S′, A) that conform to what we said our controller is supposed to do in Eq. (7.2).