Symbolic Model Checking of Relative Safety LTL Properties

A well-known classification in formal methods distinguishes between safety and liveness properties. A generalization of these concepts defines safety and liveness relative to another property, usually considered an assumption on the traces of the language. Safety properties have the advantage that their model checking problem can be reduced to simple reachability. However, the generalization of such reduction to the case of relative safety has not yet been investigated. In this paper, we study the problem of model checking relative safety properties in the context of Linear-time Temporal Logic. We show that the problem can be reduced to reachability when the system model is free of livelocks related to the assumptions. More in general, we provide an algorithm that removes such livelocks from the system model driven by counterexamples to the relative safety property. We compare the approach with other reduction to safety algorithms on several benchmarks.