In this paper we further develop the methodology of temporal logic as an executable imperative language, presented by Moszkowski [Mos86] and Gabbay [Gab87, Gab89] and present a concrete framework, called MetateM for executing (modal and) temporal logics. Our approach is illustrated by the development of an execution mechanism for a propositional temporal logic and for a restricted first order temporal logic. ∗ Work supported partially by Alvey under grants PRJ/SE/054 and IKBS/170 and by ESPRIT under Basic Research Action 3096 (SPEC). 1
Howard Barringer, Michael Fisher, Dov M. Gabbay, G