Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eleventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1996)

Paper: Model-checking of correctness conditions for concurrent objects (at LICS 1996)

Authors: Rajeev Alur Kenneth L. McMillan Doron A. Peled

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

BibTeX

  @InProceedings{AlurMcMillanPeled-Modelcheckingofcorr,
    author = 	 {Rajeev Alur and Kenneth L. McMillan and Doron A. Peled},
    title = 	 {Model-checking of correctness conditions for concurrent objects},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996)},
    year =	 {1996},
    month =	 {July}, 
    pages =      {219--228},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski