Skip to main content
main-content

Inhaltsverzeichnis

Frontmatter

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

Chapter II. Axiomatization of Propositional Temporal Logic

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