In 1977, WIS scientists formalized a specially tailored variant of the classical logic of time ("tense logic"), termed "temporal logic", in order to make it possible to specify formally the requirements of complex system, where the complixity arises from the unpredictable interactions with the environment. Temporal logic has become the main lingua franca for specifying system requirements, and it forms the basis for many verification techniques for software and system. In particular, the reigning verification method, model checking, uses temporal logic as its underlying formalism.
Over the years, numerous variants of temporal logic have been defined for a variety of specification and verification tasks for both hardware and software, including ones that deal with infinite domains. Program and system verification cannot be considered these days without the availability of temporal logic and its underlying rich theory.
In 1996 these contributions served as the basis for bestowing the Turing Award on their developer.