Executing temporal logic programs (full version)

From bibtex.

Abstract

Over the last few years, temporal logic has been investigated as a tool for reasoning about computer programs, digital circuits and message-passing systems. In earlier work we proposed that temporal logic itself directly serve as the basis of a programming language. Since then we have implemented an interpreter for such a language called Tempura. We are developing Tempura as a tool for directly executing suitable temporal logic specifications of digital circuits, parallel programs and other dynamic systems. Since every Tempura statement is also a temporal formula, we can use the entire temporal logic formalism for our assertion language and semantics. Tempura has the two seemingly contradictory properties of being a logic programming language and having imperative constructs such as assignment statements. The presentation given here describes Interval Temporal Logic (ITL), a formalism with conventional temporal operators such as ○ (next) and □ (always) as well as lesser known ones such as chop. This serves as the basis for the Tempura programming language. We show the design of an interpreter for Tempura and include a variety of sample Tempura programs illustrating how to model both hardware and software. The concept of temporal projection is also discussed and incorporated into ITL and Tempura.