Loading...
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.
Type
research article
Web of Science ID
WOS:000481764700002
Author(s)
Date Issued
2019-09-01
Publisher
Published in
Volume
101
Issue
9
Start page
1227
End page
1240
Peer reviewed
REVIEWED
Written at
EPFL
EPFL units
Available on Infoscience
September 6, 2019
Use this identifier to reference this record