Abstract

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.