Operational semantics of Framed Tempura

This paper investigates the operational semantics of temporal logic programs. To this end, a temporal logic programming language called Framed Tempura is employed. The evaluation rules for both the arithmetic and boolean expressions are defined. The semantic equivalence rules for the reduction of a program within a state is formalized. Furthermore, the transition rules within a state and transition rules over an interval between configurations are also specified. Moreover, some examples are given to illustrate how these rules work. Thus, the executable behavior of framed programs can be captured in an operational way. In addition, the consistency between the operational semantics and the minimal model semantics based on model theory is proved in detail.