UNITY PROPERTIES AND SEQUENCES OF STATES, SOME OBSERVATIONS

We examine the expressive power of Unity properties in relation to exe cution sequences of Unity programs. One might expect that if two progr ams have the same unless and leadsto properties, then they have the sa me execution sequences. We show that this is not true. We examine whet her this difference vanishes if we adopt a stronger notion of fairness , or use unsures properties instead of leadsto properties (possibly ad opting a stronger fairness notion also). We show by a simple example t hat both approaches are not successful. Hence, properties are not expr essive enough to characterize execution sequences, and it is not clear what execution model corresponds to Unity properties. As a consequenc e, the notion of property preserving program refinement differs from t he notion of decreasing nondeterminism.