  In this paper the reversibility of executable Interval Temporal Logic (ITL)
specifications is investigated. ITL allows for the reasoning about systems in
terms of behaviours which are represented as non-empty sequences of states. It
allows for the specification of systems at different levels of abstraction. At
a high level this specification is in terms of properties, for instance safety
and liveness properties. At concrete level one can specify a system in terms of
programming constructs. One can execute these concrete specification, i.e.,
test and simulate the behaviour of the system. In this paper we will formalise
this notion of executability of ITL specifications. ITL also has a reflection
operator which allows for the reasoning about reversed behaviours. We will
investigate the reversibility of executable ITL specifications, i.e., how one
can use this reflection operator to reverse the concrete behaviour of a
particular system.
