Robust Vacuity for Branching Temporal Logic

Arie Gurfinkel, Marsha Chechik

There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventu…