main-content

## Inhaltsverzeichnis

### Introduction

Abstract
Important goals of mathematical logic are, in general, to:
• provide languages for the precise formulation of propositions,
• investigate mechanisms for finding out the truth or falsity of propositions.
Fred Kröger

### Chapter I. Propositional Temporal Logic

Abstract
Let us begin with an informal discussion of the basic ideas already indicated in the introduction. The starting point of our considerations is the idea that there are different time points which may yield different truth values of propositions. We make a first important agreement: we assume the set of time points to be infinite, discrete and linearly ordered with a smallest element. This leads to the following picture of a time scale:
Fred Kröger

Without Abstract
Fred Kröger

### Chapter III. First-Order Temporal Logic

Abstract
Temporal logic can be developed from its propositional basis to a first-order predicate logic in a way analogous to how this is done in the classical case.
Fred Kröger

### Chapter IV. Temporal Semantics of Programs

Abstract
We want to apply temporal logic to the description of (the computational behaviour of) programs and their verification. For the sake of technical conciseness we restrict the programs to a fixed (somewhat abstract) syntactic form.
Fred Kröger

### Chapter V. Invariance and Precedence Properties of Programs

Abstract
Let
$$\begin{array}{l} \prod \equiv initialR;\\ cobeginI{I_1}\parallel \ldots \parallel I{I_P}coend\backslash {\rm{hfill}}\backslash {\rm{end}}gathered \end{array}$$
be a program. We begin with the consideration of invariance properties whose general form is
$$A \to \square B.$$
Fred Kröger

### Chapter VI. Eventuality Properties of Programs

Abstract
We now want to investigate the verification of eventuality properties of programs expressing that “eventually something will happen”. However, we first have to come back to our interleaving model of computation and the notion of execution sequences of programs and have a somewhat closer look at them.
Fred Kröger

### Chapter VII. Special Methods for Sequential Programs

Abstract
All proof principles discussed in the previous sections are applicable to any program. For sequential programs there exist two further special verification methods which — although related to the universal methods — have some significance of their own and are sometimes easier to use. In this last chapter we want to represent these two methods within our temporal logic framework.
Fred Kröger

### Backmatter

Weitere Informationen