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.
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):
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
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:
Well-known relationships exist between these properties.
Especially:
Also, always properties correspond to the intuition of a
predicate that is "always true":
Finally, strong properties are stronger than weak properties:
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).
Transition systems can be composed only if the following two conditions are satisfied:
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.)
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
However, weak next and always properties are
not universal: it is possible that two systems satisfy
(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):
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
The "locality" interpretation is used here to keep things simple and intuitive. An equivalent, more semantical interpretation can be used:
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.,
To summarize, we have the following situation:
universal | non universal | | -----+----------------------------------------------+------+------------+-----> p next_{s} q p next_{u} q | p next_{w} 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!