Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 10, Issue 6, pp. 877-895: Abstract.

A mixed decision method for duration calculus

N Chetcuti-Serandio and L Farinas del Cerro

Institut de Recherche en Informatique de Toulouse, 118, route de Narbonne, F-31062 Toulouse cedex 04, France, E-mail: {chetcuti, farinas}@irit.fr

The Duration Calculus is an interval logic with an additional notion of duration. It became one of the main references of real-time system specification for which it was introduced. From a practical point of view an important challenge is to define automated proof procedures for this calculus. Since the propositional Duration Calculus is undecidable, in this paper we isolate a fragment and we define a mixed decision method combining standard tableau techniques with temporal constraint network resolution algorithms. This method gives a natural procedure to decide whether a given formula is satisfiable. This fragment is strong enough to embed Allen's Interval Algebra.

Keywords: automated deduction, representation of time, software engineering

  Full-Text PDF  (216 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2000.