Applications of Interval-based Temporal Separation: the Reactivity Normal Form, Inverse $\Pi$, Craig Interpolation and Beth Definability

TL;DR

This paper demonstrates how interval-based temporal separation techniques can be used to derive normal forms, elimination of propositional quantification, and interpolation properties in an extended interval temporal logic, enhancing formal reasoning capabilities.

Contribution

It introduces a new normal form for interval temporal logic formulas and applies interval-based separation to achieve interpolation and Beth definability results.

Findings

Concise proofs of reactivity normal form for ITL.

Expressibility of inverse temporal projection operator.

Elimination of propositional quantification in ITL-NL.

Abstract

We show how interval-based temporal separation on the extension of Moszkowski's discrete time interval temporal logic (Moszkowski, 1986) by the neighbourhood modalities (ITL-NL) and a lemma which is key in establishing this form of separation in (Guelev and Moszkowski, 2022) can be used to obtain concise proofs of an interval-based form of the reactivity normal form as known from (Manna and Pnueli, 1990), a new normal form for ITL formulas which, given a state formula w, features the conditions that the maximal w- and non w-subintervals of an interval satisfying the given formula need to satisfy, the expressibility of the inverse of the temporal projection operator from (Halpern, Manna and Moszkowski, 1983), the elimination of propositional quantification in ITL-NL and, consequently, uniform Craig interpolation and Beth definability for ITL-NL.