
Extending Temporal Logic Programming with
Choice Predicates Nondeterminismy
MEHMET A. ORGUN WILLIAM W. WADGE
Department of Computing Department of Computer Science
Macquarie University University of Victoria
Sydney, NSW 2109, Australia Victoria, B.C. V8W 3P6, Canada
Abstract
In temporal logic programming, a stream can be specified by a singlevalued, timevarying predicate which, at any given moment in time, represents the corresponding element in the stream. However, due to inherent nondeterminism in logic programming, timevarying predicates do not necessarily represent singlevalued relations at any given moment in time. Choice predicates are also timevarying predicates, but, in principle, they act like a dataflow node with multiple input lines which nondeterministically selects one of its inputs as output. Therefore they are guaranteed to be singlevalued at all moments in time, and they can be regarded as representing ondeterministic" streams. Users do not define choice predicates, they are supplied automatically for all predicates defined in temporal logic programs. Inputs to choice predicates are supplied by the corresponding predicates. When the connection between choice predicates and the corresponding predicates is established, we obtain nonHorn temporal logic programs as a result. The modeltheoretic semantics of such a program is developed in terms of minimal models". However, the logical structure of the program dictates which minimal models are constructible from the program. We in particular discuss a characterization of constructible minimal models as limits of chains of models obtained by alternating applications of two new mappings NTP and CP . The paper also outlines a proof procedure for the temporal language Chronolog extended with choice predicates.
1 Introduction
In logic programming languages, streams are usually represented by infinitary data structures such as infinite lists. Through streams, nonterminating dataflow computations can be modeled in concurrent logic programming languages such as Parlog [14]
yTo appear in Journal of Logic and Computation