Execution of TILCO temporal logic specifications

Temporal logics are able to describe temporal constraints amongst events and actions, as invariance, precedence, periodicity, repeated occurrences, liveness and safety conditions. They are typically used to verify properties in the requirements analysis, in order to describe high level system behaviour and for test case generation. In some cases, temporal logics are used for the specification of real time systems and for their execution. In this paper a model and algorithm to execute specifications in TILCO first order temporal logic are presented. To this end, the TILCO specifications are translated into a model which can be directly, executed by a specific inference engine. An example is also presented.