Dealing with Multiple Granularity of Time

in Temporal Logic Programming

CHUCHANG LIU AND MEHMET A. ORGUN

Department of Computing, Macquarie University, NSW 2109, Australia
Tel: +61 2 850-9514 (dept), Fax: +61 2 850-9551
E-mail: fcliu,[email protected]

Abstract
Chronolog(MC) is an extension of logic programming based on a clocked temporal logic (CTL), a linear-time temporal logic with multiple granularity of time. A Chronolog(MC) program consists of a clock definition, a clock assignment and a program body, and each predicate symbol appearing in the program body is associated with a local clock through the clock definition and assignment. This paper investigates the logical basis of the language, presents a clocked temporal resolution where time-matching is essential, and in particular proposes three algorithms for time-matching. The paper also discusses the declarative semantics for Chronolog(MC) programs in terms of clocked temporal Herbrand models. It is shown that Chronolog(MC) programs also satisfy the minimum model semantics. The language can be used to model a wide range of simulation systems and other relevant tasks where the notion of dynamic change is central.

1 Introduction

An important activity in computer science is the invention, analysis and application of formal logics which are designed to specify, reason about and represent algorithms, programs and systems. Recently, there is a substantial interest in temporal logic which has been widely used as a formalism for program specification and verification (Manna and Pnueli, 1981), reasoning about time (Sadri, 1987) and modeling temporal databases (Chomicki, 1994; Gabbay and McBrien 1991; Gagn?e and Plaice, 1995).

Some researchers have recently suggested that temporal logic can be directly used as programming languages. For instance, Tokio (Aoyagi et al, 1986) is a logic language based on interval temporal logic; Templog (Abadi and Manna, 1989; Baudinet, 1992) and Chronolog (Wadge, 1988; Orgun and Wadge, 1992) are based on linear-time temporal logics; Temporal Prolog (Gabbay, 1987,1991) is based on linear and branching time temporal logics; and Metatem (Fisher and Owens, 1992; Fisher, 1994; Fisher and Reynolds, 1995) is a framework for the direct execution of temporal logics within which programs are represented as sets of temporal rules of a particular form. There are also a number of other temporal logic programming languages (Brzoska,1993; Tang,1989; Hrycej, 1993; Fruhwirth, 1993). For more information, we refer the reader to the surveys of Fisher and Owens (1993), and Orgun and Ma (1994).

1.1 Motivation { Why Extend Chronolog?

Chronolog is suitable for specifying time-dependent properties of certain problems in a natural way (Orgun and Wadge, 1992; Liu and Orgun, 1995). It is based on a linear-time