On the complexity of linearizability

It was previously shown that the problem of verifying whether a finite concurrent system is linearizable can be done with an EXPSPACE complexity. However, the best known lower bound is PSPACE-hardness, and can be obtained using a reduction from control-state reachability to linearizability. In this paper, we close the complexity gap between the PSPACE lower bound and the EXPSPACE upper bound, and show that linearizability is EXPSPACE-complete.