On the implementation complexity of specifications of concurrent programs

Paul C. Attie

doi:10.1007/978-3-540-39989-6_11

On the implementation complexity of specifications of concurrent programs

Paul C. Attie

Research output: Chapter in Book/Report/Conference proceeding › Chapter

1 Scopus citations

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)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Faith Ellen Fich
Publisher	Springer Verlag
Pages	151-165
Number of pages	15
ISBN (Print)	354020184X, 9783540201847
DOIs	https://doi.org/10.1007/978-3-540-39989-6_11
State	Published - 2003
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2848
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-39989-6_11

Cite this

Attie, P. C. (2003). On the implementation complexity of specifications of concurrent programs. In F. E. Fich (Ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 151-165). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2848). Springer Verlag. https://doi.org/10.1007/978-3-540-39989-6_11

On the implementation complexity of specifications of concurrent programs. / Attie, Paul C.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Faith Ellen Fich. Springer Verlag, 2003. p. 151-165 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2848).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Attie, PC 2003, On the implementation complexity of specifications of concurrent programs. in FE Fich (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2848, Springer Verlag, pp. 151-165. https://doi.org/10.1007/978-3-540-39989-6_11

Attie PC. On the implementation complexity of specifications of concurrent programs. In Fich FE, editor, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2003. p. 151-165. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-39989-6_11

Attie, Paul C. / On the implementation complexity of specifications of concurrent programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Faith Ellen Fich. Springer Verlag, 2003. pp. 151-165 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{1a029576a1564d22925e3779d85cdd17,

title = "On the implementation complexity of specifications of concurrent programs",

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.",

author = "Attie, {Paul C.}",

year = "2003",

doi = "10.1007/978-3-540-39989-6_11",

language = "English (US)",

isbn = "354020184X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "151--165",

editor = "Fich, {Faith Ellen}",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - On the implementation complexity of specifications of concurrent programs

AU - Attie, Paul C.

PY - 2003

Y1 - 2003

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

U2 - 10.1007/978-3-540-39989-6_11

DO - 10.1007/978-3-540-39989-6_11

M3 - Chapter

AN - SCOPUS:35248820690

SN - 354020184X

SN - 9783540201847

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 151

EP - 165

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Fich, Faith Ellen

PB - Springer Verlag

ER -

On the implementation complexity of specifications of concurrent programs

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this