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

TL;DR

The paper develops interval-based separation results for ITL-NL to derive a concise interval-based reactivity normal form, and to establish the inverse of the temporal projection operator, elimination of propositional quantification, and uniform Craig interpolation and Beth definability. It leverages separation, guarded normal forms, and automata-theoretic arguments to obtain a finite closure under decomposition and to express Pi-inverse without increasing expressive power. These results yield uniform interpolation and definability theorems for ITL-NL, extending definability tools beyond point-based temporal logics through neighbourhood modalities. Overall, the work significantly enhances the definability and interpolation toolbox for ITL-NL and demonstrates robust interval-based normal forms and transformations.

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), 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.

Theorems & Definitions (12)

• Definition 1.1
• Definition 1.2
• Theorem 1.3: Corollary 2.6 in GM2022
• Proposition 1.4: Lemma 3.2 in GM2022
• Proposition 1.5: Lemma 3.4 in GM2022
• Proposition 2.1
• Theorem 5.1
• Lemma 5.2
• Theorem 6.1
• Corollary 6.2: Strongest Consequence in $$ITL-NL$$