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 language||English (US)|
|Number of pages||15|
|Journal||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Publication status||Published - Dec 1 2003|
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)