We present a completeness proof for Propositional Interval Temporal Logic with finite time which avoids certain difficulties of conventional methods. It is more gradated than previous efforts since we progressively reduce reasoning within the original logic to simpler reasoning in sublogics. Furthermore, our approach benefits from being less constructive since it is able to invoke certain theorems about regular languages over finite words without the need to explicitly describe the associated intricate proofs. A modified version of regular expressions called Fusion (...) Expressions is used as part of an intermediate logic called Fusion Logic. Both have the same expressiveness as PITL but are lower-level notations which play an important role in the hierarchical structure of the overall completeness proof. In particular, showing completeness for PITL is reduced to showing completeness for Fusion Logic. This in turn is shown to hold relative to completeness for conventional linear-time temporal logic with finite time. Logics based on regular languages over finite words and!-words offer a promising but elusive framework for formal specification and verification. A number of such logics and decision procedures have been proposed. In addition, various researchers have obtained complete axiom systems by embedding and expressing the decision procedures directly within the logics. The work described here contributes to this topic by showing how to exploit some interesting links between regular languages and interval-based temporal logics. (shrink)

We generalise an interval-related interpolation theorem about abstract-time Interval Temporal Logic, which was first obtained in [GUE 01]. The generalisation is based on the abstract-time variant of a projection operator in the Duration Calculus, 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. (shrink)

We present a complete axiomatisation of the operator of projection onto state in the Duration Calculus relative to validity in DC without extending constructs. Projection onto state was introduced and studied extensively in our earlier works. We first establish the completeness of a system of axioms and proof rules for the operator relative to validity in the extension of DC by neighbourhood formulas, which express the neighbourhood values of boolean DC state expressions. By establishing a relatively complete axiomatisation for the (...) neighbourhood formulas in DC, we then achieve completeness of our system relative to basic DC. (shrink)

Gabbay's separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In this paper, we establish an analogous statement a...

Interval Temporal Logic is a finite-time linear temporal logic with applications in hardware verification, temporal logic programming and specification of multimedia documents. Due to the logic's non-elementary complexity, efficient ITL-based verification tools have been difficult to develop, even for propositional subsets. MONA is an efficient implementation of an automata-based decision procedure for the logic WS1S. Despite the non-elementary complexity of WS1S, MONA has been successfully applied in problems such as hardware synthesis, protocol verification and theorem proving. Here we consider a (...) rich propositional subset of ITL, PITL, whose expressive power is equivalent to that of WS1S, and in turn to that of regular languages. PITL not only includes operators such as chop, star and projection, but also past operators such as previous, chop in the past and since. We provide an interpretation of PITL formulas in WS1S, which led us to a direct translation from PITL formulas to MONA specifications. We present the tool PITL2MONA as an implementation of such translation. With PITL2MONA acting as a front-end, MONA is used as a decision procedure for PITL. To our knowledge, this is one of the few implementations of a decision procedure for PITL, the first one based on automata, and the only one which handles both projection and past operators. We have tested our implementation on a number of examples; we show in this paper the application of PITL and its MONA-based decision procedure in solutions to the dining-philosophers and a multimedia synchronisation problem, together with some experimental results on these and some other examples. (shrink)