
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 8509514 (dept), Fax: +61 2 8509551
Email: fcliu,[email protected]
Abstract
Chronolog(MC) is an extension of logic programming based on a clocked temporal logic
(CTL), a lineartime 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 timematching is essential, and
in particular proposes three algorithms for timematching. 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 lineartime 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 timedependent properties of certain problems in a natural way (Orgun and Wadge, 1992; Liu and Orgun, 1995). It is based on a lineartime