## Model-Checking of Correctness Conditions for Concurrent Objects

*Rajeev Alur, Kenneth L. McMillan, and Doron A. Peled*
The notions of serializability, linearizability and sequential
consistency are used in the specification of concurrent systems. We
show that the model checking problem for each of these properties can
be cast in terms of the containment of one regular language in another
regular language shuffled using a semi-commutative alphabet. The three model
checking problems are shown to be, respectively, in {\sc Pspace}, in
{\sc Expspace}, and undecidable.

*Proceedings of the
11th Annual IEEE Symposium on Logic in Computer Science*
(LICS 1996), pp. 219-228.