TLC: A Temporal Logic with Clocks

Chuchang Liu Mehmet A. Orgun

Department of Computing

Macquarie University

NSW 2109, Australia

E-mail: fcliu,[email protected]

ABSTRACT

Temporal logic language TLC is a linear-time logic with multiple granularity of time. In this logic, all formulas can be clocked and are allowed to be defined on local clocks which are subsequences of the global clock. The language can be used to describe 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 [7, 1], reasoning about time [9] and modeling temporal databases [2].

In logic languages based on line-time temporal logics, all predicates are usually defined on a global clock. For instance, in temporal logic programming language Chronolog [8], the set of natural numbers ! models the collection of moments in time with an unbounded future. All predicates appearing in a Chronolog program are defined on the global clock, i.e., the sequence of natural numbers < ; 1; 2; : : : >. However, in some applications, such as distributed computations and temporal databases, one may find that it is necessary to consider local time" or provide local clocks; some events occur at irregular intervals, and it seems unnatural to force them all onto a prescribed notion of time.

To model the behavior of systems in which granularity of time is needed, Chronolog is extended by introducing multiple clocks, that is, defining local clocks associated with predicate symbols [3, 4]. The extended language is called Chronolog(MC),

for Chronolog with Multiple Clocks". It is based on a temporal logic with clocks, called TLC. In this logic, all formulas can be clocked and are allowed to be defined on local clocks different from the global clock. Because of the introduction of multiple clocks, the temporal language can be applied to the specification of a wide range of simulation systems and other relevant tasks where the notion of dynamic change is central.

In this paper, summarising our previous work [4, 3, 5], we briefly introduce the temporal logic TLC and its applications to the description of simulation systems. Because of space limitations, all proofs for the lemmas are omitted.

2 SYNTAX

A local clock is a subsequence of the global clock, i.e. the strictly increasing sequence of natural numbers: < ; 1; 2; : : : >. Let CK be the set of all clocks and v be a ordering relation on the elements of CK defined as follows: for any ck1; ck2 2 CK, ck1 v ck2 iff for all t 2 ck1, we have that t 2 ck2, where the expression t 2 cki denotes the fact that t is a moment in time on the clock cki. It is easy to show that (CK; v) is a complete lattice. Therefore, we can define

ck1 u ck2 def= g:l:b:fck1; ck2g

ck1 t ck2 def= l:u:b:fck1; ck2g

where ck1; ck2 2 CK, g:l:b: stands for greatest lower bound" and l:u:b: for least upper bound" under the relation v.

In TLC, we have two temporal operators : first and next, which refer to the initial moment and the next moment in time, respectively. TLC formulas are constructed using the following rules: (1) Any formula of first-order logic is a TLC formula; (2) if A is a formula, then first A and next A are also formulas.