Sometimes “Tomorrow” is “Sometime”

We address the hierarchical (vertical) decomposition, or abstract implementation, of object specification in temporal logic. Whereas previous approaches to refinement in the context of temporal logic such as those developed by Lamport and by Barringer, Kuiper and Pnueli are based on a single logic that accommodates different levels of action granularity, our approach is based on relating different logics corresponding to different levels of granularity. More precisely, we map abstract actions (propositions) to concrete objects (theories) and, through inference rules that relate the different logics, derive properties of the abstracted actions from the behaviour of the corresponding objects. In this way, we keep a tighter control of action granularity and interference, enabling us to maintain the use of the “next” operator and make the development of reactive systems more tractable.