Technical reports

Executing temporal logic programs
(full version)

Ben Moszkowski

August 1985, 96 pages

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.

Full text

PDF (6.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-71,
  author =	 {Moszkowski, Ben},
  title = 	 {{Executing temporal logic programs (full version)}},
  year = 	 1985,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-71.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-71},
  number = 	 {UCAM-CL-TR-71}
}