A model checker for linear time temporal logic

This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.This work was supported both by Alvey under grant PRJ/SE/054 (SERC grant GR/D/57942) and by ESPRIT under Basic Research Action 3096 (SPEC).