Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
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.
Richard Lee Davis, Engin Walter Bumbacher, Jérôme Guillaume Brender