On the size of data structures used in symbolic model checking

Paolo Liberatore, Marco Schaerf

Temporal Logic Model Checking is a verification method in which we describe a system, the model, and then we verify whether some properties, expressed in a temporal logic formula,…