Embedding CTL* in an Extension to Interval Temporal Logic (ITL)

In this paper we present an embedding of the most common branching time logics (CTL/CTL*) in an extension of interval temporal logic (ITL+). The significance of this result is threefold: first the theoretical aspect is, that branching time and linear time are not so much different. A more practical aspect is that the intuitive interactive proof method of symbolic execution of ITL+ can be used for branching time logics as well. The opposite direction is interesting as well, for a subset of finite state systems, interactive verification of ITL+ formulas can be translated into a model checking problem. The proof presented in this paper has been done with the interactive theorem prover KIV. So this contribution can also be seen as a case study on reasoning about temporal logics in an interactive verification environment.