Applications of discrete-time interval-based temporal separation

We show how interval-based temporal separation in the extension of Moszkowski’s discrete time interval temporal logic (ITL; Moszkowski, Executing Temporal Logic Programs. Cambridge University Press, 1986) by the neighbourhood modalities (ITL-NL) and a lemma that is key in establishing this form of separation in Guelev and Moszkowski (2022, A separation theorem for discrete-time interval temporal logic, J. Appl. Non Class. Logics, 32, 28–54) can be used to obtain concise proofs of an interval-based version of the reactivity normal form known from Manna and Pnueli (A hierarchy of temporal properties. In 9th Symposium on Principles of Distributed Computing, pp. 377–408. ACM Press, 1990), a new normal form for ITL formulas that, given a state formula w, features the conditions that the maximal w- and w-subintervals of an interval satisfying the given formula must satisfy, the expressibility of the inverse of the temporal projection operator from Halpern, Manna and Moszkowski (A hardware semantics based on temporal intervals. In ICALP 1983, Proceedings, Volume 154 of LNCS, J. Daz, ed, pp. 278–291. Springer, 1983) in ITL, the elimination of propositional quantification in ITL-NL and, consequently, uniform Craig interpolation and Beth definability for ITL-NL.