Title :
Model-checking of correctness conditions for concurrent objects
Author :
Alur, Rajeev ; McMillan, Ken ; Peled, Doron
Author_Institution :
AT&T Bell Labs., USA
Abstract :
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 PSPACE, in EXPSPACE, and undecidable
Keywords :
decidability; formal languages; formal specification; parallel programming; EXPSPACE; PSPACE; concurrent objects; linearizability; model checking problem; regular language; semi-commutative alphabet; serializability; specification; undecidable; Application software; Automata; Computer bugs; Delay; Design optimization; History; Protocols; System recovery; Testing; Transaction databases;
Conference_Titel :
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location :
New Brunswick, NJ
Print_ISBN :
0-8186-7463-6
DOI :
10.1109/LICS.1996.561322
