Executable Interval Temporal Logic Specifications

TL;DR

This paper explores the reversibility of executable Interval Temporal Logic (ITL) specifications, focusing on how the reflection operator can be used to reverse system behaviors at various abstraction levels.

Contribution

It formalizes the executability of ITL specifications and investigates the use of the reflection operator to reverse behaviors, enhancing understanding of system reversibility.

Findings

Formalization of executable ITL specifications

Analysis of the reflection operator for reversing behaviors

Insights into reversibility at different abstraction levels

Abstract

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.