1992•Formal Aspects of ComputingRequires access
A model checker for linear time temporal logic
Michael Fisher
Open publisher page 6 citations
Abstract
Abstract 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.