Temporal logic is gaining recognition as an attractive and versatile formalism for rigorously specifying and reasoning about computer programs, digital circuits and message-passing systems. This book introduces Tempura, a programming language based on temporal logic, Tempura provides a way of directly executing suitable temporal logic specifications of digital circuits, parallel programs and other dynamic systems. Since every Tempura statement is also a temporal formula, the entire temporal logic formalism can be used as the assertion language and semantics. One result is (...) that Tempura has the two seemingly contradictory properties of being a logic programming language and having imperative constructs such as assignment statements. The presentation investigates Interval Temporal Logic, a formalism with conventional temporal operators such as next and always as well as lesser known ones such as chop. This provides the basis for Tempura. The design of an interpreter for Tempura is also included, as are a variety of sample Tempura programs illustrating how to model both hardware and software. (shrink)

This paper presents a new kind of interpolation theorems about Neighbourhood Logic and Interval Temporal Logic . Unlike Craig interpolation, which holds for these logics too, the new theorems treat the existence of interpolants which specify properties of selected intervals in the models of NL and ITL.

Craig's interpolation lemma (if φ → ψ is valid, then φ → θ and θ → ψ are valid, for θ a formula constructed using only primitive symbols which occur both in φ and ψ) fails for many propositional and first order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves (...) many technical problems. The paper presents strong evidence for this claim by defining interpolation algorithms for both propositional and first order hybrid logic. These algorithms produce interpolants for the hybrid logic of every elementary class of frames satisfying the property that a frame is in the class if and only if all its point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur. (shrink)

Quantified hybrid logic is quantified modal logic extended with apparatus for naming states and asserting that a formula is true at a named state. While interpolation and Beth's definability theorem fail in a number of well-known quantified modal logics , their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of first-order logic has the interpolation property, (...) irrespective of whether varying, constant, expanding, or contracting domains are assumed. (shrink)