In order to achieve autonomous operation of a vehicle in urban situations with unpredictable traffic, several realtime systems must interoperate, including environment perception, localization, planning, and control. In addition, a robust vehicle platform with appropriate sensors, computational hardware, networking, and software infrastructure is essential. We previously published an overview of Junior, Stanford's entry in the 2007 DARPA Urban Challenge. This race was a closed-course competition which, while historic and inciting much progress in the field, was not fully representative of the situations that exist in the real world. In this paper, we present a summary of our recent research towards the goal of enabling safe and robust autonomous operation in more realistic situations. First, a trio of unsupervised algorithms automatically calibrates our 64-beam rotating LIDAR with accuracy superior to tedious hand measurements. We then generate high-resolution maps of the environment which are subsequently used for online localization with centimeter accuracy. Improved perception and recognition algorithms now enable Junior to track and classify obstacles as cyclists, pedestrians, and vehicles; traffic lights are detected as well. A new planning system uses this incoming data to generate thousands of candidate trajectories per second, choosing the optimal path dynamically. The improved controller continuously selects throttle, brake, and steering actuations that maximize comfort and minimize trajectory error. All of these algorithms work in sun or rain and during the day or night. With these systems operating together, Junior has successfully logged hundreds of miles of autonomous operation in a variety of real-life conditions.

We present the Yoneda Lemma in terms of categories without explicit reference to the notion of functor. From this perspective we then define a commune as a common generalization of Chu spaces and presheaves, and give some applications.

We review the conceptual development of (true) concurrency and branching time starting from Petri nets and proceeding via Mazurkiewicz traces, pomsets, bisimulation, and event structures up to higher dimensional automata (HDAs), whose acyclic case may be identified with triadic event structures and triadic Chu spaces. Acyclic HDAs may be understood as extending the two truth values of Boolean logic with a third value .

We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection with the binary logical transformations of the corresponding operations on the category of Chu spaces on a two-letter alphabet.

We consider tractable and intractable cases of the satisfiability problem for conjunctions of inequalities between variables and constants in a fixed finite poset. We show that crowns are intractable. We study members and closure properties of the cl

We give a uniform representation of the objects of mathematical practice as Chu spaces, forming a concrete self dual bicomplete closed category and hence a constructive model of linear logic. This representation distributes mathematics over a two dimensional space called the Stone gamut. The Stone gamut is coordinatized horizontally by coherence, ranging from -1 for sets to 1 for complete atomic Boolean algebras (CABA's), and vertically by complexity of language. Complexity 0 contains only sets, CABA's, and the inconsistent empty set. Complexity 1 admits noninteracting set CABA pairs. The entire Stone duality menagerie of partial distributive lattices enters at complexity 2. Groups, rings, fields, graphs, and categories are all entered by level 16, and every category of relational structures and their homomorphisms eventually appears. The key is the identification of continuous functions and homomorphisms, which puts Stone Pontrjagin duality on a uniform basis by merging algebra and topology into a simple common framework.

We represent concurrent processes as Boolean propositions or gates, cast in the role of accepters of concurrent behavior. This properly extends other mainstream representations of concurrent behavior such as event structures, yet is defined more simply. It admits an intrinsic notion of duality that permits processes to be viewed as either schedules or automata. Its algebraic structure is essentially that of linear logic, with its morphisms being consequence-preserving renamings of propositions, and with its operations forming the core of a natural concurrent programming language.>

The genesis of the calculus of binary relations, which was introduced by A. De Morgan (1860) and was subsequently greatly developed by C.S. Peirce (1933) and E. Schroder (1895), is examined. Its further development, from the perspective of modern model theory, in the 1940s and 1950s is described.>

The phenomena of branching time and true or noninterleaving concurrency find their respective homes in automata and schedules.But these two models of computation are formally equivalent via Birkhoff duality, an equivalence we expound on here in tutorial detail.So why should these phenomena prefer one over the other?We identify dimension as the culprit: l-dimensional automata are skeletons permitting only interleaving concurrency, whereas true n-fold concurrency resides in transitions of dimension n.The truly concurrent automaton dual to a schedule is not a skeletal distributive lattice but a solid one!We introduce true nondeterminism and define it as monoidal homotopy; from this perspective nondeterminism in ordinary automata arises from forking and joining creating nontrivial homotopy, The automaton dual to a poset schedule is simply connected whereas that dual to an event structure schedule need not be, according to monoidal homotopy though not to group homotopy.We conclude with a formal definition of higher dimensional automaton as an n-complex or n-category, whose two essential axioms are associativity of concatenation within dimension and an interchange principle between dimensions. 1 Background A central problem in the semantics of imperative computation is the construction of convenient models of computation embodying the apparent aspects of both branching time and true or noninterleaving or causal t

An adaptive forward differencing algorithm is presented for rapid rendering of cubic curves and bicubic surfaces. This method adjusts the forward difference step size so that approximately one pixel is generated along an ordinary or rational cubic curve for each forward difference step. The adjustment involves a simple linear transformation on the coefficients of the curve which can be accomplished with shifts and adds. This technique combines the advantages of traditional forward differencing and adaptive subdivision. A hardware implementation approach is described including the adaptive control of a forward difference engine. Surfaces are rendered by drawing many curves spaced closely enough together so that no pixels are left unpainted. A simple curve anti-aliasing algorithm is also presented in this paper. Anti-aliasing cubic curves is supported via tangent vector output at each forward difference step. The adaptive forward differencing algorithm is also suitable for software implementation.

In the course of developing a system for fitting smooth curves to camera input we have developed several direct (i.e. noniterative) methods for fitting a shape (line, circle, conic, cubic, plane, sphere, quadric, etc.) to a set of points, namely exact fit, simple fit, spherical fit, and blend fit. These methods are all dimension-independent, being just as suitable for 3D surfaces as for the 2D curves they were originally developed for.Exact fit generalizes to arbitrary shapes (in the sense of the term defined in this paper) the well-known determinant method for planar exact fit. Simple fit is a naive reduction of the general overconstrained case to the exact case. Spherical fit takes advantage of a special property of circles and spheres that permits robust fitting; no prior direct circle fitters have been as robust, and there have been no previous sphere fitters. Blend fit finds the best fit to a set of points of a useful generalization of Middleditch-Sears blending curves and surfaces, via a nonpolynomial generalization of planar fit.These methods all require (am+bn)n2 operations for fitting a surface of order n to m points, with a = 2 and b = 1/3 typically, except for spherical fit where b is larger due to the need to extract eigenvectors. All these methods save simple fit achieve a robustness previously attained by direct algorithms only for fitting planes. All admit incremental batched addition and deletion of points at cost an2 per point and bn3 per batch.

No abstract available.

A number of techniques are presented for making conic splines more effective for 2D computer graphics. We give a brief account of the theory of conic splines oriented to computer graphics. We make Pitteway's algorithm exact, and repair an "aliasing" problem that has plagued the algorithm since its introduction in 1967. The curvature-matching problem for conics is solved by way of a simple formula for curvature at an endpoint which permits curvature to be matched exactly at non-inflectior points and more closely than was previously realized possible at points of inflection. A formula for minimum-curvature-variation of conic splines is given. These techniques provide additional support for Pavlidis' position [6] that conics can often be very effective as splines.The work was motivated by, and provides much of the foundation for, an implementation of conic splines at Sun Microsystems as part of Sun's Pixrect graphics package, the lowest layer of Sun's graphics support.

We describe five paradigm shifts in programming language design, some old and some relatively new, namely Effect to Entity, Serial to Parallel, Partition Types to Predicate Types, Computable to Definable, and Syntactic Consistency to Semantic Consistency. We argue for the adoption of each. We exhibit a programming language, Viron, that capitalizes on these shifts.

We describe a model of net-connected processes that amounts to a reformulation of a model derived by Brock and Ackerman from the Kahn-McQueen model of processes as relations on streams of data. The reformulation leads directly to a straightforward definition of process composition. Our notion of processes and their composition constitutes a natural generalization of the notion of functions and their composition. We apply this definition of process composition to the development of an algebra of processes, which we propose as supplying a formal semantics for a language whose domain of discourse includes nets of interconnected processes. This in turn leads us to logics of such nets, about which we raise three open and fundamental problems: existence of a finite basis for the operations of the language, finite axiomatizability of the equational theory, and decidability of this theory. A natural generalization of the model deals with the time complexity of computations.

We describe a mu-calculus which amounts to modal logic plus a minimization operator, and show that its satisfiability problem is decidable in exponential time. This result subsumes corresponding results for propositional dynamic logic with test and converse, thus supplying a better setting for those results. It also encompasses similar results for a logic of flowgraphs. This work provides an intimate link between PDL as defined by the Segerberg axioms and the mu-calculi of de Bakker and Park.

When the "binding mechanisms" of assignment, quantification, and procedure definition are removed from a conventional first order total correctness logic of programs, the remaining logical system is decidable in time approximately one exponential in the length of the input. This system is maximal in the sense that the presence of any one of the three binding mechanisms would make it undecidable. Such a decision procedure can play a central role in the construction of program verifiers based on decision methods.

A linear implementation of the optimal universal data compression methods of Lempel and Ziv is described.The main tool is McCreight's algorithm for constructing suffix trees.Both bounded and unbounded memory are considered.

The goal of automatic program verification is to prove programs correct formally. We argue that the existing notions of formal proof are too syntactic and as such too intimately bound up with details of low-level computation. We propose a more semantic notion of formal proof which nevertheless pays due respect to the problem of effectiveness in proof checking. Such a notion supplies a more practical basis for the specification of verifiers than do extant approaches. In particular the problem of constructing verifiers according to our approach is reduced entirely to routine development and implementation of decision methods, while permitting shorter proofs and yet remaining easy to develop proofs with.

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 closure. (ii) Every free dynamic algebra can be factored into finite dynamic algebras. (iii) Every finite dynamic algebra is isomorphic to a Kripke structure. (ii) and (iii) imply Parikh's completeness theorem for the Segerberg axioms. We also present an approach to treating the inductive aspect of recursion within dynamic algebras.

We briefly survey the major proposals for models of programs and show that they all lead to the same propositional theory of programs. Methods of algebraic logic dominate in the proofs. One of the connections made between the models, that involving language models, is quite counterintuitive. The common theory has already been shown to be complete in deterministic exponential time; we give here a simpler proof of the upper bound.

We discuss problems arising in reasoning about on-going processes, using the modal constructs after, throughout, during, and preserves. Earlier work established decidability of the theory whose language included only the first two of these, along with program connectives | , ; and *. Here we give a complete Gentzen-type axiomatizations for useful combinations of the other modalities. We also indicate how such Gentzen-type axiomatizations lead to deterministic exponential time upper bounds on the complexity of decision procedures for these languages. It remains an open problem how to completely axiomatize the combination of modalities during and preserves.

We investigate the principles underlying reasoning about nondeterministic programs, and present a logic to support this kind of reasoning. Our logic, an extension of dynamic logic ([22] and [12]), subsumes most existing first-order logics of nondeterministic programs, including that developed by Dijkstra based on the concept of weakest precondition. A significant feature is the strict separation between the two kinds of nonterminating computations: infinite computations and failures. The logic has a Tarskian truth-value semanics, an essential prerequisite to establishing completeness of axiomatizations of the logic. We give an axiomatization for flowchart (regular) programs that is complete relative to arithmetic in the sense of Cook. Having a satisfactory tool at hand, we turn to the clarification of the concept of the total correctness of nondeterministic programs, providing in passing, a critical evaluation of the widely used "predicate transformer" approach to the definition of programming constructs, initiated by Dijkstra [5]. Our axiom system supplies a complete axiomatization of wp.

We give a new characterization of the set of satisfiable formulae of propositional dynamic logic (PDL) based on the method of tableaux. From it we derive a heuristically efficient goal-directed proof procedure and a complete axiom system for PDL. The proof procedure illustrates a striking connection between natural deduction and symbolic execution. The completeness proof for the axiom system incorporates a method for the automatic synthesis of invariants. We also augment DL with new modalities throughout, during, and preserves, supply a new semantic foundation for DL programs, and show how to extend the satisfiability characterizations for PDL to throughout.

We consider the problem of automating some of the duties of programmers. We take as our point of departure the claim that data management has been automated to the point where the programmer concerned only about the correctness (as opposed to the efficiency) of his program need not involve himself in any aspect of the storage allocation problem. We focus on what we feel is a sensible next step, the problem of automating aspects of control. To accomplish this we propose a definition of control based on a fact/heuristic dichotomy, a variation of Chomsky's competence/performance dichotomy. The dichotomy formalizes an idea originating with McCarthy and developed by Green, Hewitt, McDermott, Sussman, Hayes, Kowalski and others. It allows one to operate arbitrarily on the control component of a program without affecting the program's correctness, which is entirely the responsibility of the fact component. The immediate objectives of our research are to learn how to program keeping fact and control separate, and to identify those aspects of control amenable to automation.

Dynamic logic is a generalization of first order logic in which quantifiers of the form “for all χ...” are replaced by phrases of the form “after executing program α...”. This logic subsumes most existing first-order logics of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness, yet is more closely related to classical first-order logic than any other proposed logic of programs. We consider two issues: how hard is the validity problem for the formulae of dynamic logic, and how might one axiomatize dynamic logic? We give bounds on the validity problem for some special cases, including a Π02-completeness result for the partial correctness theories of uninterpreted flowchart programs. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic.

An algorithm is presented which finds all occurrences of one given string within another, in running time proportional to the sum of the lengths of the strings. The constant of proportionality is low enough to make this algorithm of practical use, and the procedure can also be extended to deal with some more general pattern-matching problems. A theoretical application of the algorithm shows that the set of concatenations of even palindromes, i.e., the language $\{\alpha \alpha ^R\}^*$, can be recognized in linear time. Other algorithms which run even faster on the average are also considered.

This paper deals with logics of programs. The objective is to formalize a notion of program description, and to give both plausible (semantic) and effective (syntactic) criteria for the notion of truth of a description. A novel feature of this treatment is the development of the mathematics underlying Floyd-Hoare axiom systems independently of such systems. Other directions that such research might take are also considered. This paper grew out of, and is intended to be usable as, class notes [27] for an introductory semantics course. The three sections of the paper are: 1. A framework for the logic of programs. Programs and their partial correctness theories are treated as binary relations on states and formulae respectively. Truth-values are assigned to partial correctness assertions in a plausible (Tarskian) but not directly usable way. 2. Particular Programs. Effective criteria for truth are established for some programs using the Tarskian criteria as a benchmark. This leads directly to a sound, complete, effective axiom system for the theories of these programs. The difficulties involved in finding such effective criteria for other programs are explored. The reader's attention is drawn to Theorems 4, 16, 18 and 22-24, as worthy of mention even out of the context in which they now appear. 3. Variations and extensions of the framework. Alternatives to binary relations for both programs and theories are speculated on, and their possible roles in semantics are considered. We discuss a hierarchy of varieties of programs and the importance of this hierarchy to the issues of definability and describability. Modal logic is considered as a first-order alternative to Floyd-Hoare logic. We give an appropriate axiom system which is complete for loop-free programs and also puts conventional predicate calculus in a different light by lumping quantifiers with non-logical assignments rather than treating them as logical concepts. Proofs of all theorems are relegated to an appendix.

Consider n processes operating asynchronously in parallel, each of wich maintains a single "special" variable which can be read (but not written) by the other processes. All coordination between processes is to be accomplished by means of the execution of the primitive operations of a process (1) reading another process's special variable, and (2) setting its own special variable to some value. A process may "die" at any time, when its special variable is (automatically) set a special "dead" value. A dead process may revive. Reading a special variable which is being simultaneously written returns either the old or the new value. Each process may be in a certain "critical" state (which it leaves if it dies). We present a coordination scheme with the following properties. (1) At most one process is ever in its critical state at a time. (2) If a process wants to enter its critical state, it may do so before any other process enters its critical state more than once. (3) The special variables are bounded in value. (4) Some process wanting to enter its critical state can always make progress to that goal. By the definition of the problem, no process can prevent another from entering its critical state by repeatedly failing and restarting. In the case of two processes, what makes our solution of particular interest is its remarkable simplicity when compared with the extant solutions to this problem. Our n-process solution uses the two-process solution as a subroutine, and is not quite as elegant as the two-process solution.

To within a constant factor, only two complexity classes of complete binary bases exist. We show that they are separated by at most O(nlog310), or about O(n2.095), complementing a result of Khrapchenko that establishes an order n2 lower bound.

To prove that a number n is composite, it suffices to exhibit the working for the multiplication of a pair of factors. This working, represented as af string, is of length bounded by a polynomial in $\log _2 n$. We show that the same property holds for the primes. It is noteworthy that almost no other set is known to have the property that short proofs for membership or nonmembership exist for all candidates without being known to have the property that such proofs are easy to come by. It remains an open problem whether a prime n can be recognized in only $\log _2^\alpha n$ operations of a Turing machine for any fixed $\alpha $. The proof system used for certifying primes is as follows. Axiom. $(x,y,1)$. Inference Rules. \[ R_1 :\quad(p,x,a),q \vdash (p,x,qa)\quad\text{provided }x^{(p - 1)/q} \not\equiv 1(\bmod p)\text{ and }q | (p - 1). \]\[ R_2 :\quad(p,x,p - 1) \vdash p\quad\text{provided } x^{p - 1} \equiv 1(\bmod p). \] Theorem 1. pis a theorem$\equiv p$is a prime. Theorem 2. pis a theorem$\supset p$has a proof of$\lceil {4\log _2 p} \rceil $lines.

We show that $n^3 $ distinct and-gate inputs appear in any circuit constructed from and-gates and or-gates that computes the product of two $n \times n$ Boolean matrices. Using not-gates as well, it is possible to realize a circuit for this problem using only $O(n^{\log _2 7} \log ^2 n)$ gates, whence we infer a much larger complexity gap between and-or and and-or-not circuits than was previously known.

We are interested in combinational circuits synthesized from and-gates and or-gates. We first show that n3 distinct and-gate inputs are needed to form the product of two Boolean matrices, and hence O(n3) two-input and-gates are needed to compute the transitive closure of a Boolean matrix. While this result has the flavor of Kerr's (achievable)lower bound [Kerr 1970] of n3+-gates for computing the min/+ product of integer-valued matrices using only min-gates and +-gates, the problem turns out on closer inspection to be considerably more subtle, and in fact we have been able to come only to within a factor of two of the best known upper bound of n3and-gates.

Random access machines (RAMs) are usually defined to have registers that hold integers. While this captures in part the structure of a commercial computer, it overlooks an implementation-dependent feature of most binary oriented machines, namely their ability to operate bit by bit on the bit vectors used to represent integers. Typical operations are bit-wise Boolean operations (and, or, not, etc.) and shifts by an amount specified in some register. These operations are ideal for certain problems, such as dealing with sets represented as bit vectors, some parsing algorithms [4], propositional calculus theorem proving, and analysis of sorting networks. A RAM so implemented we shall call a vector machine.

Article Free Access Share on Top down operator precedence Author: Vaughan R. Pratt Massachusetts Institute of Technology Massachusetts Institute of TechnologyView Profile Authors Info & Claims POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languagesOctober 1973 Pages 41–51https://doi.org/10.1145/512927.512931Online:01 October 1973Publication History 25citation3,168DownloadsMetricsTotal Citations25Total Downloads3,168Last 12 Months170Last 6 weeks70 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

A memory may be regarded as a computer with input, output and storage facilities, but with no explicit functional capability. The only possible outputs are permutations of a multiset of its inputs. Thus the natural question to ask of a class of memories is, what permutations can its members compute?

New upper and lower bounds are presented for the maximum number of comparisons, f(i,n), required to select the i-th largest of n numbers. An upper bound is found, by an analysis of a new selection algorithm, to be a linear function of n: