Abstract
We generalise an interval-related interpolation theorem about abstract-time Interval Temporal Logic (ITL, [MOS 85, DUT 95]), which was first obtained in [GUE 01]. The generalisation is based on the abstract-time variant of a projection operator in the Duration Calculus (DC, [ZHO 91, HAN 97, ZHO 04]), which was introduced in [DAN 99] and later studied extensively in [GUE 02]. We propose a way to understand interpolation in the context of formal verification. We give an example showing that, unlike abstract-time ITL, DC does not have the Craig interpolation property in general, and establish a special form of Craig interpolation for abstract-time DC. Explicit definability after Beth is known to be strongly related to Craig interpolation in general. We show a limitation of a different kind to the scope of Beth definability in ITL by a counterexample too. We call the generalisation of interval-related interpolation that we present projection-related interpolation. The DC-specific restrictions apply to it too. We show that both Craig and projection-related interpolation hold about the ⌈P⌉-subset of DC without such restrictions. Our proofs of these theorems for the ⌈P⌉-subset entail algorithms for the construction of the interpolants.
Original language | English |
---|---|
Pages (from-to) | 181-208 |
Number of pages | 28 |
Journal | Journal of Applied Non-Classical Logics |
Volume | 14 |
Issue number | 1-2 |
DOIs | |
Publication status | Published - 27 Jun 2004 |