Automatic translation of natural language system specifications into temporal logic

Abstract

This paper presents a method for automatically translating natural language specifications into temporal logic. Using this method, users may express complex specifications in relatively free natural language, allowing multi-sentence specifications, the use of pronouns instead of repeating the description of previously mentioned objects and complex temporal relations. These specifications are translated into temporal logic, while ensuring the correctness of the translation. This approach overcomes a well-known obstacle of applying model-checking industrially. In contrast to prior attempts, the translation is linguistically based on a modern formalism for discourse representation. An implementation of this translation method is presented in one of the modern computational linguistics systems.