perm filename FOURTN.MSS[BIB,CSR]3 blob sn#620177 filedate 1981-10-28 generic text, type C, neo UTF8

COMMENT ā VALID 00002 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 @Entry(Code "STAN-CS-81-871", C00012 ENDMK Cā; @Entry(Code "STAN-CS-81-871", Title "Good Layouts for Pattern Recognizers", Author "Howard W. Trickey", Price "$2.45", not available, Note "15 pages", Date "August 1981") A system to lay out custom circuits that recognize regular languages can be a useful VLSI design automation tool. This paper describes the algorithms used in an implementation of a regular expression compiler. Layouts that use a network of programmable logic arrays (PLA's) have smaller areas than those of some other methods, but there are the problems of partitioning the circuit and then placing the individual PLA's. Regular expressions have a structure which allows a novel solution to these problems: dynamic programming can be used to find layouts which are in some sense optimal. Various search pruning heuristics have been used to increase the speed of the compiler, and the experience with these is reported in the conclusions. @Entry(Code "STAN-CS-81-872", Title "Synthesis of Communicating Processes from Temporal Logic Specifications", Author "Zohar Manna and Pierre Wolper", Price "$2.85", FREE, Note "28 pages", Date "September 1981") In this paper, we apply Propositional Temporal Logic (PTL) to the specification and synthesis of the synchronization part of communicating processes. To specify a process, we give a PTL formula that describes its sequence of communications. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL. This model can then be interpreted as a program. @Entry(Code "STAN-CS-81-874", Title "Multiprocessing Architectures for Local Computer Networks", Author "Alfred Z. Spector", Price "$5.75", FREE, Note "125 pages", Date "August 1981") The scheduling problem for unit time task systems with arbitrary precedence constraints is known to be NP-complete. We show that the same is true even if the precedence constraints are restricted to certain subclasses which make the corresponding parallel programs more structured. Among these classes are those derived from hierarchic cobegin-coend programming constructs, level graph forests, and the parallel or serial composition of an out-tree and an in-tree. In each case, the completeness proof depends heavily on the number of processors being part of the problem instances. @Entry(Code "STAN-CS-81-876", Title "On Linear Area Embedding of Planar Graphs", Author "Danny Dolev and Howard Trickey", Price "$2.65", FREE, Note "21 pages", Date "September 1981") Planar embedding with minimal area of graphs on an integer grid is one of the major issues in VLSI. Valiant has given an algorithm to construct a planar embedding for trees in linear area; he also proved that there are planar graphs that require quadratic area. We give an algorithm to embed outerplanar graphs in linear area. We extend this algorithm to work for for every planar graph that has the following property: for every vertex there exists a path of length less than K to the exterior face, where K is a constant. Finally, finding a minimal embedding area is shown to be NP-Complete for forests, and hence for more general types of graphs. @Entry(Code "STAN-CS-81-877", Title "Verification of Sequential Programs: Temporal Axiomatization", Author "Zohar Manna", Price "$3.35", FREE, Note "45 pages", Date "September 1981") This is one in a series of reports describing the application of temporal logic to the specification and verification of computer programs. In earlier reports, we introduced temporal logic as a tool for reasoning about concurrent programs and specifying their properties and presented proof principles for establishing these properties. Here, we restrict ourselves to deterministic, sequential programs. We present a proof system in which properties of such programs, expressed as temporal formulas, can be proved formally. Our proof system consists of three parts: a general part elaborating the properties of temporal logic, a domain part giving an axiomatic description of the data domain, and a program part giving an axiomatic description of the program under consideration. We illustrate the use of the proof system by giving two alternative formal proofs of the total correctness of a simple program. @Entry(Code "STAN-CS-81-878", Title "Maximal Objects and the Semantics of Universal Relation Databases", Author "David Maier and Jeffrey D. Ullman", Price "2.30", FREE, Note "10 pages", Date "October 1981")