Computing property-preserving behaviour abstractions from trace reductions: abstraction-based verification of linear-time properties under fairness.