1
00:00:00,180 --> 00:00:03,680
But I'm going to start off by explaining temporal logic.

2
00:00:05,640 --> 00:00:11,900
So you all know logic and or XOR and so on. I mean, I hope everyone in this room is familiar

3
00:00:11,900 --> 00:00:15,500
with those concepts. If you aren't, you should learn about them. They're pretty cool.

4
00:00:16,900 --> 00:00:23,640
And temporal logic adds some new operators to our logic to reason about time and order.

5
00:00:24,360 --> 00:00:29,880
We get operators like always and eventually and at the next step and until.

6
00:00:31,120 --> 00:00:33,800
And so with these operators, we can reason about.

7
00:00:34,800 --> 00:00:35,900
We did this thing.

8
00:00:37,180 --> 00:00:43,620
And after that thing, something is true forever. We did this thing. And at the next step,

9
00:00:43,900 --> 00:00:44,760
this thing is true.

10
00:00:45,900 --> 00:00:49,980
Then we also get these operators that can allow us to reason about the past, where we

11
00:00:49,980 --> 00:00:55,740
can say things like once and at the previous step and since and so on. These are the

12
00:00:55,740 --> 00:00:57,800
ones that we lean in heavily in Dogwood.

13
00:00:58,800 --> 00:01:05,020
And these operators, just like those logic operators, give us this really cool foundation

14
00:01:05,020 --> 00:01:10,280
for all kinds of programming logic. These temporal operators give us a firm mathematical

15
00:01:10,280 --> 00:01:13,960
foundation for expressing these time -based policies.