On the implementation complexity of specifications of concurrent programs

Paul C. Attie

Research output: Contribution to journalArticle

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 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)
Volume2848
StatePublished - Dec 1 2003
Externally publishedYes

Fingerprint

Concurrent
Specification
Specifications
Temporal logic
Temporal Logic
Branching
Correctness
Hardware
Synthesis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

@article{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",
month = "12",
day = "1",
language = "English (US)",
volume = "2848",
pages = "151--165",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

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 -