A Challenge   (prizes to win!)

Mani Chandy and I wrote a paper, Theorems about Composition, that I presented at the Fifth International Conference on Mathematics of Program Construction (MPC'2000). At the end of my talk, I proposed a challenge to the audience (at that time, money was offered but, sorry, it's only for participants in the conference): Is there a weakest universal property stronger than the always (or henceforth) property of temporal logic and, if yes, is it the property we defined and called universal always?

The technical backgroung that underlies this question is very simple and fits on two slides. However, I found these questions surprisingly difficult and I have not been able to answer them. At some point, they were driving me crazy and I gave up. Maybe a different approach (or a smarter person) could solve the problem. Here is a self-contained description of it.

Transition Systems

We assume a single state type identical for all systems, namely, a tuple of variables of some kind. For each system, this tuple is partitioned between shared (i.e., writable by other systems) and local (i.e., non writable by other systems) variables.

In this context, a transition system is then defined by (we pay no attention to fairness issues here):

• a state predicate (a function from states to booleans), denoted by Init, that defines the possible initial states. This predicate is supposed to be satisfiable.
• a finite set of transitions (functions from states to states), denoted by S. This set is supposed to be nonempty and to contain at least the identity function.

Such a transition system defines a (nonempty, possibly infinite) set of infinite computations: start with an initial state that satisfies Init and apply successive transitions from S to get the next states. Formally, a computation C is an infinite sequence of states c₀, c₁, ... c_n, ... such that:

• Init.c₀
• (forall n :: (exists s in S :: c_n+1 = s.c_n))

Properties of Transition Systems

In this context, a property is a predicate on transition systems, defined either in terms of Init and S (strong properties) or in terms of infinite computations (weak properties). We are especially interested in four types of properties, parameterized by one or two state predicates:

• Strong next:
  p next_s q = (forall x :: (forall s in S :: p.x => q.(s.x)))

• Weak next:
  p next_w q = (forall C :: (forall n :: p.c_n => q.c_n+1))

• Always (a.k.a. henceforth, a.k.a. weak invariant, a.k.a. noninductive invariant):
  always p = [Init => p] /\ (p next_w p)

• Invariant (a.k.a. strong invariant, a.k.a. inductive invariant):
  invariant p = [Init => p] /\ (p next_s p)

Well-known relationships exist between these properties. Especially: p next_w q = (exists I :: (invariant I) /\ (p /\ I next_s q)).

Also, always properties correspond to the intuition of a predicate that is "always true": always p = (forall C :: (forall n :: p.c_n)).

Finally, strong properties are stronger than weak properties: [(p next_s q) => (p next_w q)] and [(invariant p) => (always p)].

It should be noted, though, that reverse implications do not hold, i.e., strong and weak properties are not equivalent. The reason is that strong properties must hold even for states x that are not reachable, while weak properties only take into account reachable states (cf the issue of UNITY's substitution axiom).

Composition

Transition systems can be composed only if the following two conditions are satisfied:

• The conjunction of their Init predicates is satisfiable.
• A system cannot modify variables that are declared local in another system, i.e., such variables v must satisfy v.x = v.(s.x) for all transitions s of the system and all states x.

When these conditions are satisfied, systems can be composed and the resulting system is defined by the conjunction of all Init predicates and the union of all sets S of transitions. (Any variable that is declared local is a subsystem is local in the system. We only consider compositions of a finite number of systems so that it is guaranteed that the resulting set of transitions is finite.)

Universal and Non Universal Properties

A property is said to be universal if and only if, when it holds in two systems, it holds in the system resulting from the composition of these two systems.

For instance, strong next and invariant properties are universal: if (p next_s q) is satisfied by two systems, it is also satisfied by the system resulting from their composition (same thing with (invariant p) properties).

However, weak next and always properties are not universal: it is possible that two systems satisfy (p next_w q) but their composition does not. This is because some states that are not reachable by a system in isolation may become reachable when the system is composed with other systems.

A Universal Next

(invariant p) is a universal property stronger than (always p) (which is not universal). In the same way, strong next properties are universal properties stronger than weak next. It is possible to define properties that are universal, stronger that weak next, but weaker than strong next. (See our papers for explanations of why we are interested in keeping properties weak.) For instance, the following property, called universal next is universal, stronger than weak next but weaker than strong next (of course, a universal always can be defined in the same way):

p next_u q = (exists I :: (invariant I) /\ (I local) /\ (p /\ I next_s q)).
where (I local) means that the truth value of I in any state can only be changed by modifying the value of a variable declared as local in the system under consideration. This locality constraint is the only difference between (p next_u q) and (p next_w q). Recall that:

p next_w q = (exists I :: (invariant I) /\ (p /\ I next_s q)).

The "locality" interpretation is used here to keep things simple and intuitive. An equivalent, more semantical interpretation can be used:

p next_u q = (exists I :: WE.(invariant I) /\ (p /\ I next_s q)).
where WE.X is the weakest property Y such that each time a component of a system satisfies Y, the system satisfies X (i.e., Y.F => (forall G :: X.F||G), forall F). Details about the predicate transformer WE can be found in papers.

To summarize, we have the following situation:

                                                 universal | non universal
                                                           |
                                                           |
-----+----------------------------------------------+------+------------+----->
 p nexts q                                      p nextu q  |        p nextw q
                                                           |

Challenging Questions

1. Is there a weakest universal property stronger than (p next_w q)?
2. If there is, what is it? Especially, is it (p next_u q)?

If anyone is interested in solving these two questions and has ideas on how to handle such a problem, I'm very interested in hearing from him or her. Feel free to contact me if you need more details or explanations about this problem. The first person who gives me a (correct and checkable) answer to (at least) one of these question wins ... my eternal esteem!

Michel Charpentier <>