STOC

We study the expressive power of various versions of Dynamic Logic and compare them with each other as well as with standard languages in the logical literature. One version of Dynamic Logic is equivalent to the infinitary logic L^CK_ω1ω, but regular ...

This paper introduces a logic for probabilistic programming⁺ PROB-DL (for probabilistic dynamic logic; see Section 2 for a formal definition). This logic has “dynamic” modal operators in which programs appear, as in Pratt's [1976] dynamic logic DL. ...

Propositional algorithmic logic PAL is a propositional counterpart of algorithmic logics. It investigates properties of program connectives: begin...end, while...do, if..then..else, or .... PAL supplies tools for reasoning about programs constructed ...

Dynamic algebras constitute the variety (equationally defined class) of models of the Segerberg axioms for propositional dynamic logic. We obtain the following results (to within inseparability). (i) In any dynamic algebra * is reflexive transitive ...

A generalization of the alternate stacking procedure of Valiant for deciding the equivalence of some deterministic pushdown automata (dpda) is introduced. To analyze the power of the generalized procedure we define a subclass of dpda's, called the ...

It follows by Gödel's incompleteness Theorem [6] that any effective sound system of logic for elementary arithmetic must be incomplete. We show that in any effective sound system of logic for elementary arithmetic, there exist valid unprovable formulae ...

The main results of this paper demonstrate the consistency of “P = NP” and a variant of “NP @@@@ coNP” with certain natural fragments of number theory to be defined precisely in the sequel.@@@@ Consistency results represent an approach to the lower ...

Although there has been considerable additional work discussing limitations of formal proof techniques for Computer Science ([YO-73&77], [HAR-76], [HAR&HO-77], [HAJ-77&79], [GO-79]), these papers show only very general consequences of incompleteness: ...

Dijkstra's informally-stated Dining Philosophers problem [D] involves a number n of philosophers sitting in a circle, a single fork between each pair of adjacent philosophers. The problem is to program the philosophers in ways which guarantee certain ...

This paper attempts to get at some of the fundamental properties of distributed computing by means of the following question: “How much does each processor in a network of processors need to know about its own identity, the identities of other ...

A controller for a packet switching network is an algorithm to control the flow of packets through the network. A local controller is a controller executed independently by each node in the network, using only local information available to these nodes. ...

This paper is part of an investigation into efficient ways of implementing variable-length lists (see Brown [1]). Storage and access optimality are discussed from an information-theoretic viewpoint; in particular, we develop the notions of Kraft storage ...

Given a vector of tasks intended to execute the same program simultaneously on a machine which can execute only one instruction at a time, but can execute that instruction for any specified subset of the vector, the object is to schedule the execution ...

Relational database theory has discovered complete axiomatizations for functional and multivalued dependencies. However, a database design system that makes use of dependencies declared by the user must deal with some more general kinds of dependencies ...

In the last year or so, a number of generalizations of these dependencies have appeared: Nicolas's mutual dependencies [Ni], which say that a relation is the join of three of its projections; Rissanen's and Aho, Beeri, and Ullman's join dependencies ([...

For a number of common configurations of points (lines) in the plane, we develop datastructures in which insertions and deletions of points (or lines, respectively) can be processed rapidly without sacrificing much of the efficiency of query answering ...

Perhaps the most important application of computer geometry involves determining whether a pair of convex objects intersect. This problem is well understood in a model of computation where the objects are given as input and their intersection is ...

Given a collection of disjoint objects in the plane, we are interested in translating them by a common vector. If we have a primitive for translating one object at a time, then the order in which the objects can individually be translated is often ...

A wire-routing problem which arises commonly in the layout of circuits for very large scale integration (VLSI) is discussed. Given the coordinates of terminals u₁, u₂, ..., u_n of one component and v₁, v₂, ..., v_n of another, the problem is to lay out n ...

We consider the problem of finding a minimal cost layout of a tree in Euclidian d-space. A tree is an acyclic undirected edge-weighted graph, and a layout is an assignment of a point in d-dimensional Euclidian space to each of the nodes of the tree. The ...

The chip complexity of a computation is concerned with the chip area, A, and the time, T, required to perform the computation when implemented on a chip. An area-time product AT^α,for α ≥ 0, is used as a complexity measure. A particular value of α, which ...

The two major cost measures used in the past for grid embeddings are area (or the area of the smallest square or rectangle that contains the embedding) and total edge length. This paper is primarily concerned with a third measure, total number of nodes. ...

The k paths problem asks whether it is possible to find k edge-disjoint paths joining k given pairs of vertices in a graph. We show that this problem can be solved in polynomial time for k≤5 if the input graph is k+2 -connected.

It follows from this ...

There are no known polynomial time algorithms for graph isomorphism. For certain classes of graphs, however, efficient algorithms have been found. In particular, there is a polynomial time algorithm for isomorphism of planar graphs [4,5].

This paper ...

We present an algorithm which determines isomorphism of graphs in v^O(g)steps where v is the number of vertices and g is the genus of the graphs. In [FMR 79] an algorithm was presented for embedding graph on surfaces of genus g in v^O(g) steps. Here we ...

The isomorphism problem for graphs has been in recent years the object of a much research (see e.g. [Col 78] or [Re-Cor 77]). Its complexity is still unknown. It is not known whether the problem is NP-complete, although it is NP, of course. It is not ...

We give algorithms to decide graph isomorphism in a subclass of graphs which we call cone graphs. A cone graph is an undirected graph for which there exists a vertex r which uniquely determines a breadth-first search (BFS) tree. Equivalently, all ...

The “accessibility problem” for linear sequential machines (Harrison [7]) is the problem of deciding whether there is an input x that sends such a machine from a given state q₁ to a given state q₂. Harrison [7] showed that this problem is reducible to ...

We exploit the fact that the set of all polynomials Pε@@@@[x₁,..,x_n] of degree ≤d which can be evaluated with ≤v nonscalar steps can be embedded into a Zariski-closed affine set W(d,n,v),dim W(d,n,v)≤(v+1 +n)² and deg W(d,n,v)≤(2vd)^(v+1+n)2. As a ...

We look at several classes of straight-line programs and show that the equivalence problem is either undecidable or computationally intractable for all but the trivial classes. For example, there is no algorithm to determine if an arbitrary program (...