DocumentCode
2721696
Title
Model-checking of correctness conditions for concurrent objects
Author
Alur, Rajeev ; McMillan, Ken ; Peled, Doron
Author_Institution
AT&T Bell Labs., USA
fYear
1996
fDate
27-30 Jul 1996
Firstpage
219
Lastpage
228
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location
New Brunswick, NJ
ISSN
1043-6871
Print_ISBN
0-8186-7463-6
Type
conf
DOI
10.1109/LICS.1996.561322
Filename
561322
Link To Document