## DIMACS TR: 96-21

## Verification of Fair Transition Systems

### Authors: Orna Kupferman, Moshe Y. Vardi

**
ABSTRACT
**

In {\em program verification\/}, we check that an {\em
implementation\/} meets its {\em 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 {\em
trace-based implementation}, where we require every computation of
the implementation to correlate to some computation of the
specification. The second approach is {\em 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 {\em complexity-theoretic\/} point of view. We consider and
compare the complexity of verification of {\em fair transition
systems}, modeling both the implementation and the specification, in
the two approaches. We consider {\em unconditional, weak\/}, and {\em
strong\/} fairness.
For the trace-based approach, the corresponding problem is {\em
fair containment}. For the tree-based approach, the corresponding
problem is {\em fair simulation}.
We show that while both problems are PSPACE-complete,
their complexities 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 trace-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.

Paper Available at:
ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1996/96-21.ps.gz

DIMACS Home Page