### Abstract

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) |
---|---|

Pages (from-to) | 151-165 |

Number of pages | 15 |

Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Volume | 2848 |

State | Published - Dec 1 2003 |

Externally published | Yes |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

**On the implementation complexity of specifications of concurrent programs.** / Attie, Paul C.

Research output: Contribution to journal › Article

}

TY - JOUR

T1 - On the implementation complexity of specifications of concurrent programs

AU - Attie, Paul C.

PY - 2003/12/1

Y1 - 2003/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=35248820690&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35248820690&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:35248820690

VL - 2848

SP - 151

EP - 165

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -