In program verification, we check that an implementation meets its spe
cification. Both the specification and the implementation describe the
possible behaviors of the program, although at different levels of ab
straction. We distinguish between two approaches to implementation of
specifications. The first approach is trace-based implementation, wher
e we require every computation of the implementation to correlate to s
ome computation of the specification. The second approach is tree-base
d implementation, where we require every computation tree embodied in
the implementation to correlate to some computation tree embodied in t
he specification. The two approaches to implementation are strongly re
lated to the linear-time versus branching-time dichotomy in temporal l
ogic. In this work, we examine the trace-based and the tree-based appr
oaches from a complexity-theoretic point of view. We consider and comp
are the complexity of verification of fair transition systems, modelin
g both the implementation and the specification in the two approaches.
We consider unconditional, weak, and strong fairnesses. For the trace
-based approach, the corresponding problem is fair containment. For th
e tree-based approach, the corresponding problem is fair simulation. W
e show that while both problems are PSPACE-complete, their complexitie
s in terms of the size of the implementation do not coincide, and the
trace-based approach is easier. As the implementation is normally much
bigger than the specification, we see this as an advantage of the tra
ce-based approach. Our results are at variance with the known results
for the case of transition systems with no fairness, where no approach
is evidently advantageous.