Checking Properties within Fairness and Behavior Abstractions

Ulrich Ultes-Nitsche, Pierre Wolper

This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used. It shows that using a m…