Verification of Fair Transition Systems

In program verification, we check that an implementation meets its specification. Both the specification and the implementation describe the possible behaviors of the program, though at different levels of abstraction. We distinguish between two approaches to implementation of specifications. The first approach is trace-based implementation, where we require every computation of the implementation to correlate to some computation of the specification. The second approach is tree-based implementation, where we require every computation tree embodied in the implementation to correlate to some computation tree embodied in the specification. The two approaches to implementation are strongly related to the linear-time versus branching-time dichotomy in temporal logic. In this work we examine the trace-based and the tree-based approaches from a complexitytheoretic point of view. We consider and compare the complexity of verification of fair transition systems, modeling both the implementati..