Madhavan Mukund
Tutorial talk, Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, January 1997.
Over the past two decades, temporal logic has become a very basic tool for specifying properties of reactive systems. For finite-state systems, it is possible to use techniques based on Büchi automata to verify if a system meets its specifications. This is done by synthesizing an automaton which generates all possible models of the given specification and then verifying if the given system refines this most general automaton. In these notes, we present a self-contained introduction to the basic techniques used for this automated verification. We also describe some recent space-efficient techniques which work on-the-fly.