Temporal logic via recursion, part III
Nov. 1st, 2012 09:00 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
chaourcehttp://chaource.livejournal.com/84914.html Part I
http://chaource.livejournal.com/85196.html Part II
Temporal logic can express properties such that "x must become true when y first becomes true" or "x stays true until y first becomes false". To even come up with such properties, we used intuition or guessing. It would be useful to derive the list of all the different temporal logic operations we can use.
There are some relationships between logic operations. Ordinary Boolean logic has relations like (a+b)' = a'b', so the "and" operation can be expressed through "not" and "or". Knowing these relations, we can transform or simplify Boolean expressions.
Similarly, there are relationships between temporal operations. Some of these we have seen: ALL(x') = NOT SOME(x); ALL(x) = x ⊵ TRUE. It would be useful to have a small set of temporal operations from which all others can be expressed, and to determine the relationships between temporal operations. Our goal is to be able to perform calculations in temporal logic as effectively as in Boolean logic.
In all texts about temporal logic I've seen so far, these questions are not considered. Instead one postulates a fixed, small set of temporal operations. Some authors use "strict UNTIL", others "weak UNTIL". I would like to get to the bottom of it.
Update: what I am trying to develop here is known in the research literature as "fixpoint linear temporal logic". Rigorous definitions are in [Banieqbal, Barringer: Temporal logic with fixed points. 1989. Springer lecture notes in computer science, volume 398. Pages 62-74.]
Let us begin by considering unary operations. A unary temporal operation F is defined through a recursive formula,
F x := φ(x, NEXT(F x))
How many different operations can we define in this way? The sense of the recursion can be positive and negative, and the function φ(x,f) can be chosen arbitrarily. There are 16 such Boolean functions &phi(x,f), and so we have a choice of not more than 32 different unary operations F.
Of course, not all φ(x,f) will yield a valid definition of an operation F. At the very least, the function φ(x,f) must depend on both x and f in a nontrivial way, so φ(x,f)=x or φ(x,f)=f or φ(x,f)=0 are not to be considered.
Another constraint is that the Boolean equation f = φ(x,f) must have solutions for all x. This is formally expressed as the condition ∀x ∃f : f = φ(x,f), or equivalently
∀ x : φ(x,1)+ φ'(x,0).
Let us solve this constraint explicitly. Any Boolean function φ(x,f) can be written as
φ(x,f) = a(x) f' + b(x) f,
where a(x) and b(x) are some Boolean functions. (These functions are determined as a(x) := φ(x,0) and b(x) := φ(x,1). )
Using this formula, we compute
φ(x,1)+ φ'(x,0) = b(x) + a'(x).
So the constraint is ∀ x : b(x) + a'(x). Thus, b(x) + a'(x) ≡ 1. Therefore we can multiply any term by b(x) + a'(x). In particular, a = a(b+a') = ab + aa' = ab. So we get
φ(x,f) = a(x) f' + b(x) f = a(b + a') f' + b f
= abf'+bf = b(af'+f) = b(a+f) = ab + bf = a + bf.
(Recall that in Boolean logic a=a+ab because a+ab=a(1+b)=1a=a and a+a'b=a+b because a+a'b=(a+ab)+a'b=a+(a+a')b=a+1b=a+b.)
It follows that φ(x,f) can be simplified to a formula that does not explicitly contain f'. Now we have the formula
φ(x,f) = a(x) + b(x)f,
where a(x) and b(x) satisfy a'(x)+b(x)=1 for all x.
The condition that φ(x,f) essentially depends on both x and f excludes the choices b(x)≡0, a(x)≡1, and a(x)≡b(x). (If a≡b then a+bf=a+af=a does not depend on f.) Also, if we chooise a(x) and b(x) in some way, then a+bf = a+af+bf=a+(a+b)f, so the choice of a(x)+b(x) instead of a(x) leads to the same φ(x,f). The following possibilities remain:
a(x)≡0:
φ(x,f) = xf; φ(x,f) = x'f;
a(x)=x:
φ(x,f) = x + f
a(x)=x':
φ(x,f) = x' + f
The choice of x' or x does not add to our freedom; we can always substitute x' instead of x into the operation F; so we are left only with two choices: φ(x,f)=xf and φ(x,f)=x+f. These are the defining functions for the temporal operations ALL and SOME.
Finally, there is a choice of optimistic and pessimistic recursion. As we have noted before, any operation F x defined through the optimistic recursion is dual to NOT (F (NOT x)), which is defined through pessimistic recursion. The duality transformation takes φ(x,f) into φ'(x',f'). It is easy to see that the duality brings ALL into SOME and vice versa. Therefore, we are left only with two different unary operations, ALL and SOME, and the duality relationship between them. All other unary operations F are either trivial (always equal to TRUE or FALSE) or equivalent to ALL x, ALL x', SOME x, or SOME x'.
So far we have seen relationships such as (ALL x)' = SOME x'. Are there other relationships? For example, can we simplify ALL x + ALL(xy) + SOME(y') or other such temporal expressions?
An example: consider the formulas
F1 x := ALL x + SOME x
F2 x := ALL x + SOME x'
Can we simplify them by a straightforward calculation? What are the techniques of calculation that we need for this?
Using the recursive definitions of ALL and SOME, we compute
F1 x = x NEXT(ALL x) + x + NEXT(SOME x) = x + NEXT(SOME x)
F2 x = x NEXT(ALL x) + x' + NEXT(SOME x') = x' + NEXT(ALL x + SOME x') = x' + NEXT(F2 x').
It appears that F1 x = SOME x and F2 x = SOME x'. However, the recursive definitions alone are only necessary conditions, they are insufficient for determining the operations F1 and F2 unambiguously. For that, we need to determine the "mood" of the recursion.
Let us introduce the notation N- and N+ for the operators NEXT that came into our equations from in pessimistic and optimistic recursions respectively. With this notation, we write the recursive definitions like this,
F1 x = x N+(ALL x) + x + N-(SOME x) = x + NEXT-(SOME x)
F2 x = x N+(ALL x) + x' + N-(SOME x') = x' + N+(ALL x) + N-(SOME x').
In the case of F1, we can conclude that indeed F1 x = SOME x. But the calculation of F2 x stumbles on the problem of combining the two NEXT operators having different moods.
Here we can use the following rules of calculation:
N+(A) + N-(B) = N+(A+B) (optimism + pessimism = optimism)
N+(A) N-(B) = N-(AB) (optimism * pessimism = pessimism)
In principle, we would need a general proof that these rules yield correct definitions. I only give a heuristic argument: an optimistic property holds in the infinite future, an "or" operation does not change this fact. A pessimistic property fails to hold in the infinite future, so an "and" operation makes the entire property also fail in the infinite future.
Thus we obtain:
F2 x = x' + N+(SOME x').
The optimistic mood for SOME yields an identical truth; hence F2 x = TRUE regardless of x. In other words, ALL x + SOME x' = TRUE.
Exercise: a) Prove that SOME(x)+SOME(y) = SOME(x+y) and that ALL(x)ALL(y)=ALL(xy). b) Is it true that SOME(x)SOME(y) = SOME(xy)?
Solution:
a) The recursive definition for F(x,y) := SOME(x) + SOME(y) is
F(x,y) = x + N-(SOME x) + y + N-(SOME y) = x+y + N-(SOME x + SOME y) = x+y + F(x,y).
The mood is pessimistic, thus F(x,y) = SOME(x+y).
In the same way (or by duality) we prove the second statement.
b) Trying to make a recursive definition for SOME(x)SOME(y), we fail:
SOME(x)SOME(y) = (x + N-(SOME x))(y + N-(SOME y)) = xy + x N-(SOME y) + y N-(SOME x) + N-(SOME(x)SOME(y))
There is no closed-form recursion for SOME(x)SOME(y). So we try to find a counterexample, and sure enough, if x = {1,0,0,...} and y = {0,1,0,...}, then SOME(x)SOME(y)={1,0,...} while SOME(xy)=FALSE.
Exercise: Simplify the temporal expression ALL x + ALL(xy) + SOME(y').
Solution:
It is not true in general that ALL(a)+ALL(b)=ALL(a+b). However, in this case ALL(x)+ALL(xy)=ALL(x)+ALL(x)ALL(y)=ALL(x). Therefore
ALL x + ALL(xy) + SOME(y') = ALL x + SOME(y').
Considering now the more interesting case of binary operations, we again start with the same premise: a binary operation, x G y, is defined through a recursive formula
x G y = ψ(x,y, NEXT(x G y))
The Boolean function ψ(x,y,f) must satisfy two requirements: it should essentially depend on x,y,f and it should admit solutions of f = ψ(x,y,f), for all x,y.
We again write ψ(x,y,f) = a(x,y)f'+b(x,y)f and derive the constraint ∀x,y: a'(x,y)+b(x,y)≡1. It again follows that ψ(x,y,f) can be written in the form where f' does not appear,
ψ(x,y,f) = a(x,y) + b(x,y)f.
Each choice of a(x,y) and b(x,y) is admissible as long as the constraint ∀x,y: a'(x,y)+b(x,y)≡1 holds. Now it remains to see which choices of a(x,y) and b(x,y) yield different and independent operations G.
In the case of unary operations, we could simply list all possible functions. Now we have 16 possible choices of a(x,y) and independently 16 possible choices of b(x,y). Instead of trying to list all possibilities, let us use a more economical approach.
We can first observe that a(x,y)≡0 does not bring us a new operation: the recursion x G y = b(x,y) NEXT(x G y) is the same as ALL(b(x,y)). Similarly, b(x,y)≡1 can be omitted from our search.
If G1 and G2 are two binary operations defined through functions
ψ1(x,y,f) = a1(x,y) + b1(x,y)f,
ψ2(x,y,f) = a2(x,y) + b2(x,y)f,
what do we obtain if we write "x G1 y + x G2 y"? Will this be another binary operation of the same kind?
The recursion relation for "x G1 y + x G2 y" is
x G1 y + x G2 y = a1(x,y) + b1(x,y) NEXT(x G1 y) + a2(x,y) + b2(x,y) NEXT(x G2 y).
We can convert this into a recursion relation for the single new operation if, say, b1 = b2. In this case, let us say that the operations G1 and G2 are "compatible" with respect to logical "or". Suppose that this condition holds; then we have obtained a new operation with the equation
ψ(x,y,f) = a1(x,y) + a2(x,y) + b1 f.
[More generally, G1 and G2 are "or"-compatible if there is some Boolean function b(x,y) such that
∀ A,B : a1 + b1 A + a2 + b2 B ≡ a1 + b A + a2 + b B
This can happen only if ∀ x,y : a1 + a2 + b1 = a1 + a2 + b2. However, this consideration does not really appear to enlarge the set of "or"-compatible operations.]
Consider the set of all binary operations that are "or"-compatible with G. These binary operations are defined through equations with functions ψ(x,y,f) of the form
a1(x,y) + b f
a2(x,y) + b f
...
aN(x,y) + b f
Computing the logical "or" of two of these operations gives another of these operations. So we can choose four of them as the "basic" building blocks, for instance:
a1 = x'y'; a2 = xy'; a3 = x'y; a4 = xy
Any nonzero function a(x,y) can be obtained from these four by logical "or". For example, a(x,y)=y' is expressed as a = a1 + a2.
Consider now the logical "and" of two binary operations:
(x G1 y)(x G2 y) = (a1(x,y) + b1(x,y) NEXT(x G1 y))(a2(x,y) + b2(x,y) NEXT(x G2 y)).
If a1 = a2 = a, we call the operations G1 and G2 "and"-compatible. Then the recursion equation can be simplified to
(x G1 y)(x G2 y) = a(x,y) + b1(x,y) b2(x,y) NEXT((x G1 y)(x G2 y)).
In other words, by combining two "and"-compatible operations we get the logical "and" of their "b" functions. Again we can consider the set of all operations that are "and"-compatible with a given operation G. These operations are defined through functions ψ(x,y,f) of the form
a(x,y) + b1(x,y) f
...
a(x,y) + bN(x,y) f
We can choose four functions
b1 = x+y, b2 = x'+y, b3 = x+y', b4 = x'+y'
as "building blocks" from which any function b(x,y), not identically equal to 1, can be obtained by logical "and". For example, b(x,y)=x is expressed as b = b1 b3.
Let us define by G_{ij} the binary operation defined through the building blocks a_i and b_j, for i,j between 1 and 4. Thus, for instance, the binary operation G23 is defined by
x G21 y = a2(x,y) + b1(x,y) NEXT(x G21 y) = xy' + (x+y) NEXT(x G21 y).
Therefore, we get the following picture. All admissible binary operations G are defined through recursive equations of the form
x G y = a(x,y) + b(x,y) NEXT(x G y),
where the Boolean functions a(x,y) and b(x,y) are expressed through the "building blocks" in some way. Accordingly, the operation G is expressed through "and"/"or" and the basic binary operations G_{ij}. For example, in order to express the operation
x ⊵ y := y' + x NEXT(x ⊵ y)
we need to select a(x,y)=y'=a1+a2 and b(x,y)=x = b1 b3. Therefore we can express x ⊵ y as
x ⊵ y = (x G11 y + x G21 y)(x G13 y + x G23 y).
It remains to see which of the sixteen "basic operations" G_{ij} are nontrivial and independent. The constraint a'+b=1 must hold in each case; this eliminates the operations G11, G22, G33, and G44. To reduce further the number of different operations, we can use the symmetries with respect to exchanging x and y, and also with respect to exchanging x with x', and y with y'.
Exchanging x and y is equivalent to exchanging a2 with a3, as well as b2 with b3. For instance, compare the operations G12 and G13; they are defined by
x G12 y = a1(x,y) + b2(x,y) NEXT(x G12 y) = x'y' + (x'+y) NEXT(x G12 y)
x G13 y = a1(x,y) + b3(x,y) NEXT(x G12 y) = x'y' + (x+y') NEXT(x G13 y)
It is evident that x G12 y = y G13 x. Similarly, x G42 y = y G43 x; also, x G23 y = y G32 x.
Exchanging x with x' is equivalent to exchanging the indices 1 with 2 and 3 with 4. Let us, for instance, compare
x G13 y = x'y' + (x+y') NEXT(x G13 y)
x G24 y = xy' + (x'+y') NEXT(x G24 y)
It is evident that x G13 y = x' G24 y. Similarly, x G14 y = x' G23 y; x G12 y = x' G21 y; and so on.
We also have x G14 y = x' G41 y' and x G23 y = x' G32 y'. Both x/x' and y/y' were exchanged here.
Finally, only the following two operations remain independent:
x G41 y = xy + (x+y) NEXT(x G41 y) (generates G14, G23, G32)
x G21 y = xy' + (x+y) NEXT(x G21 y) (generates G12, G13, G24, G31, G34, G42, G43)
We also note that each of the operations is, in principle, available in both moods (optimistic and pessimistic). The resulting temporal operations are different.
Thus, we conclude that only four independent binary operations are sufficient to describe all binary operations in (this kind of) temporal logic.
Exercise: Interpret these four operations.
Solution: Consider the operation G41: it evaluates to true at the current time if x=y=1 at the current time; or else x=1 or y=1, and the condition is repeated at the next time. We can describe the condition in words like this: "at least one of x and y remains true until the first time when x and y both become true".
The mood of the recursion remains yet undetermined. If we choose the optimistic mood, we assume that the condition is true "in the infinitely far future". Thus, at least one of x and y remains true "in the infinite future", and we do not require that x and y ever both become true. If we choose the pessimistic mood, we require that x and y both actually become true at some time (at the present time or in the future). The two conditions obtained with the two mood choices are different and both nontrivial.
Now consider x G21 y. The recursive definition can be simplified to
x G21 y = xy' + (xy+xy'+y) NEXT(x G21 y) = xy' + (xy+y) NEXT(x G21 y) = xy' + y NEXT(x G21 y).
This operation evaluates to true at the current time if xy' = 1 at the current time, or else if y is true and the condition holds at the next time. As long as y stays true, we postpone the decision and wait. Once y becomes false, x must be true at the same time. We can describe this operation as "x is true when y first becomes false". If the recursion is chosen to be optimistic, we do not require that y ever actually becomes false; otherwise we do. Again, both mood choices yield different and nontrivial temporal conditions.
http://chaource.livejournal.com/85196.html Part II
Temporal logic can express properties such that "x must become true when y first becomes true" or "x stays true until y first becomes false". To even come up with such properties, we used intuition or guessing. It would be useful to derive the list of all the different temporal logic operations we can use.
There are some relationships between logic operations. Ordinary Boolean logic has relations like (a+b)' = a'b', so the "and" operation can be expressed through "not" and "or". Knowing these relations, we can transform or simplify Boolean expressions.
Similarly, there are relationships between temporal operations. Some of these we have seen: ALL(x') = NOT SOME(x); ALL(x) = x ⊵ TRUE. It would be useful to have a small set of temporal operations from which all others can be expressed, and to determine the relationships between temporal operations. Our goal is to be able to perform calculations in temporal logic as effectively as in Boolean logic.
In all texts about temporal logic I've seen so far, these questions are not considered. Instead one postulates a fixed, small set of temporal operations. Some authors use "strict UNTIL", others "weak UNTIL". I would like to get to the bottom of it.
Update: what I am trying to develop here is known in the research literature as "fixpoint linear temporal logic". Rigorous definitions are in [Banieqbal, Barringer: Temporal logic with fixed points. 1989. Springer lecture notes in computer science, volume 398. Pages 62-74.]
Unary operations
Let us begin by considering unary operations. A unary temporal operation F is defined through a recursive formula,
F x := φ(x, NEXT(F x))
How many different operations can we define in this way? The sense of the recursion can be positive and negative, and the function φ(x,f) can be chosen arbitrarily. There are 16 such Boolean functions &phi(x,f), and so we have a choice of not more than 32 different unary operations F.
Of course, not all φ(x,f) will yield a valid definition of an operation F. At the very least, the function φ(x,f) must depend on both x and f in a nontrivial way, so φ(x,f)=x or φ(x,f)=f or φ(x,f)=0 are not to be considered.
Another constraint is that the Boolean equation f = φ(x,f) must have solutions for all x. This is formally expressed as the condition ∀x ∃f : f = φ(x,f), or equivalently
∀ x : φ(x,1)+ φ'(x,0).
Let us solve this constraint explicitly. Any Boolean function φ(x,f) can be written as
φ(x,f) = a(x) f' + b(x) f,
where a(x) and b(x) are some Boolean functions. (These functions are determined as a(x) := φ(x,0) and b(x) := φ(x,1). )
Using this formula, we compute
φ(x,1)+ φ'(x,0) = b(x) + a'(x).
So the constraint is ∀ x : b(x) + a'(x). Thus, b(x) + a'(x) ≡ 1. Therefore we can multiply any term by b(x) + a'(x). In particular, a = a(b+a') = ab + aa' = ab. So we get
φ(x,f) = a(x) f' + b(x) f = a(b + a') f' + b f
= abf'+bf = b(af'+f) = b(a+f) = ab + bf = a + bf.
(Recall that in Boolean logic a=a+ab because a+ab=a(1+b)=1a=a and a+a'b=a+b because a+a'b=(a+ab)+a'b=a+(a+a')b=a+1b=a+b.)
It follows that φ(x,f) can be simplified to a formula that does not explicitly contain f'. Now we have the formula
φ(x,f) = a(x) + b(x)f,
where a(x) and b(x) satisfy a'(x)+b(x)=1 for all x.
The condition that φ(x,f) essentially depends on both x and f excludes the choices b(x)≡0, a(x)≡1, and a(x)≡b(x). (If a≡b then a+bf=a+af=a does not depend on f.) Also, if we chooise a(x) and b(x) in some way, then a+bf = a+af+bf=a+(a+b)f, so the choice of a(x)+b(x) instead of a(x) leads to the same φ(x,f). The following possibilities remain:
a(x)≡0:
φ(x,f) = xf; φ(x,f) = x'f;
a(x)=x:
φ(x,f) = x + f
a(x)=x':
φ(x,f) = x' + f
The choice of x' or x does not add to our freedom; we can always substitute x' instead of x into the operation F; so we are left only with two choices: φ(x,f)=xf and φ(x,f)=x+f. These are the defining functions for the temporal operations ALL and SOME.
Finally, there is a choice of optimistic and pessimistic recursion. As we have noted before, any operation F x defined through the optimistic recursion is dual to NOT (F (NOT x)), which is defined through pessimistic recursion. The duality transformation takes φ(x,f) into φ'(x',f'). It is easy to see that the duality brings ALL into SOME and vice versa. Therefore, we are left only with two different unary operations, ALL and SOME, and the duality relationship between them. All other unary operations F are either trivial (always equal to TRUE or FALSE) or equivalent to ALL x, ALL x', SOME x, or SOME x'.
Algebraic relationships
So far we have seen relationships such as (ALL x)' = SOME x'. Are there other relationships? For example, can we simplify ALL x + ALL(xy) + SOME(y') or other such temporal expressions?
An example: consider the formulas
F1 x := ALL x + SOME x
F2 x := ALL x + SOME x'
Can we simplify them by a straightforward calculation? What are the techniques of calculation that we need for this?
Using the recursive definitions of ALL and SOME, we compute
F1 x = x NEXT(ALL x) + x + NEXT(SOME x) = x + NEXT(SOME x)
F2 x = x NEXT(ALL x) + x' + NEXT(SOME x') = x' + NEXT(ALL x + SOME x') = x' + NEXT(F2 x').
It appears that F1 x = SOME x and F2 x = SOME x'. However, the recursive definitions alone are only necessary conditions, they are insufficient for determining the operations F1 and F2 unambiguously. For that, we need to determine the "mood" of the recursion.
Let us introduce the notation N- and N+ for the operators NEXT that came into our equations from in pessimistic and optimistic recursions respectively. With this notation, we write the recursive definitions like this,
F1 x = x N+(ALL x) + x + N-(SOME x) = x + NEXT-(SOME x)
F2 x = x N+(ALL x) + x' + N-(SOME x') = x' + N+(ALL x) + N-(SOME x').
In the case of F1, we can conclude that indeed F1 x = SOME x. But the calculation of F2 x stumbles on the problem of combining the two NEXT operators having different moods.
Here we can use the following rules of calculation:
N+(A) + N-(B) = N+(A+B) (optimism + pessimism = optimism)
N+(A) N-(B) = N-(AB) (optimism * pessimism = pessimism)
In principle, we would need a general proof that these rules yield correct definitions. I only give a heuristic argument: an optimistic property holds in the infinite future, an "or" operation does not change this fact. A pessimistic property fails to hold in the infinite future, so an "and" operation makes the entire property also fail in the infinite future.
Thus we obtain:
F2 x = x' + N+(SOME x').
The optimistic mood for SOME yields an identical truth; hence F2 x = TRUE regardless of x. In other words, ALL x + SOME x' = TRUE.
Exercise: a) Prove that SOME(x)+SOME(y) = SOME(x+y) and that ALL(x)ALL(y)=ALL(xy). b) Is it true that SOME(x)SOME(y) = SOME(xy)?
Solution:
a) The recursive definition for F(x,y) := SOME(x) + SOME(y) is
F(x,y) = x + N-(SOME x) + y + N-(SOME y) = x+y + N-(SOME x + SOME y) = x+y + F(x,y).
The mood is pessimistic, thus F(x,y) = SOME(x+y).
In the same way (or by duality) we prove the second statement.
b) Trying to make a recursive definition for SOME(x)SOME(y), we fail:
SOME(x)SOME(y) = (x + N-(SOME x))(y + N-(SOME y)) = xy + x N-(SOME y) + y N-(SOME x) + N-(SOME(x)SOME(y))
There is no closed-form recursion for SOME(x)SOME(y). So we try to find a counterexample, and sure enough, if x = {1,0,0,...} and y = {0,1,0,...}, then SOME(x)SOME(y)={1,0,...} while SOME(xy)=FALSE.
Exercise: Simplify the temporal expression ALL x + ALL(xy) + SOME(y').
Solution:
It is not true in general that ALL(a)+ALL(b)=ALL(a+b). However, in this case ALL(x)+ALL(xy)=ALL(x)+ALL(x)ALL(y)=ALL(x). Therefore
ALL x + ALL(xy) + SOME(y') = ALL x + SOME(y').
Binary operations
Considering now the more interesting case of binary operations, we again start with the same premise: a binary operation, x G y, is defined through a recursive formula
x G y = ψ(x,y, NEXT(x G y))
The Boolean function ψ(x,y,f) must satisfy two requirements: it should essentially depend on x,y,f and it should admit solutions of f = ψ(x,y,f), for all x,y.
We again write ψ(x,y,f) = a(x,y)f'+b(x,y)f and derive the constraint ∀x,y: a'(x,y)+b(x,y)≡1. It again follows that ψ(x,y,f) can be written in the form where f' does not appear,
ψ(x,y,f) = a(x,y) + b(x,y)f.
Each choice of a(x,y) and b(x,y) is admissible as long as the constraint ∀x,y: a'(x,y)+b(x,y)≡1 holds. Now it remains to see which choices of a(x,y) and b(x,y) yield different and independent operations G.
In the case of unary operations, we could simply list all possible functions. Now we have 16 possible choices of a(x,y) and independently 16 possible choices of b(x,y). Instead of trying to list all possibilities, let us use a more economical approach.
We can first observe that a(x,y)≡0 does not bring us a new operation: the recursion x G y = b(x,y) NEXT(x G y) is the same as ALL(b(x,y)). Similarly, b(x,y)≡1 can be omitted from our search.
If G1 and G2 are two binary operations defined through functions
ψ1(x,y,f) = a1(x,y) + b1(x,y)f,
ψ2(x,y,f) = a2(x,y) + b2(x,y)f,
what do we obtain if we write "x G1 y + x G2 y"? Will this be another binary operation of the same kind?
The recursion relation for "x G1 y + x G2 y" is
x G1 y + x G2 y = a1(x,y) + b1(x,y) NEXT(x G1 y) + a2(x,y) + b2(x,y) NEXT(x G2 y).
We can convert this into a recursion relation for the single new operation if, say, b1 = b2. In this case, let us say that the operations G1 and G2 are "compatible" with respect to logical "or". Suppose that this condition holds; then we have obtained a new operation with the equation
ψ(x,y,f) = a1(x,y) + a2(x,y) + b1 f.
[More generally, G1 and G2 are "or"-compatible if there is some Boolean function b(x,y) such that
∀ A,B : a1 + b1 A + a2 + b2 B ≡ a1 + b A + a2 + b B
This can happen only if ∀ x,y : a1 + a2 + b1 = a1 + a2 + b2. However, this consideration does not really appear to enlarge the set of "or"-compatible operations.]
Consider the set of all binary operations that are "or"-compatible with G. These binary operations are defined through equations with functions ψ(x,y,f) of the form
a1(x,y) + b f
a2(x,y) + b f
...
aN(x,y) + b f
Computing the logical "or" of two of these operations gives another of these operations. So we can choose four of them as the "basic" building blocks, for instance:
a1 = x'y'; a2 = xy'; a3 = x'y; a4 = xy
Any nonzero function a(x,y) can be obtained from these four by logical "or". For example, a(x,y)=y' is expressed as a = a1 + a2.
Consider now the logical "and" of two binary operations:
(x G1 y)(x G2 y) = (a1(x,y) + b1(x,y) NEXT(x G1 y))(a2(x,y) + b2(x,y) NEXT(x G2 y)).
If a1 = a2 = a, we call the operations G1 and G2 "and"-compatible. Then the recursion equation can be simplified to
(x G1 y)(x G2 y) = a(x,y) + b1(x,y) b2(x,y) NEXT((x G1 y)(x G2 y)).
In other words, by combining two "and"-compatible operations we get the logical "and" of their "b" functions. Again we can consider the set of all operations that are "and"-compatible with a given operation G. These operations are defined through functions ψ(x,y,f) of the form
a(x,y) + b1(x,y) f
...
a(x,y) + bN(x,y) f
We can choose four functions
b1 = x+y, b2 = x'+y, b3 = x+y', b4 = x'+y'
as "building blocks" from which any function b(x,y), not identically equal to 1, can be obtained by logical "and". For example, b(x,y)=x is expressed as b = b1 b3.
Let us define by G_{ij} the binary operation defined through the building blocks a_i and b_j, for i,j between 1 and 4. Thus, for instance, the binary operation G23 is defined by
x G21 y = a2(x,y) + b1(x,y) NEXT(x G21 y) = xy' + (x+y) NEXT(x G21 y).
Therefore, we get the following picture. All admissible binary operations G are defined through recursive equations of the form
x G y = a(x,y) + b(x,y) NEXT(x G y),
where the Boolean functions a(x,y) and b(x,y) are expressed through the "building blocks" in some way. Accordingly, the operation G is expressed through "and"/"or" and the basic binary operations G_{ij}. For example, in order to express the operation
x ⊵ y := y' + x NEXT(x ⊵ y)
we need to select a(x,y)=y'=a1+a2 and b(x,y)=x = b1 b3. Therefore we can express x ⊵ y as
x ⊵ y = (x G11 y + x G21 y)(x G13 y + x G23 y).
It remains to see which of the sixteen "basic operations" G_{ij} are nontrivial and independent. The constraint a'+b=1 must hold in each case; this eliminates the operations G11, G22, G33, and G44. To reduce further the number of different operations, we can use the symmetries with respect to exchanging x and y, and also with respect to exchanging x with x', and y with y'.
Exchanging x and y is equivalent to exchanging a2 with a3, as well as b2 with b3. For instance, compare the operations G12 and G13; they are defined by
x G12 y = a1(x,y) + b2(x,y) NEXT(x G12 y) = x'y' + (x'+y) NEXT(x G12 y)
x G13 y = a1(x,y) + b3(x,y) NEXT(x G12 y) = x'y' + (x+y') NEXT(x G13 y)
It is evident that x G12 y = y G13 x. Similarly, x G42 y = y G43 x; also, x G23 y = y G32 x.
Exchanging x with x' is equivalent to exchanging the indices 1 with 2 and 3 with 4. Let us, for instance, compare
x G13 y = x'y' + (x+y') NEXT(x G13 y)
x G24 y = xy' + (x'+y') NEXT(x G24 y)
It is evident that x G13 y = x' G24 y. Similarly, x G14 y = x' G23 y; x G12 y = x' G21 y; and so on.
We also have x G14 y = x' G41 y' and x G23 y = x' G32 y'. Both x/x' and y/y' were exchanged here.
Finally, only the following two operations remain independent:
x G41 y = xy + (x+y) NEXT(x G41 y) (generates G14, G23, G32)
x G21 y = xy' + (x+y) NEXT(x G21 y) (generates G12, G13, G24, G31, G34, G42, G43)
We also note that each of the operations is, in principle, available in both moods (optimistic and pessimistic). The resulting temporal operations are different.
Thus, we conclude that only four independent binary operations are sufficient to describe all binary operations in (this kind of) temporal logic.
Exercise: Interpret these four operations.
Solution: Consider the operation G41: it evaluates to true at the current time if x=y=1 at the current time; or else x=1 or y=1, and the condition is repeated at the next time. We can describe the condition in words like this: "at least one of x and y remains true until the first time when x and y both become true".
The mood of the recursion remains yet undetermined. If we choose the optimistic mood, we assume that the condition is true "in the infinitely far future". Thus, at least one of x and y remains true "in the infinite future", and we do not require that x and y ever both become true. If we choose the pessimistic mood, we require that x and y both actually become true at some time (at the present time or in the future). The two conditions obtained with the two mood choices are different and both nontrivial.
Now consider x G21 y. The recursive definition can be simplified to
x G21 y = xy' + (xy+xy'+y) NEXT(x G21 y) = xy' + (xy+y) NEXT(x G21 y) = xy' + y NEXT(x G21 y).
This operation evaluates to true at the current time if xy' = 1 at the current time, or else if y is true and the condition holds at the next time. As long as y stays true, we postpone the decision and wait. Once y becomes false, x must be true at the same time. We can describe this operation as "x is true when y first becomes false". If the recursion is chosen to be optimistic, we do not require that y ever actually becomes false; otherwise we do. Again, both mood choices yield different and nontrivial temporal conditions.
