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