In this section, we present a brief introduction to five temporal logic-based programming languages: Chronolog, F-Limette, Concurrent MetateM, Tempura and Tokio. While a variety of verification systems based upon temporal logics have been produced, particularly involving model-checking techniques, the development of executable temporal logics is becoming increasingly important. It may turn out that the effective utilization of the full power of temporal logics in a wide range of areas will depend crucially upon the development of such languages. Since a number of researchers have tried to implement various programming languages based on temporal logic, the systems described here provide only limited coverage of the research area. However, they represent systems that are currently under active development and, as such, provide an indication of the breadth of ongoing research in this field.
Each of the sections that follow covers one of the five languages. Within each section, an introduction to the language and its applications is given, and the significant references and pointers to FTP and WWW sites are provided.
We can classify these languages in several ways. Chronolog and Concurrent MetateM use linear-time temporal logic, while Tempura and Tokio use interval temporal logic and F-Limette uses metric temporal logic. Concurrent MetateM and Tempura use deterministic execution schemes suitable for practical programming languages, while the others are extensions of Prolog (or at least SLD-resolution) and feature backtracking mechanisms. Concurrent MetateM is naturally applicable to concurrent object-based (and agent-based) systems, while the others are primarily intended for single object implementation. Thus, together, these languages cover much of the range of elements being actively explored throughout the field of executable temporal logics.