Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Logical Interpolation and Projection onto State in the Duration Calculus

Logical Interpolation and Projection onto State in the Duration Calculus 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Applied Non-Classical Logics Taylor & Francis

Logical Interpolation and Projection onto State in the Duration Calculus

Guelev, Dimitar P.
Journal of Applied Non-Classical Logics , Volume 14 (1-2): 28 – Jan 1, 2004
Download PDF
28 pages

Logical Interpolation and Projection onto State in the Duration Calculus

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,...
Loading next page...
 
/lp/taylor-francis/logical-interpolation-and-projection-onto-state-in-the-duration-AeWak2tNhH
Publisher
Taylor & Francis
Copyright
Copyright Taylor & Francis Group, LLC
ISSN
1958-5780
eISSN
1166-3081
DOI
10.3166/jancl.14.181-208
Publisher site
See Article on Publisher Site

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.

Journal

Journal of Applied Non-Classical Logics – Taylor & Francis

Published: Jan 1, 2004

Keywords: duration calculus; projection; Craig interpolation

There are no references for this article.