Reification - Changing Viewpoint but Preserving Truth

In this paper we investigate the technique of stepwise refinement used to facilitate and to structure the design process of complex software systems and to increase the productivity by reusing code, proofs, etc. Assuming an object- oriented approach to system specification, i.e., objects are understood as units of structure and behaviour, data refinement as well as action refinement have to be addressed. Our approach relies on temporal logics as a suitable framework to express system dynamics. Applying refinement techniques during the design process implies that a system is described as a sequence of specifications of different abstraction levels. This also incorporates the change of granularity. For instance, action refinement means that one can look at things from different points of view: what is atomic from the abstract point of view may be compound from the refined one. To emphasize this complex meaning of refinement we refer to it as reification. Major problems arise when temporal logics is combined with reification. This is due to the fact that temporal operators like ``tomorrow'' and ``yesterday'' (among others) assume a specific time scale where each action execution causes the transition to the following instance of time. Thus, a temporal formula expresses a specific viewpoint according to this time scale. In this paper we investigate the use of temporal operators in the presence of reification.