On the Complexity of Verifying Concurrent Transition Systems
------------------------------------------------------------

In implementation verification, we check that an
implementation is correct with respect to a specification by checking
whether the behaviors of a transition system that models the program's
implementation correlate with the behaviors of a transition system
that models its specification. In this paper, we investigate the effect
of concurrency on the complexity of implementation verification.  
We consider trace-based and tree-based approaches to the verification
of concurrent transition systems, with and without fairness. Our
results show that in almost all cases the complexity of the problem is
exponentially harder than that of the sequential case. Thus, 
as in the model-checking verification methodology, the state-explosion
problem cannot be avoided.