MetateM: An introduction

In this paper a methodology for the use of temporal logic as an executable imperative language is introduced. The approach, which provides a concrete framework, called MetateM , for executing temporal formulae, is motivated and illustrated through examples. In addition, this introduction provides references to further, more detailed, work relating to the MetateM approach to executable logics.