On the implementation complexity of specifications of concurrent programs

Research output: Contribution to journalArticle

1 Scopus citations


We present a decision algorithm for the following problem: given a specification, does there exist a concurrent program which both satisfies the specification and which can be implemented in hardware-available operations in a straightforward manner, i.e, without long correctness proofs, and without introducing excessive blocking and/or centralization? In case our decision algorithm answers "yes," we also present a synthesis method to produce such a program. We consider specifications expressed in branching time temporal logic. Our result gives a way of classifying specifications as either "easy to implement" or "difficult to implement," and can be regarded as the first step towards a notion of "implementation complexity" of specifications.

Original languageEnglish (US)
Pages (from-to)151-165
Number of pages15
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publication statusPublished - Dec 1 2003
Externally publishedYes


ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this