Temporal Landscapes: A Graphical Logic of Behavior
Brendan Fong (Topos Institute), Alberto Speranzon (Honeywell, Aerospace), David I. Spivak (Topos Institute & MIT LIDS)

TL;DR
This paper introduces a novel temporal logic based on temporal type theory that reasons about behaviors over time using temporal landscapes, providing a new perspective on reasoning about autonomous agents.
Contribution
It presents a new logical framework that models truth as temporal landscapes, enabling reasoning about behaviors over durations rather than static truth values.
Findings
Demonstrates the logic's application to autonomous agents
Provides examples illustrating reasoning about temporal behaviors
Introduces a new approach to temporal reasoning in logic
Abstract
We present an elementary introduction to a new logic for reasoning about behaviors that occur over time. This logic is based on temporal type theory. The syntax of the logic is similar to the usual first-order logic; what differs is the notion of truth value. Instead of reasoning about whether formulas are true or false, our logic reasons about temporal landscapes. A temporal landscape may be thought of as representing the set of durations over which a statement is true. To help understand the practical implications of this approach, we give a wide variety of examples where this logic is used to reason about autonomous agents.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsInnovation Diffusion and Forecasting · Data Visualization and Analytics · Complex Systems and Decision Making
\NewEnviron
scaletikzpicturetowidth[1]\pgfmathparse#1/\BODY
Temporal Landscapes: A Graphical Logic of Behavior††thanks: B. Fong and D.I. Spivak were supported by AFOSR grant FA9550–17–1–0058.
Brendan Fong Email: [email protected] InstituteHoneywell AerospaceTopos Institute & MIT, LIDS
Alberto Speranzon Email: [email protected] AerospaceTopos Institute & MIT, LIDS
David I. Spivak Email:[email protected] Institute & MIT, LIDS
Abstract
We present an elementary introduction to a new logic for reasoning about behaviors that occur over time. This logic is based on temporal type theory. The syntax of the logic is similar to the usual first-order logic; what differs is the notion of truth value. Instead of reasoning about whether formulas are true or false, our logic reasons about temporal landscapes. A temporal landscape may be thought of as representing the set of durations over which a statement is true. To help understand the practical implications of this approach, we give a wide variety of examples where this logic is used to reason about autonomous agents.
1 Introduction
Logical formalization of temporal considerations has a long and rich history, though the first modern treatment is probably the tense logic of Prior [Pri67], which has yielded what is now known simply as temporal logic. In temporal logic, as in any logical system, one has a syntactic way of building new formulas from simpler ones, say using conjunction and negation (), as well as a notion of model whose purpose is to specify the truth value of each such formula.
Temporal logic gets its expressive power from various operators, which collect information about other times into the current time. For example, in linear temporal logic (LTL), one considers the binary until operator . At time , one may ask whether will hold until holds, denoted , which more precisely means that there exists such that and for all . One can understand all such operators as given by some sort of quantification over , replacing each formula, e.g. , by a predicate in one variable. Restricting first-order logic by requiring that all atomic predicate symbols take only one variable, one obtains what is known as first-order monadic logic, and adding the 2-ary predicate , one obtains what is known as the first order monadic logic of order, . It was shown by Kamp [Kam68] that temporal logic with the until operator, together with its past-tense cousin since, is precisely as expressive as . Various additions and restrictions have been proposed over the years, in attempts to co-optimize between expressivity and computability.
A completely different approach to temporal reasoning, known as temporal type theory (TTT), was given in [SS19]. Instead of defining new logical operators that collate past and future times into the present, temporal type theory alters the very notion of truth itself, to make truth inherently depend on time. The goal of this article is to describe, in elementary terms, how TTT makes this idea precise, as well as how it can be used in practice.
Temporal type theory begins by defining a topological space called the interval domain , whose points are the closed intervals , which we call time-intervals, and whose open sets are generated by open intervals , each of which consists of all points with . A sheaf on is a type of behavior: it assigns to each basic open a set , and for every , it assigns a restriction function that clips a longer-lasting behavior to a shorter-lasting behavior . Behavior types include:
, , , and , the behaviors of natural numbers, integers, rationals, and reals (unchanging over any interval ); 2. 2.
, the behavior of “varying” real numbers (changing continuously over any );111Note that the constant reals can be considered as a subtype of the varying real numbers. 3. 3.
for any vector field on a topological space, the behavior of integral curves through (of duration ); 4. 4.
for any graph , the behavior of stochastically-timed walks through ; 5. 5.
more generally, for any hybrid system [Hen00], the behavior of all legal trajectories; 6. 6.
, the behavior of truth values, also known as propositions, which one can think of as audits or monitors of behavior. will be the main character in this paper; 7. 7.
the empty behavior and the singleton behavior ( itself), as well as products, unions, subobjects, quotients, and exponentials of all the above.
Discussing behavior types in detail is out of scope for this paper, as it includes definitions of sheaves and toposes; the interested reader is referred to [SS19] for a technical discussion, or to [FS19, Chapter 7] for a gentle introduction. The goal in this paper is to give the reader a relatively self-contained understanding of —the behavior type of truth values—in terms of temporal landscapes.
We will also not give a detailed comparison between the expressive power of various temporal logics, such as Metric Interval Temporal Logic (MITL) [AFH96] or Signal Temporal Logic (STL) [MN04], with that of temporal type theory. The main difference is simply that temporal type theory is a type theory, meaning that it can combine and reason about various types of behaviors, as exemplified above. Another is that temporal logic assumes a kind of omniscience about the future: the truth value of a proposition at time can contain information about what occurs over a whole interval . TTT does not have this omniscience: a proposition whose truth value depends on more than one moment—such as “whenever occurs at time , must occur before time ”—is only falsifiable on long-enough intervals, e.g. those containing . The aggregated truth value of a proposition over all intervals is its temporal landscape; information about what occurs over an interval is “stored” over the interval itself, not at its left endpoint. However, LTL and MITL do embed as a fragment of TTT [SS19, Chapter 8.6], so proofs from these logics are valid in TTT.
Our focus will be on the descriptive power of temporal type theory: through increasingly complex examples we shall demonstrate how TTT—in particular temporal landscapes—can be used to accurately model the relevant time-varying phenomena. We hope that this will be enough to give the reader a basic understanding of these ideas, even if translating them into reasoning power holds few subtleties.
Luckily, the base language of TTT is standard higher-order logic, which is quite similar to first-order logic. Not only should reasoning in TTT thus be more familiar to users with a grounding in predicate logic, a wide variety of proof assistants, including HOL, Lean, and Coq, can hence be easily adapted to provide formal verification of reasoning in TTT [CH88, Mou+15, NPW02].
We will begin in Section 2 by defining temporal landscapes. In Section 3 we discuss logical operations on temporal landscape and in Section 4 we give several increasingly expressive examples of temporal landscapes in the context of autonomous agents. Conclusions are provided in Section 5.
2 Definition of temporal landscape
Temporal landscapes provide the truth values of a logical system, which we call temporal landscape logic. Truth values may be thought of as acceptable answers to “yes/no”-style questions. For example, in standard propositional logic, the truth values are simply and . In propositional logic then, the question “Is it raining?” may be answered with “yes” () or “no” (). In temporal landscape logic, the answer to this question is a temporal landscape indicating precisely those time intervals during which it is raining. Let us be a bit more precise.
Let be the real numbers, thought of as representing points in time. Given two times with , we write for the set of all times between and ; we call this a time interval. Graphically, we may represent a time interval by a point above the diagonal in the plane , see Fig. 1a.
A temporal landscape is a set of time intervals with two special properties. The first is known as down-closure: if a time interval is in the temporal landscape, and is contained in , then is in the temporal landscape too. This property makes the assumption that if an assertion holds throughout a time interval, then it holds on all subintervals. For example, if it is raining throughout the time interval from 9:00 to 13:00, then it is also raining throughout the time interval from 10:00 to 10:45. In pictures, this means that a temporal landscape must be closed under both moving right and moving downward, as shown in Fig. 1a.
The second property of temporal landscapes is an openness (sometimes called a roundedness) property: if an assertion holds on some , then there exists some larger interval, with both and . This larger interval may only be infinitesimally larger, but it must be strictly larger on both sides. In pictures, we illustrate this as in Fig. 1b.The above is summarized in Definition 2.1.
Definition 2.1**.**
A temporal landscape on is a set of time intervals , , such that
- (a)
if , and , then . 2. (b)
if then there exists such that .
We write for the set of temporal landscapes.
Together, requirements (a) and (b) state that temporal landscapes form the open sets of the Scott topology on the interval domain , a well-studied topological space in domain theory [Gie+03]. While we will not need any topos or sheaf theory here, we remark that sheaves on form a topos, whose subobject classifier consists precisely of temporal landscapes; this topos is the subject of [SS19].
Remark 2.2*.*
By definition—Definition 2.1(b)—a temporal landscape does not include its boundary: it is an open set in . Hence in our examples so far, Figs. 1a and 1b, we have drawn them using a dotted line. From now on we use the visually simpler convention of drawing them with a solid line.
The simplest temporal landscape is that of a roof; this form the basis for the topology on .
Definition 2.3**.**
Given a pair in , the roof over is the temporal landscape
[TABLE]
Given any pair of real numbers , a temporal landscape on is a temporal landscape that is a subset of .
General temporal landscapes are curves that remain above the diagonal line and whose slope is piecewise continuous and remains in the interval . Note that rotating by , the slope condition becomes precisely the statement that the curve must be what is known as a 1-Lipschitz function.
3 Temporal landscape logic
Temporal landscapes form the truth values of a logical system. More precisely, temporal landscapes form the elements of what is known as a Heyting algebra. This means that standard logical constants and operations, such as , , AND (), OR () and implication (), have interpretations as temporal landscapes and operations on them.
To begin, we introduce the temporal landscapes and . The temporal landscape contains all time intervals . This landscape is the maximal one that visually can be depicted as a infinite triangle over the time line. On the other hand, the temporal landscape contains no time intervals at all: and it is the minimal landscape.
Given temporal landscapes and , their conjunction is given by their intersection, and their disjunction is given by their union. For an explicit example of conjunction, see Fig. 4 on page 4. In that example, the temporal landscape on the right is the conjunction—that is, the intersection—of the temporal landscapes and on the left and center.
It is straightforward to check that the results of these operations are again temporal landscapes, and that obey the usual properties of (constructive) first-order logic; for example, for any temporal landscape , we have .
Defining an implication that obeys the usual properties is a bit more subtle. Given temporal landscapes and , we define the temporal landscape
[TABLE]
To become acquainted with implication in general, we start with a special case, namely that of negation.
The negation operator is given by . Equivalently, since is the empty set, we may write
[TABLE]
The visual intuition of the implication generalizes that of negation, replacing the empty landscape with . The temporal landscape of contains a roof over all time intervals within which is contained in , as shown in Fig. 2.222In the following, we will often restrict ourselves to temporal landscapes on some arbitrary bounded interval, typically starting at 0, just for typographical convenience. In the example shown in Fig. 2, the landscape might appear having a confusing shape. The interpretation of such a landscape is that the predicate is only true over intervals of length at most three, the union of which is the solid line of height 3 above the axis.
Now that we have defined the logical connectives, we move on to the quantifiers and . The simplest case is when these quantifiers range over a constant type , which we may think of simply as a set.333In temporal type theory we can also quantify over non-constant behavior types, e.g. , but this is a bit more technical. Since such quantification appears only in a single subsection (e.g. in Eq. 4), we simply refer the reader to [SS19] for a definition. Given a set , a function is a collection of -many temporal landscapes. Taking their union defines the temporal landscape , which will be a temporal landscape. Taking their intersection may not satisfy condition (b) of Definition 2.1, so we define to be the largest temporal landscape contained in this intersection.
Throughout this document, the reader will see the connectives , and the quantifiers and . In each case, they refer to the operations on landscapes defined above.
4 Predicates over grid worlds
In this section we give increasingly expressive examples of how to use temporal landscapes to describe the behavior of an agent moving in various types of environments. We start with a fairly standard model, used in the Artificial Intelligence (AI) literature, to describe motions of an agent over a discretized space.
In a non-temporal situation, it is typical to represent an environment as a two- (or higher-)dimensional regular grid where each region of the space is a cell and cells overlap only on specified boundaries. Mathematically it is convenient to model this with an undirected graph , where is a set of vertices, associated to subdivisions (or cells) of the environment, and is the set of edges representing the fact that it is possible to move from one subdivision to another.
As we are working temporally, we replace sets with behavior types, which may be thought of as time-varying sets. More precisely, a behavior type specifies, for every temporal landscape, a set of behaviors that could take place over those durations. These sets of behaviors are required to obey a certain compatibility condition, so that for example behaviors over long time intervals restrict to behaviors on shorter subintervals.
4.1 Modelling the environment: constant and non-constant behavior types
Static environments. To simplify matters, let us first consider the case in which the environment does not vary in time. For this, we use constant behavior types: given a set , the constant behavior type on , by abuse of notation written again simply as , is the behavior type that for every temporal landscape simply specifies as its set of possible behaviors.
Suppose we want to say that our environment is modelled by the graph , and that it does not change over time. To do this, we simply take and construct its constant behavior type , and take as the constant subtype of consisting precisely of the pairs in the set . The constancy of the subtype says that the adjacency relation does not change: and either are adjacent or are not adjacent, independently of time.
To describe this fact logically in temporal type theory (TTT), we may write the formula
[TABLE]
That said, in higher order logics like TTT, one typically exchanges subobjects for predicates, e.g. replacing with .444Recall that is the set of temporal landscapes; see Definition 2.1. Then the statement would read
[TABLE]
If we impose axiom Eq. 1 then for any , the landscape for is either the always-true landscape , or the always-false landscape , depending on whether we want an edge or not. In this case we would say that forms a constant graph.
Dynamic environments. It is also interesting, however, to decline to require that our environment obey axiom Eq. 1, and thus model environments in which the adjacency of cells changes over time. This makes sense in the autonomous setting if we imagine that sometimes a door is blocked or a secret passage is opened.
That said, for most situations, including all that follow, it is good enough to use a model of the environment where adjacency is symmetric: if is connected to , then is connected to . Using the language of TTT, this means our environment obeys the axiom
[TABLE]
It will also be convenient to work with the function given by currying . It sends a cell to the (time-varying) set of cells adjacent to . For our example, we want to consider the notion of neighbor, by which we mean an adjacent cell, not including the cell itself. For each , its neighbors are the subtype of defined by the formula
[TABLE]
It is worth noticing, once more, that we can interpret in terms of temporal landscapes, by considering . This means that is a truth value—i.e. a temporal landscape—that describes when a given is a neighbor of . Of course, if we assume that is a constant graph, again will either be the landscape or the landscape, depending on whether and are neighbors.
Working with TTT feels much like predicate logic and set theoretic constructions. In contrast with temporal logic, where one must get used to working with new logical operators such as ‘until’ and ‘since’. For those who are trained in these languages, TTT provides a more easy to read language for reasoning about time. However, it is also true that TTT, being an intuitionistic logic, does introduce some “complexities”, as the law of excluded middle (or equivalently, double negation elimination) needs not to hold. Temporal landscapes provide a graphical interpretation that helps reason about temporal logic statement and mitigate some of these complexities.
4.2 Free/occupied cells: the negation operator
We now expand our example by adding a predicate . This predicate will be assumed to model the idea of a cell being occupied: for each cell , it specifies the set of time intervals over which is occupied. We will see that this predicate can capture situations that are more interesting than “mere occupancy”, and that temporal landscapes provides a formal language to express such scenarios.
If a cell is not occupied, we will say that it is free. We further define ; for each , the landscape is the set of time intervals over which is free. As mentioned in Section 3, double negation is not a trivial operation (the logic is constructive rather than Boolean). The predicate gives a good example of why this might be useful, i.e. why it makes sense that need not hold.
Suppose we have agents , , and , and predicates , , and , which map a cell to the temporal landscape of intervals over which the respective agent is in . Suppose that we wish to define to be the predicate describing the intervals over which at least one of the agents , , and is in . Note that this is slightly ambiguous in English, but we will see that the negation operator in TTT allows us to easily distinguish between the two readings of this sentence as and .
To do this, define to be the disjunction of these three predicates. For each , specifies the time intervals over which a single agent, whether it be , , or , remains in the cell throughout. Then specifies the time intervals over which there is always at least one agent in , but agents are allowed to come and go.
More concretely, fix some cell and suppose that an agent is in throughout the interval , an agent is in throughout , and another agent is in throughout . Then the temporal landscapes for , for , and for are shown on the left, middle, and right, of Fig. 3.
While the middle and right-hand diagram fit the usual interpretation of “when” the room is free/occupied, they are derived from the left-hand diagram, which is more expressive.
In particular, note that on the left-hand side diagram we have that does not contain the time interval , because this point falls in between the two roofs corresponding to and occupying the cell. This might appear strange, since there is at least one agent in the cell throughout , and thus we might expect to contain this interval. However, expresses the more refined idea of those intervals over which there exists any specific agent occupying : agent occupies on the interval and occupies on the interval ; is the disjunction of , and .
As an example of where the extra expressivity of might be important, consider a simple situation where an emergency light is placed within the cell and where two consecutive “blinks” of the light would represent a dangerous situation. In the case the light is ON at and again at , the temporal landscape for would correctly capture the fact that such an alarm would be missed as there is not a single agent in the cell at those instances. Thus, unless and communicate about the status of the light, the notification of danger would be completely missed. Such communication—and memory / recall in general—amounts to a strategy for persistently encoding intervallic facts into the present state.
4.3 Objects in a room: quantifiers
In this subsection we use TTT to describe when neighbors of a cell are free (unoccupied), despite possibly moving obstacles. We will consider two scenarios, both depicted in Fig. 4a.
This might be important, for example, for an autonomous vehicle, where one might want to know when it is immediately adjacent to an obstacle, and hence should be wary of a collision. In these scenarios the large black dots each represent an obstacle. In the first scenario the objects are stationary; in the second, they move in the direction shown by the arrow.
To begin, note that we can extend a predicate over any subtype as follows:555Note that is (constructively) equivalent to .
[TABLE]
This predicate describes the intervals over which all are free. In particular, we will be interested in for a cell , which tells us when every neighbor of is free, or equivalently, when none of ’s neighbors is occupied.
Static objects. Assume that the objects, represented by the two large black dots, are static (i.e. forget the arrows in Fig. 4a for now). Consider the cell indicated in Fig. 4a. In the case that the black objects are static, one sees that the predicate is the always-true landscape , since the configuration of “free” cells does not change over time. In particular, if we were to draw the temporal landscapes for each , each one would be the always-true landscape, and so their conjunction.
Dynamic objects. Next we consider a situation in which the black dots represent moving objects. In this scenario, the two objects move in the indicated directions (one downwards and the other leftwards) at a rate of one cell per unit time. When they reach a cell adjacent to the boundary of the domain, they remain there forever after.
In this case there is an equality of predicates ; both correspond to the always-true landscape, because these two cells are never occupied by either of the moving obstacles. For the predicate , however we note that the cell will be occupied for one time unit, between 3 and 4. Thus the cell is free for the interval , and of course for any subinterval of it, such as . The cell is also free for any interval , as long as ; the temporal landscape is shown in Fig. 4b. Similar reasoning applied to yields the temporal landscape shown in Fig. 4c.
The temporal landscape for is the conjunction of these temporal landscapes, i.e. all of ’s neighbors must be free, as shown in Fig. 4d. As described in Section 3 the resulting temporal landscape is going to be the “minimum” landscape—red boldface in Fig. 4d—of the four landscapes shown with dashed lines and in black, in green, and in blue.
Looking at the red landscape on the right of Fig. 4 we immediately see that the neighborhood of , namely , is not free in the interval .
4.4 Max dwell time in a room: implication
Let denote the type of agents’ IDs and let denote the predicate that an agent is at a vertex . We also define a room to be a subset of vertices, .666Note that we have not said and are constant over time: agents might come into service or be decommissioned, and rooms might be constructed, demolished, or expanded over time. Then for an agent , one may write to denote the proposition , namely the agent is in the room . The situation is shown in Fig. 5a, where we indicate an agent by a blue dot and shade in lighter blue the cells forming a room .
The wall—cells that are always occupied—are depicted in gray. Arrows depict possible trajectories that agent can take to move within the room and then exit.
Suppose we want to express the proposition that an agent stays in a room for at most units of time before it must exit the room. To model this, for some , we can use the predicate
[TABLE]
which says that given an agent , as long as ’s position remains in room , there is some start time such that the clock remains between and .
Let us consider an example. Let and suppose the agent is not in the room during the intervals and , but is in the room during and . The landscapes for the left and right hand side of (3), namely and respectively, are shown in blue and red in Fig. 5b.
Note the temporal landscape of the right hand side of (3) (red), it is an “always true” capped at 3 time units. This is because given a time there always exists a real value with , and such predicate is true for intervals of length .
The temporal landscape for the entire predicate (3), is shown in Fig. 5c. Note that in the interval [0,10] it is always true that the agent is within the room for at most 3 time units, however in [7,15] it is never true that the agent is within the room for at most 3 time units. Indeed, all we can say is that on intervals of length at most 3, the agent is clearly is in the room for at most 3 time units, however this is not true for longer time intervals.
4.5 Regions and occupancy
Let us now consider a modified grid world, where instead of constructing a uniform spatial partitioning of the environment we leverage what we, as humans, would argue is a reasonable “semantic” subdivision of the space. Take for example a building, such a partitioning would be based on more abstract concepts than cells, such as “rooms”, “corridors”, “foyers” etc. To ground the discussion, consider the scenario depicted in Fig. 6a. This picture depicts an agent (shown with a red dot) traversing a continuous environment, following a trajectory shown by a dashed line. The environment has been semantically subdivided into different regions (rooms).
In order to model the agent moving through the building, we begin by saying what a trajectory is. We normalize the building to be the square . Then define the set of all possible time-parametrized trajectories through the building to be:
[TABLE]
For example, in Fig. 6a, we depict a time-parametrized trajectory over an interval ), where , , , etc. making the distance traveled per unit time non-uniform along the trajectory.
It is worth noticing that in earlier examples, we considered a discretized space, whereas now we are considering a continuous space , and behaviors defined over such space.
As in the discrete case, suppose we are given a predicate that models the subset of (possibly changing in time) in which the agent cannot be. For example in Figure 6a we show some gray regions, which are intended to be walls, and hence always occupied/non-traversable. Thus if is in a wall, we put . Again as in the discrete case, we use this to define a predicate , by .
The agent is moving through the building, but to be more realistic we could imagine that the agent occupies space larger than a point, and that different parts of the agent move at slightly different speeds. Hence the agent consists of several different trajectories, all of which are close to one another, say within a distance of . We define using the Euclidean norm . We also put an upper bound on the speed of the agent, say , and define the agent’s possible positions as the following behavior type:
[TABLE]
Here the bound is the temporal landscape consisting of those intervals over which holds for all . For more on derivatives in temporal type theory, see [SS19, Section 7.3].
Let us consider the constant type representing the rooms as shown in Figure 6a. Suppose we have a predicate , indicating the landscape on which a trajectory stays within a room. As before, for any moving agent with trajectories , let us denote with the predicate , which says that agent is in a room if all of the trajectories that make up are in .
The temporal landscape for the proposition for when a single agent is in a room is a roof. Thus the temporal landscape of is obtained by taking the union—namely the max—of these roofs as shown in Fig. 6b.
Note that because of the agent footprint there are intervals where the agent can be in two rooms and since the agent is always in some room and thus is the always-true landscape.
4.6 Landmarks and maps: “slanted” temporal landscapes
So far, for most of the examples—except for that in Fig. 5—all the temporal landscapes have consisted of a finite union of roofs. One thus wonders when a “slanted” temporal landscape would be relevant in an application and what it would represent.
Consider the scenario as shown in Fig. 7a. An agent (red dot) travels, at constant velocity, within an indoor environment along the red dashed path. The agent is equipped with a range limited sensor, such as a LIDAR (blue disk) which emits a set of discrete laser beams. For each laser beam the LIDAR gets a return whenever a laser beam hits a surface. The measurement is the (possibly noisy) location of the surface along each beam (blue dots). We have denoted with (1) and (2) two specific locations along the path. We depict with small blue dots a possible set of sensor measurements—samples—along walls and columns (black rectangles).
Further suppose that the agent is equipped with a fixed amount of onboard memory, so that not all the samples can be stored. When the buffer used to store samples is full, past samples will be deleted to make space for new ones. Identify each sample with an integer and define the predicate that will be true over as long as the sample is in the memory of the agent.
The temporal landscape for is clearly a roof over the interval where is the instance when the sample was first stored in memory and is the instance when it was overwritten by a new sample (for then there is enough memory so that no overwriting occurs).
The following predicate will have a “slanted” temporal landscape
[TABLE]
For example, it might look like the temporal landscape in Fig. 7b. Initially, in the corridor, the number of samples is high and the memory will be fully allocated. As new samples are obtained, old ones will be overwritten. Assuming a constant velocity and number of samples per unit of time, we have a constant overwriting so that a sample is in memory only over a constant size interval: thus the landscape will be parallel to the time line. As the agent enters a part of the environment that has fewer surfaces, the number of samples per unit time decreases, and thus samples will persist in memory over longer and longer periods of time, especially given that the environment becomes sparser as the agent moves left to right. Once the agent starts sensing the beginning of the right-most corridor, the number of samples starts to quickly increase, the persistence of a sample in memory decreases and the maximum persistence in the onboard memory is reached (the landscape is parallel to the time line again).
It is worth mentioning that an idea related to temporal landscapes has been applied to other problems in robotics and in particular to monitor and diagnose perception systems [ASC21]. In this context, the concept of temporal diagnostic graphs was introduced.
5 Conclusion
In this paper, we have attempted to give an intuitive introduction to the logic of temporal type theory in terms of temporal landscapes. On the one hand, these are just collections of time intervals over which a proposition may be true. On the other, they can be drawn as Lipschitz functions and hence visualized. They form a logical system, where all of the connectives and quantifiers are defined by operations on these Lipschitz functions.
After introducing these landscapes, we discussed a series of examples from the domain of autonomous agents. These became fairly complex, e.g. considering an agent’s position not just as a point but as a collection of points, each moving with bounded speed, avoiding possibly moving obstacles, and storing recent LIDAR measurements in a small-capacity memory that is constantly being overwritten. These examples point to the great expressivity of temporal type theory.
In practice, TTT can serve as a sort of big tent, where calculations from model checkers or ODE solvers can be embedded. While infinite in nature, we explained how temporal landscapes can be finitely approximated. We thus hope to have shown how TTT can be used to specify and guide algorithmic developments in autonomous systems and any modeling environment in which time is an issue.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[AFH 96] Rajeev Alur, Tomás Feder and Thomas A. Henzinger “The benefits of relaxing punctuality” In Journal of the ACM (JACM) 43.1 ACM, 1996, pp. 116–146 DOI: 10.1145/3828.3837 · doi ↗
- 2[ASC 21] Pasquale Antonante, David I. Spivak and Luca Carlone “Monitoring and Diagnosability of Perception Systems”, 2021 URL: https://arxiv.org/pdf/2011.07010.pdf
- 3[CH 88] Thierry Coquand and Gérard Huet “The calculus of constructions” In Information and Computation 76.2-3 , 1988, pp. 95–120 DOI: 10.1016/0890-5401(88)90005-3 · doi ↗
- 4[FS 19] Brendan Fong and David I. Spivak “An Invitation to Applied Category Theory: Seven Sketches in Compositionality” Cambridge University Press, 2019 DOI: 10.1017/9781108668804 · doi ↗
- 5[Gie+03] G. Gierz et al. “Continuous lattices and domains” 93 , Encyclopedia of Mathematics and its Applications Cambridge University Press, 2003, pp. xxxvi+591 DOI: 10.1017/CBO 9780511542725 · doi ↗
- 6[Hen 00] Thomas A Henzinger “The theory of hybrid automata” In Verification of Digital and Hybrid Systems Springer, 2000, pp. 265–292 DOI: 10.1007/B Fb 0032003 · doi ↗
- 7[Kam 68] Johan Anthony Wilem Kamp “Tense logic and the theory of linear order”, 1968
- 8[MN 04] Odet Maler and Dejan Nickovic “Monitoring temporal properties of continuous signals.” In FORMATS , 2004, pp. 152–166
