Hamza, Jad2019-09-062019-09-062019-09-062019-09-0110.1007/s00607-018-0596-7https://infoscience.epfl.ch/handle/20.500.14299/160912WOS:000481764700002It 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.Computer Science, Theory & MethodsComputer Sciencelinearizabilitycomplexityverificationconcurrencymodel-checkingtext::journal::journal article::research article