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 …