Entry Attie:1998:SCS from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Attie:1998:SCS,
  author =       "Paul C. Attie and E. Allen Emerson",
  title =        "Synthesis of concurrent systems with many similar
                 processes",
  journal =      j-TOPLAS,
  volume =       "20",
  number =       "1",
  pages =        "51--115",
  month =        jan,
  year =         "1998",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Sat Jan 2 10:46:05 MST 1999",
  bibsource =    "http://www.acm.org/pubs/toc/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org:80/pubs/citations/journals/toplas/1998-20-1/p51-attie/",
  abstract =     "Methods for synthesizing concurrent programs from
                 temporal logic specifications based on the use of a
                 decision procedure for testing temporal satisfiability
                 have been proposed by Emerson and Clarke and by Manna
                 and Wolper. An important advantage of these synthesis
                 methods is that they obviate the need to manually
                 compose a program and manually construct a proof of its
                 correctness. One only has to formulate a precise
                 problem specification; the synthesis method then
                 mechanically constructs a correct solution. A serious
                 drawback of these methods in practice, however, is that
                 they suffer from the state explosion problem. To
                 synthesize a concurrent system consisting of $K$
                 sequential processes, each having $N$ states in its
                 local transition diagram, requires construction of the
                 global product-machine having about {\em NK\/} global
                 states in general. This exponential growth in $K$ makes
                 it infeasible to synthesize systems composed of more
                 than 2 or 3 processes. In this article, we show how to
                 synthesize concurrent systems consisting of many (i.e.,
                 a finite but arbitrarily large number $K$ of) similar
                 sequential processes. Our approach avoids construction
                 of the global product-machine for $K$ processes;
                 instead, it constructs a two-process product-machine
                 for a single pair of generic sequential processes. The
                 method is uniform in {\em K}, providing a simple
                 template that can be instantiated for each process to
                 yield a solution for any fixed {\em K}. The method is
                 also illustrated on synchronization problems from the
                 literature.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "theory; verification",
  subject =      "{\bf C.2.4} Computer Systems Organization,
                 COMPUTER-COMMUNICATION NETWORKS, Distributed Systems.
                 {\bf D.1.2} Software, PROGRAMMING TECHNIQUES, Automatic
                 Programming. {\bf D.1.3} Software, PROGRAMMING
                 TECHNIQUES, Concurrent Programming. {\bf D.2.4}
                 Software, SOFTWARE ENGINEERING, Software/Program
                 Verification. {\bf F.3.1} Theory of Computation, LOGICS
                 AND MEANINGS OF PROGRAMS, Specifying and Verifying and
                 Reasoning about Programs, Mechanical verification. {\bf
                 I.2.2} Computing Methodologies, ARTIFICIAL
                 INTELLIGENCE, Automatic Programming, Program
                 synthesis.",
}

Related entries