Temporal logic via recursion, part II
I talked about a recursion approach to temporal logic in part I. Temporal logic operates on infinite sequences of Boolean values and includes ordinary Boolean operations (AND, OR, NOT) as well as new, "temporal" operations. The only allowed "temporal" operations are those defined recursively, through an equation of the form
F x = φ(x, NEXT(F x))
where φ(x,f) is a Boolean formula.
For instance, the temporal operations ALL(x) and SOME(x) are defined recursively by
ALL x = x NEXT(ALL x)
SOME x = x + NEXT(SOME x) (*)
I am now using the notation "F x" instead of "F(x)" for temporal logic operations. Where needed for clarity, we will still use parentheses.
There is, however, an important deficiency of the recursive definitions: they cannot, by themselves, define temporal operations unambiguously.
A recursive definition "F = φ(x, NEXT F)" is usually understood as an "equation" for the unknown function F; due to the form of this equation, a solution F may be called a fixed point of the function φ(x, NEXT F). In any case, the solution of this equation is the function F we are defining. However, what if this equation has several solutions? Which of the solutions is the function F we are trying to define?
An example of this problem is shown already by the temporal operations ALL and SOME. Initially, we defined SOME(x) as the logical "or" of all values of the sequence x, starting from the current value. For instance, if x = {0, 0, 1, 0, 0, ...}, with all values 0 after time 3, then SOME(x) = {1, 1, 1, 0, 0, ...}. However, the recursive definition (*) admits a solution where SOME(x)=TRUE regardless of x:
TRUE = x + NEXT(TRUE) -- this is obviously an identity, for any Boolean sequence x.
Therefore, the recursive definition (*) by itself does not uniquely define the function SOME.
Similarly, the recursive definition for ALL(x) admits a solution when ALL(x)=FALSE for any x.
How can we fix this?
It might appear that the problem with ALL and SOME is contrived: the solution clearly should not be ALL(x)=FALSE for any x. No, the problem is not at all contrived. Actually, this problem is present in all of our examples so far!
For instance, we have previously defined the temporal operation ⊳ through the recursive equation
x ⊳ y = xy' + xy NEXT(x ⊳ y)).
Our intention was to make (x ⊳ y) true if x stays true strictly longer than y. Now we may ask: does x ⊳ y actually imply that y becomes false at a certain time in the future, while x remains true? What if x = y = TRUE = {1, 1, ...}, does x stay true "strictly longer than" y in this case? (What is TRUE ⊳ TRUE?)
It turns out that our recursive definition does not allow us to derive the value of (TRUE ⊳ TRUE). Indeed, if X = TRUE ⊳ TRUE then, by definition,
X = (TRUE AND NOT TRUE) OR (TRUE AND TRUE AND NEXT(X)) = NEXT(X).
So all we know is that X = NEXT(X), which allows two solutions, X = TRUE and X = FALSE. Thus, we cannot decide whether TRUE ⊳ TRUE = TRUE or TRUE ⊳ TRUE = FALSE, if all we know is the recursive definition of ⊳.
It seems there is a crucial piece of information missing from all our recursive definitions that we wrote so far. What is missing?
Let us first consider the simple question: if a temporal operation F is defined through
F x = φ(x,NEXT(F x)), (**)
NEXT(F x)=F(NEXT(x)), (***)
what are the values of F(TRUE) and F(FALSE)?
It is clear from (***) that these values must be again either TRUE or FALSE. Therefore, the temporal equation (**) is reduced to an ordinary, Boolean equation,
f = φ(x,f).
If f(x) is a (Boolean) solution of this equation then we have F(TRUE)=f(TRUE), F(FALSE)=f(FALSE). It remains to determine f(x) by solving this Boolean equation.
Incidentally, we can see that any temporal operation can be converted into an ordinary Boolean function by considering only the constant sequences TRUE and FALSE. This is sol because, in our temporal logic, all operations commute with NEXT, therefore the value of any temporal formula on the sequences TRUE or FALSE must be also either TRUE or FALSE.
In this way, we can convert a recursive definition of a temporal operation into a simple Boolean (non-temporal) equation. The value of the temporal operation on TRUE and FALSE can then be determined.
I talked here about solving Boolean equations, but I did not consider the question of how to distinguish between several solutions. The method of solution consisted of making sure that solutions exist, then assuming that the solution equals "true", and checking whether this assumption is correct.
For our equation, f = φ(x,f), this method amounts to setting f(x)=φ(x,1). This is certainly a solution (provided that the equation has solutions). It is clear that in this way we will always select a solution that prefers "true" over "false"; this is so because we first check whether f=1 is a solution, and choose f=0 only if f=1 does not work. If, for some x, both f=0 and f=1 are solutions, our method will select f=1. Let us therefore call this solution optimistic.
We can define the optimistic solution formally: f_opt(x) is optimistic if it has the value "true" at least as often as any other solution f(x), i.e. f(x) => f_opt(x) for all solutions f.
The "pessimistic" method consists of setting f(x) = φ(x,0). By the same reasoning, this solution will prefer "false" over "true" whenever possible.
The definitions of temporal operations ALL and SOME give rise to the Boolean equations
f(x) = x f(x)
and
f(x) = x + f(x)
All these equations have more than one solution at least for some choices of the parameters x,y. Thus, it makes sense to talk about optimistic and pessimistic solutions. The pessimistic solution to f = xf is f=0, while the optimistic one is f=x. This is exactly the same alternative as we had for the temporal operation ALL(x): either it is always FALSE, or it is the logical "and" of the elements of x. The optimistic solution to f = x+f is f=1, while the pessimistic one is f = x.
Consider the operation x ⊳ y. If we denote by f(x,y) the non-temporal version of this operation, we obtain the equation
f(x,y) = xy'+xy f(x,y)
The optimistic solution to this is f(x,y)=x; the pessimistic solution is f(x,y)=xy'. It follows that TRUE ⊳ TRUE = TRUE in the optimistic version but FALSE in the pessimistic version.
Is the choice between optimistic and pessimistic solutions exactly the missing piece of information we are looking for?
As we have seen, temporal logic involves recursive definitions of functions on infinite Boolean sequences, and these recursive definitions often have more than one solution. If there are are multiple solutions, we may select a single solution by specifying whether we are looking for the optimistic or the pessimistic solution.
We can define this formally: the optimistic solution is a temporal function F(x) such that (at any fixed time) it has the value "true" at least as often as any other solution F. (Introducing a partial order on temporal values and functions, we may say that the optimistic solution is the largest fixed point of the recursive equation.)
For instance, the "optimistic" fixed point of the recursive equation
F x = x NEXT(F x)
is precisely the operation ALL(x).
Let us modify the rules of temporal logic by introducing two different recursive definitions: optimistic and pessimistic. Thus, we now define temporal operations as
F x :=+ φ(x, NEXT(F x))
or
F x :=- φ(x, NEXT(F x))
showing explicitly whether we select the optimistic (+) or the pessimistic (-) fixed point. Now the recursive definitions are precise, because the optimistic or pessimistic fixed points are unique (when they exist).
I will call the choice of + or - the mood of the recursive definition.
For example, ALL(x) and SOME(x) are correctly defined by
ALL x :=+ x NEXT(ALL x)
SOME x :=- x + NEXT(SOME x)
Note that ALL(x') = NOT SOME(x); we can derive this consistently if we reverse the mood of the recursive definitions when we apply NOT.
If we write a definition for SOME incorrectly, i.e. using optimistic recursion,
F x :=+ x + NEXT(F x),
the result is that F(FALSE)=TRUE, and therefore F(x)=TRUE for all x. This is certainly not the desired meaning of SOME(x)! So it is incorrect to use the optimistic recursion when defining SOME(x).
Another example: we can define the operations ⊳+ and ⊳-, by using the same recursive equation as before, but with either optimistic or pessimistic mood of the recursion. The result is that x ⊳+ y is true if x remains true strictly longer than y, and also in the case when y never becomes false. On the other hand, x ⊳- y does require that y becomes false at some time. So we can get both kinds of operations by varying the mood of the recursion.
I found the following mnemonically helpful interpretation of pessimistic and optimistic recursion. We ask the question: Does the situation in the infinitely far future make our property hold or not? If we are optimistic, we assume that our property holds in the infinitely far future (i.e. after applying NEXT() infinitely many times). If we are pessimistic, we assume that our property does not hold in the infinitely far future.
Let me illustrate this heuristic idea by examples. An optimistic definition of SOME(x) means that SOME(x) is true in the "infinitely far future". So x is already true at "some" time, and x does not have to be true now or at any other particular time. For this reason, the optimistic definition of SOME(x) becomes identically true for all x. To define SOME correctly, we need to use the pessimistic recursion.
A pessimistic definition of ALL(x) means that ALL(x) is false in the infinitely far future. Since ALL(x) requires that x be true at all times, "including" the infinitely far future, we must conclude that ALL(x) is false, now and at all times, regardless of what x is doing. For this reason, a pessimistic definition of ALL yields (incorrectly) FALSE for all x. To define ALL correctly, we need to use the optimistic recursion.
When a temporal operation is defined through recursion, it is helpful to visualize what happens by expanding the recursion a few times. For example:
SOME x = x + NEXT(SOME x) = x + NEXT(x + NEXT(SOME x)) = ...
= x + NEXT(x) + NEXT2(x) + ... + NEXTn-1(x) + NEXTn(SOME x).
Thus, after expanding n levels of recursion, we get a formula with n nested levels of NEXT(). An optimistic recursion substitutes TRUE instead of the last level of NEXT, and then takes the limit of an infinite nesting of levels; a pessimistic recursion substitutes FALSE. Thus, an optimistic definition of SOME will insert a TRUE value at the n-th level of NEXT; but this makes the entire formula TRUE. A pessimistic definition of SOME will insert a FALSE value there, removing the last term; it is clear that this is indeed the desired definition of SOME.
Exercise: The UNTIL operation.
x UNTIL y means that x remains true as long as y remains false. For example, x UNTIL y is true for the sequences
x = {1, 1, ?, ... } (does not matter what x does at time t=3)
y = {0, 0, 1, ... } (y becomes true at time t=3)
The property x UNTIL y is false for the sequences
x = {0, 0, ...} (x is not true at t=1, before t=2)
y = {0, 1, ...} (y becomes true at t=2)
Also, the property x UNTIL y is true if y never becomes true. (It is not required that y ever becomes true.)
What is the correct recursive definition of x UNTIL y? Is it pessimistic or optimistic? What will happen with the other choice of eventuality?
Solution:
x UNTIL y :=+ y + x (x UNTIL y)
Here is how we can check this solution: In the optimistic mood, we assume that (x UNTIL y) holds in the infinitely far future. Suppose that y always remains false and x always remains true. Heuristically, we write
x UNTIL y = y + x AND (far future).
This formula evaluates to "true" since we are optimistic about the far future and since, by assumption, x = TRUE.
If we want to avoid heuristic thinking, let us denote f(x,y) the result of computing x UNTIL y where x,y are either TRUE or FALSE. We can then consider f to be a Boolean function. We obtain the Boolean equation for f,
f(x,y) = y + x f(x,y)
This equation has the optimistic solution f(x,y)=x+y and the pessimistic solution f(x,y)=y. It is clear that we want the optimistic solution, since x UNTIL y should return TRUE when x=TRUE, regardless of what y does.
Project for theoretical mathematicians: To prove that
(1) Temporal solutions F of the equations
∀ x:
F x=φ(x,NEXT (F x)),
NEXT(F x)=F(NEXT(x))
exist if and only if Boolean (non-temporal) solutions of f=φ(x,f) exist,
(2) If solutions exist, there are always exactly two solutions, one optimistic and one pessimistic, and this is so in the temporal case as well as in the non-temporal case.
F x = φ(x, NEXT(F x))
where φ(x,f) is a Boolean formula.
For instance, the temporal operations ALL(x) and SOME(x) are defined recursively by
ALL x = x NEXT(ALL x)
SOME x = x + NEXT(SOME x) (*)
I am now using the notation "F x" instead of "F(x)" for temporal logic operations. Where needed for clarity, we will still use parentheses.
Ambiguity of recursive definitions
There is, however, an important deficiency of the recursive definitions: they cannot, by themselves, define temporal operations unambiguously.
A recursive definition "F = φ(x, NEXT F)" is usually understood as an "equation" for the unknown function F; due to the form of this equation, a solution F may be called a fixed point of the function φ(x, NEXT F). In any case, the solution of this equation is the function F we are defining. However, what if this equation has several solutions? Which of the solutions is the function F we are trying to define?
An example of this problem is shown already by the temporal operations ALL and SOME. Initially, we defined SOME(x) as the logical "or" of all values of the sequence x, starting from the current value. For instance, if x = {0, 0, 1, 0, 0, ...}, with all values 0 after time 3, then SOME(x) = {1, 1, 1, 0, 0, ...}. However, the recursive definition (*) admits a solution where SOME(x)=TRUE regardless of x:
TRUE = x + NEXT(TRUE) -- this is obviously an identity, for any Boolean sequence x.
Therefore, the recursive definition (*) by itself does not uniquely define the function SOME.
Similarly, the recursive definition for ALL(x) admits a solution when ALL(x)=FALSE for any x.
How can we fix this?
It might appear that the problem with ALL and SOME is contrived: the solution clearly should not be ALL(x)=FALSE for any x. No, the problem is not at all contrived. Actually, this problem is present in all of our examples so far!
For instance, we have previously defined the temporal operation ⊳ through the recursive equation
x ⊳ y = xy' + xy NEXT(x ⊳ y)).
Our intention was to make (x ⊳ y) true if x stays true strictly longer than y. Now we may ask: does x ⊳ y actually imply that y becomes false at a certain time in the future, while x remains true? What if x = y = TRUE = {1, 1, ...}, does x stay true "strictly longer than" y in this case? (What is TRUE ⊳ TRUE?)
It turns out that our recursive definition does not allow us to derive the value of (TRUE ⊳ TRUE). Indeed, if X = TRUE ⊳ TRUE then, by definition,
X = (TRUE AND NOT TRUE) OR (TRUE AND TRUE AND NEXT(X)) = NEXT(X).
So all we know is that X = NEXT(X), which allows two solutions, X = TRUE and X = FALSE. Thus, we cannot decide whether TRUE ⊳ TRUE = TRUE or TRUE ⊳ TRUE = FALSE, if all we know is the recursive definition of ⊳.
It seems there is a crucial piece of information missing from all our recursive definitions that we wrote so far. What is missing?
Optimistic and pessimistic Boolean solutions
Let us first consider the simple question: if a temporal operation F is defined through
F x = φ(x,NEXT(F x)), (**)
NEXT(F x)=F(NEXT(x)), (***)
what are the values of F(TRUE) and F(FALSE)?
It is clear from (***) that these values must be again either TRUE or FALSE. Therefore, the temporal equation (**) is reduced to an ordinary, Boolean equation,
f = φ(x,f).
If f(x) is a (Boolean) solution of this equation then we have F(TRUE)=f(TRUE), F(FALSE)=f(FALSE). It remains to determine f(x) by solving this Boolean equation.
Incidentally, we can see that any temporal operation can be converted into an ordinary Boolean function by considering only the constant sequences TRUE and FALSE. This is sol because, in our temporal logic, all operations commute with NEXT, therefore the value of any temporal formula on the sequences TRUE or FALSE must be also either TRUE or FALSE.
In this way, we can convert a recursive definition of a temporal operation into a simple Boolean (non-temporal) equation. The value of the temporal operation on TRUE and FALSE can then be determined.
I talked here about solving Boolean equations, but I did not consider the question of how to distinguish between several solutions. The method of solution consisted of making sure that solutions exist, then assuming that the solution equals "true", and checking whether this assumption is correct.
For our equation, f = φ(x,f), this method amounts to setting f(x)=φ(x,1). This is certainly a solution (provided that the equation has solutions). It is clear that in this way we will always select a solution that prefers "true" over "false"; this is so because we first check whether f=1 is a solution, and choose f=0 only if f=1 does not work. If, for some x, both f=0 and f=1 are solutions, our method will select f=1. Let us therefore call this solution optimistic.
We can define the optimistic solution formally: f_opt(x) is optimistic if it has the value "true" at least as often as any other solution f(x), i.e. f(x) => f_opt(x) for all solutions f.
The "pessimistic" method consists of setting f(x) = φ(x,0). By the same reasoning, this solution will prefer "false" over "true" whenever possible.
The definitions of temporal operations ALL and SOME give rise to the Boolean equations
f(x) = x f(x)
and
f(x) = x + f(x)
All these equations have more than one solution at least for some choices of the parameters x,y. Thus, it makes sense to talk about optimistic and pessimistic solutions. The pessimistic solution to f = xf is f=0, while the optimistic one is f=x. This is exactly the same alternative as we had for the temporal operation ALL(x): either it is always FALSE, or it is the logical "and" of the elements of x. The optimistic solution to f = x+f is f=1, while the pessimistic one is f = x.
Consider the operation x ⊳ y. If we denote by f(x,y) the non-temporal version of this operation, we obtain the equation
f(x,y) = xy'+xy f(x,y)
The optimistic solution to this is f(x,y)=x; the pessimistic solution is f(x,y)=xy'. It follows that TRUE ⊳ TRUE = TRUE in the optimistic version but FALSE in the pessimistic version.
Is the choice between optimistic and pessimistic solutions exactly the missing piece of information we are looking for?
Optimistic and pessimistic recursive definitions
As we have seen, temporal logic involves recursive definitions of functions on infinite Boolean sequences, and these recursive definitions often have more than one solution. If there are are multiple solutions, we may select a single solution by specifying whether we are looking for the optimistic or the pessimistic solution.
We can define this formally: the optimistic solution is a temporal function F(x) such that (at any fixed time) it has the value "true" at least as often as any other solution F. (Introducing a partial order on temporal values and functions, we may say that the optimistic solution is the largest fixed point of the recursive equation.)
For instance, the "optimistic" fixed point of the recursive equation
F x = x NEXT(F x)
is precisely the operation ALL(x).
Let us modify the rules of temporal logic by introducing two different recursive definitions: optimistic and pessimistic. Thus, we now define temporal operations as
F x :=+ φ(x, NEXT(F x))
or
F x :=- φ(x, NEXT(F x))
showing explicitly whether we select the optimistic (+) or the pessimistic (-) fixed point. Now the recursive definitions are precise, because the optimistic or pessimistic fixed points are unique (when they exist).
I will call the choice of + or - the mood of the recursive definition.
For example, ALL(x) and SOME(x) are correctly defined by
ALL x :=+ x NEXT(ALL x)
SOME x :=- x + NEXT(SOME x)
Note that ALL(x') = NOT SOME(x); we can derive this consistently if we reverse the mood of the recursive definitions when we apply NOT.
If we write a definition for SOME incorrectly, i.e. using optimistic recursion,
F x :=+ x + NEXT(F x),
the result is that F(FALSE)=TRUE, and therefore F(x)=TRUE for all x. This is certainly not the desired meaning of SOME(x)! So it is incorrect to use the optimistic recursion when defining SOME(x).
Another example: we can define the operations ⊳+ and ⊳-, by using the same recursive equation as before, but with either optimistic or pessimistic mood of the recursion. The result is that x ⊳+ y is true if x remains true strictly longer than y, and also in the case when y never becomes false. On the other hand, x ⊳- y does require that y becomes false at some time. So we can get both kinds of operations by varying the mood of the recursion.
I found the following mnemonically helpful interpretation of pessimistic and optimistic recursion. We ask the question: Does the situation in the infinitely far future make our property hold or not? If we are optimistic, we assume that our property holds in the infinitely far future (i.e. after applying NEXT() infinitely many times). If we are pessimistic, we assume that our property does not hold in the infinitely far future.
Let me illustrate this heuristic idea by examples. An optimistic definition of SOME(x) means that SOME(x) is true in the "infinitely far future". So x is already true at "some" time, and x does not have to be true now or at any other particular time. For this reason, the optimistic definition of SOME(x) becomes identically true for all x. To define SOME correctly, we need to use the pessimistic recursion.
A pessimistic definition of ALL(x) means that ALL(x) is false in the infinitely far future. Since ALL(x) requires that x be true at all times, "including" the infinitely far future, we must conclude that ALL(x) is false, now and at all times, regardless of what x is doing. For this reason, a pessimistic definition of ALL yields (incorrectly) FALSE for all x. To define ALL correctly, we need to use the optimistic recursion.
When a temporal operation is defined through recursion, it is helpful to visualize what happens by expanding the recursion a few times. For example:
SOME x = x + NEXT(SOME x) = x + NEXT(x + NEXT(SOME x)) = ...
= x + NEXT(x) + NEXT2(x) + ... + NEXTn-1(x) + NEXTn(SOME x).
Thus, after expanding n levels of recursion, we get a formula with n nested levels of NEXT(). An optimistic recursion substitutes TRUE instead of the last level of NEXT, and then takes the limit of an infinite nesting of levels; a pessimistic recursion substitutes FALSE. Thus, an optimistic definition of SOME will insert a TRUE value at the n-th level of NEXT; but this makes the entire formula TRUE. A pessimistic definition of SOME will insert a FALSE value there, removing the last term; it is clear that this is indeed the desired definition of SOME.
Exercise: The UNTIL operation.
x UNTIL y means that x remains true as long as y remains false. For example, x UNTIL y is true for the sequences
x = {1, 1, ?, ... } (does not matter what x does at time t=3)
y = {0, 0, 1, ... } (y becomes true at time t=3)
The property x UNTIL y is false for the sequences
x = {0, 0, ...} (x is not true at t=1, before t=2)
y = {0, 1, ...} (y becomes true at t=2)
Also, the property x UNTIL y is true if y never becomes true. (It is not required that y ever becomes true.)
What is the correct recursive definition of x UNTIL y? Is it pessimistic or optimistic? What will happen with the other choice of eventuality?
Solution:
x UNTIL y :=+ y + x (x UNTIL y)
Here is how we can check this solution: In the optimistic mood, we assume that (x UNTIL y) holds in the infinitely far future. Suppose that y always remains false and x always remains true. Heuristically, we write
x UNTIL y = y + x AND (far future).
This formula evaluates to "true" since we are optimistic about the far future and since, by assumption, x = TRUE.
If we want to avoid heuristic thinking, let us denote f(x,y) the result of computing x UNTIL y where x,y are either TRUE or FALSE. We can then consider f to be a Boolean function. We obtain the Boolean equation for f,
f(x,y) = y + x f(x,y)
This equation has the optimistic solution f(x,y)=x+y and the pessimistic solution f(x,y)=y. It is clear that we want the optimistic solution, since x UNTIL y should return TRUE when x=TRUE, regardless of what y does.
Project for theoretical mathematicians: To prove that
(1) Temporal solutions F of the equations
∀ x:
F x=φ(x,NEXT (F x)),
NEXT(F x)=F(NEXT(x))
exist if and only if Boolean (non-temporal) solutions of f=φ(x,f) exist,
(2) If solutions exist, there are always exactly two solutions, one optimistic and one pessimistic, and this is so in the temporal case as well as in the non-temporal case.
