The papers on this page are listed in approximately reverse chronological order. My joint papers with Yuri Gurevich are also available (in PDF form) from his web site.
Two forms of one useful logic: Existential fixed point logic and liberal datalog, joint with Yuri Gurevich (to appear in Bull. European Assoc. Theoret. Comp. Sci.)
A natural liberalization of Datalog is used in the Distributed Knowledge Authorization Language (DKAL). We show that the expressive power of this liberal Datalog is that of existential fixed-point logic. The exposition is self-contained.
When are two algorithms the same?, joint with Nachum Dershowitz and Yuri Gurevich
People usually regard algorithms as more abstract than the programs that implement them. The natural way to formalize this idea is that algorithms are equivalence classes of programs with respect to a suitable equivalence relation. We argue that no such equivalence relation exists.
Zero-one laws: Thesauri and parametric conditions, joint with Yuri Gurevich (Bull. European Assoc. Theoret. Comp. Sci. 91 (2007) 125-144)
The 0-1 law for first-order properties of finite structures and its proof via extension axioms were first obtained in the context of arbitrary finite structures for a fixed finite vocabulary. But it was soon observed that the result and the proof continue to work for structures subject to certain restrictions. Examples include undirected graphs, tournaments, and pure simplicial complexes. We discuss two ways of formalizing these extensions, Oberschelp's (1982) parametric conditions and our (2003) thesauri. We show that, if we restrict thesauri by requiring their probability distributions to be uniform, then they and parametric conditions are equivalent. Nevertheless, some situations admit more natural descriptions in terms of thesauri, and the thesaurus point of view suggests some possible extensions of the theory.
Program termination and well partial orderings, joint with Yuri Gurevich
The following observation may be useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U_1, . . . ,U_n then R is well-founded. A question arises how to bound the ordinal height |R| of the relation R in terms of the ordinals alpha_i = |U_i|. We introduce the notion of the stature ||P|| of a well partial ordering P and show that |R| is at most ||alpha_1 x . . . x alpha_n|| and that this bound is tight. The notion of stature is of considerable independent interest. We define ||P|| as the ordinal height of the forest of nonempty bad sequences of P, but it has many other natural and equivalent definitions. In particular, ||P|| is the supremum, and in fact the maximum, of the lengths of linearizations of P. And ||alpha_1 x . . . x \alpha_n|| is equal to the natural product of alpha_1, . . . , alpha_n.
General interactive small-step algorithms, joint with Yuri Gurevich, Dean Rosenzweig, and Benjamin Rossman
Because of the journal's length limitations, this paper is in two parts. Part 1 (pdf) Part 2 (pdf)
In earlier work, the Abstract State Machine Thesis --- that arbitrary algorithms are behaviorally equivalent to abstract state machines --- was established for several classes of algorithms, including ordinary, interactive, small-step algorithms. This was accomplished on the basis of axiomatizations of these classes of algorithms. Here we extend the axiomatization and the proof to cover interactive small-step algorithms that are not necessarily ordinary. This means that the algorithms (1) can complete a step without necessarily waiting for replies to all queries from that step and (2) can use not only the environment's replies but also the order in which the replies were received. In order to prove the thesis for algorithms of this generality, we extend the definition of abstract state machines to incorporate explicit attention to the relative timing of replies and to the possible absence of replies.
Ordinary small-step interactive algorithms, II, joint with Yuri Gurevich (to appear in the A.C.M. Transactions on Computational Logic)
This is the second in a series of three papers extending the proof of the Abstract State Machine Thesis --- that arbitrary algorithms are behaviorally equivalent to abstract state machines --- to algorithms that can interact with their environments during a step rather than only between steps. As in the first paper of the series, we are concerned here with ordinary, small-step, interactive algorithms. This means that the algorithms (1) proceed in discrete, global steps, (2) perform only a bounded amount of work in each step, (3) use only such information from the environment as can be regarded as answers to queries, and (4) never complete a step until all queries from that step have been answered. After reviewing the previous paper's formal description of such algorithms and the definition of behavioral equivalence, we define ordinary, interactive, small-step abstract state machines (ASM's). Except for very minor modifications, these are the machines commonly used in the ASM literature. We define their semantics in the framework of ordinary algorithms, and we show that they satisfy the postulates for these algorithms. This material lays the groundwork for the final paper in the series, in which we shall prove the Abstract State Machine Thesis for ordinary, interactive, small-step algorithms: All such algorithms are equivalent to ASMs.
Ordinary small-step interactive algorithms, III, joint with Yuri Gurevich (to appear in the A.C.M. Transactions on Computational Logic)
This is the third in a series of three papers extending the proof of the Abstract State Machine Thesis --- that arbitrary algorithms are behaviorally equivalent to abstract state machines --- to algorithms that can interact with their environments during a step rather than only between steps. As in the first two papers of the series, we are concerned here with ordinary, small-step, interactive algorithms. This means that the algorithms (1) proceed in discrete, global steps, (2) perform only a bounded amount of work in each step, (3) use only such information from the environment as can be regarded as answers to queries, and (4) never complete a step until all queries from that step have been answered. After reviewing the previous papers' definitions of such algorithms, of behavioral equivalence, and of abstract state machines (ASMs), we prove the main result: Every ordinary, interactive, small-step algorithm is behaviorally equivalent to an ASM. We also discuss some possible variations of and additions to the ASM semantics.
Play to test, joint with Yuri Gurevich, Lev Nachmanson and Margus Veanes
Testing tasks can be viewed (and organized!) as games against nature. We study reachability games in the context of testing. Such games are ubiquitous. A single industrial test suite may involve many instances of a reachability game. Hence the importance of optimal or near optimal strategies for reachability games. One can use linear programming or the value iteration method of Markov decision process theory to find optimal strategies. Both methods have been implemented in an industrial model-based testing tool, Spec Explorer, developed at Microsoft Research.
NP-Completeness of Deciding Binary Genetic Encodability, joint with Boris Mitavskiy (in Foundations of Genetic Algorithms: 8th International Workshop, FOGA 2005, Aizu-Wakamatsu City, Japan, 2005, Revised Selected Papers, edited by A. H. Wright, M. D. Vose, K. A. De Jong, and L. M. Schmitt, Springer Lecture Notes in Computer Science 3469 (2005) 58-74)
In previous work of the second author a rigorous mathematical foundation for re-encoding one evolutionary search algorithm by another has been developed. A natural issue to consider then is the complexity of deciding whether or not a given evolutionary algorithm can be re-encoded by one of the standard classical evolutionary algorithms such as a binary genetic algorithm. In the current paper we prove that, in general, this decision problem is NP-complete.
Why sets?, joint with Yuri Gurevich, (Bull. European Assoc. Theoret. Comp. Sci. 87 (2004) 139-156)
Sets play a key role in foundations of mathematics. Why? To what extent is it an accident of history? Imagine that you have a chance to talk to mathematicians from a far away planet. Would their mathematics be set-based? What are the alternatives to the set-theoretic foundation of mathematics? Besides, set theory seems to play a significant role in computer science, in particular in database theory and formal methods. Is there a good justification for that? We discuss these and some related issues.
Ordinary Intra-Step Interactive Algorithms, I, joint with Yuri Gurevich (to appear in the A.C.M. Transactions on Computational Logic)
PostScript or PDF
This is the first in a series of papers extending the Abstract State Machine Thesis -- that arbitrary algorithms are behaviorally equivalent to abstract state machines -- to algorithms that can interact with their environments during a step rather than only between steps. In the present paper, we describe, by means of suitable postulates, those interactive algorithms that (1) proceed in discrete, global steps, (2) perform only a bounded amount of work in each step, (3) use only such information from the environment as can be regarded as answers to queries, and (4) never complete a step until all queries from that step have been answered. We indicate how a great many sorts of interaction meet these requirements. We also discuss in detail the structure of queries and replies and the appropriate definition of equivalence of algorithms. Finally, motivated by our considerations concerning queries, we discuss a generalization of first-order logic in which the arguments of function and relation symbols are not merely tuples of elements but orbits of such tuples under groups of permutations of the argument places.
Algorithms: A Quest for Absolute Definitions, joint with Yuri Gurevich (Bull. European Assoc. Theoret. Comp. Sci. 81 (2003) 195-225)
PostScript or PDF
What is an algorithm? The interest in this foundational problem is not only theoretical; applications include specification, validation and verification of software and hardware systems. We describe the quest to understand and define the notion of algorithm. We start with the Church-Turing thesis and contrast Church's and Turing's approaches, and we finish with some recent investigations.
Pairwise Testing, joint with Yuri Gurevich (Bull. European Assoc. Theoret. Comp. Sci. 78 (2002) 100-132)
PostScript or PDF
We discuss the following problem, which arises in software testing. Given some independent parameters (of a program to be tested), each having a certain finite set of possible values, we intend to test the program by running it several times. For each test, we give the parameters some (intelligently chosen) values. We want to ensure that for each pair of distinct parameters, every pair of possible values is used in at least one of the tests. And we want to do this with as few tests as possible. Much of this paper is a survey of known ideas, which we rediscovered.
Algorithms vs. Machines, joint with Yuri Gurevich (Bull. European Assoc. Theoret. Comp. Sci. 77 (2002) 96-118)
PostScript or PDF
Yiannis Moschovakis argues that some algorithms, and in particular the mergesort algorithm, cannot be adequately described in terms of machines acting on states. We show how to describe the mergesort algorithm, on its natural level of abstraction, in terms of distributed abstract state machines.
Abstract State Machines Capture Parallel Algorithms, joint with Yuri Gurevich (A.C.M. Transactions on Computational Logic 4 (2003) 578-651)
PostScript or PDF
We give an axiomatic description of parallel, synchronous algorithms. Our main result is that every such algorithm can be simulated, step for step, by an abstract state machine with a background that provides for multisets.
Abstract State Machines Capture Parallel Algorithms: Correction and Extension, joint with Yuri Gurevich (A.C.M. Transactions on Computational Logic, to appear).
In our previous paper on this topic, we were too timid in formulating the axioms; they did not allow a parallel algorithm to create components on the fly. This restriction did not hinder us from proving that the usual parallel models, like circuits or PRAMs or even alternating Turing machines, satisfy the postulates. But it resulted in an error in our attempt to prove that parallel ASMs always satisfy the postulates. To correct the error, we liberalize our axioms and allow on-the-fly creation of new parallel components. We believe that the improved axioms accurately express what parallel algorithms ought to be. We prove the parallel thesis for the new, corrected notion of parallel algorithms, and we check that parallel ASMs satisfy the new axioms.
On Polynomial Time Computation Over Unordered Structures, joint with Yuri Gurevich and Saharon Shelah (J. Symbolic Logic 67 (2002) 1093-1125)
PostScript or PDF
This paper is motivated by the question whether there exists a logic capturing polynomial time computation over unordered structures. We consider several algorithmic problems near the border of the known, logically defined complexity classes contained in polynomial time. We show that fixpoint logic plus counting is stronger than might be expected, in that it can express the existence of a complete matching in a bipartite graph. We revisit the known examples that separate polynomial time from fixpoint plus counting. We show that the examples in a paper of Cai, Fuerer, and Immerman, when suitably padded, are in choiceless polynomial time yet not in fixpoint plus counting. Without padding, they remain in polynomial time but appear not to be in choiceless polynomial time plus counting. Similar results hold for the multipede examples of Gurevich and Shelah, except that their final version of multipedes is, in a sense, already suitably padded. Finally, we describe another plausible candidate, involving determinants, for the task of separating polynomial time from choiceless polynomial time plus counting.
Strong Extension Axioms and Shelah's Zero-One Law for Choiceless Polynomial Time, joint with Yuri Gurevich (J. Symbolic Logic 68 (2003) 65-131)
PostScript or PDF
This paper developed from Shelah's proof of a zero-one law for the complexity class "choiceless polynomial time," defined by Shelah and the authors. We present a detailed proof of Shelah's result for graphs, and describe the extent of its generalizability to other sorts of structures. The extension axioms, which form the basis for earlier zero-one laws (for first-order logic, fixed-point logic, and finite-variable infinitary logic) are inadequate in the case of choiceless polynomial time; they must be replaced by what we call the strong extension axioms. We present an extensive discussion of these axioms and their role both in the zero-one law and in general.
A New Zero-One Law and Strong Extension Axioms, joint with Yuri Gurevich (Bull. European Assoc. Theoret. Comp. Sci. 72 (2000) 103-122)
PostScript or PDF
This article is a part of the continuing column on Logic in Computer Science. One of the previous articles in the column was devoted to the zero-one laws for a number of logics playing prominent roles in finite model theory: first-order logic FO, the extension FO+LFP of first-order logic with the least fixed-point operator, and the infinitary logic where every formula uses finitely many variables. Recently Shelah proved a new, powerful, and surprising zero-one law. His proof uses so-called strong extension axioms. Here we formulate Shelah's zero-one law and prove a few facts about these axioms. In the process we give a simple proof for a "large deviation" inequality a la Chernoff.
Inadequacy of Computable Loop Invariants, joint with Yuri Gurevich (A. C. M. Trans. Computational Logic 2 (2001) 1-11)
PostScript or PDF
Hoare logic is a widely recommended verification tool. There is, however, a problem of finding easily-checkable loop invariants; it is known that decidable assertions do not suffice to verify WHILE programs, even when the pre- and post-conditions are decidable. We show here a stronger result: decidable invariants do not suffice to verify single-loop programs. We also show that this problem arises even in extremely simple contexts. Let N be the structure consisting of the set of natural numbers together with the functions S(x)=x+1, D(x)=2x and H(x) equal to x/2 rounded down. There is a single-loop program P using only three variables x,y,z such that the asserted program "x=y=z=0 P false" is partially correct on N but any loop invariant I(x,y,z) for this asserted program is undecidable.
Choiceless Polynomial Time Computation and the Zero-One Law, joint with Yuri Gurevich (Computer Science Logic (14th International Workshop, CSL 2000, Annual Conference of the EACSL, Fischbachau, Germany, August 2000, Proceedings) (ed. P. G. Clote and H. Schwichtenberg) Springer Lecture Notes in Computer Science 1862 (2000) 18-42)
PostScript or PDF
This paper is a sequel to "Choiceless Polynomial Time," a commentary on Saharon Shelah's "Choiceless Polynomial Time Logic: Inability to Express", and an abridged version of "Strong Extension Axioms and Shelah's Zero-One Law for Choiceless Polynomial Time." The last of these contains complete proofs of all the results presented here. The BGS model of computation was defined in "Choiceless Polynomial Time" with the intention of modeling computation with arbitrary finite relational structures as inputs, with essentially arbitrary data structures, with parallelism, but without arbitrary choices. It was shown that choiceless polynomial time, the complexity class defined by BGS programs subject to a polynomial time bound, does not contain the parity problem. Subsequently, Shelah proved a zero-one law for choiceless-polynomial-time properties. A crucial difference from the earlier results is this: Almost all finite structures have no non-trivial automorphisms, so symmetry considerations cannot be applied to them. Shelah's proof therefore depends on a more subtle concept of partial symmetry. After struggling for a while with Shelah's proof, we worked out a presentation which we hope will be helpful for others interested in Shelah's ideas. We also added some related results, indicating the need for certain aspects of the proof and clarifying some of the concepts involved in it. Unfortunately, this material is not yet fully written up. The part already written, however, exceeds the space available to us in the present volume. We therefore present here an abridged version of that paper; the full version is "Strong Extension Axioms and Shelah's Zero-One Law for Choiceless Polynomial Time."
Background, Reserve, and Gandy Machines, joint with Yuri Gurevich (Computer Science Logic (14th International Workshop, CSL 2000, Annual Conference of the EACSL, Fischbachau, Germany, August 2000, Proceedings) (ed. P. G. Clote and H. Schwichtenberg) Springer Lecture Notes in Computer Science 1862 (2000) 1-17)
PostScript or PDF
Algorithms often need to increase their working space, and it may be convenient to pretend that the additional space was really there all along but was not previously used. In particular, abstract state machines have, by definition, an infinite reserve. Although the reserve is a naked set, it is often desirable to have some external structure over it. For example, in "Choiceless Polynomial Time," every state was required to include all finite sets of its atoms, all finite sets of these, etc. In this connection, we define the notion of a background class of structures. Such a class specifies the constructions (like finite sets or lists) available as "background" for algorithms. The importation of reserve elements must be non-deterministic, since an algorithm has no way to distinguish one reserve element from another. But this sort of non-determinism is much more benign than general non-determinism. We capture this intuition with the notion of inessential non-determinism. Alternatively, one could insist on specifying a particular one of the available reserve elements to be imported. This is the approach used in [Robin Gandy, "Church's thesis and principles for mechanisms" in: "The Kleene Symposium" (Ed. Jon Barwise et al.), North-Holland, 1980, 123--148.]. The price of this insistence is that the specification cannot be algorithmic. We show how to turn a Gandy-style deterministic, non-algorithmic process into a non-deterministic algorithm of the sort described above, and we prove that Gandy's notion of "structural" for his processes corresponds to our notion of "inessential non-determinism."
The Underlying Logic of Hoare Logic, joint with Yuri Gurevich (Bull. European Assoc. Theoret. Comp. Sci.70 (2000) 82-110)
PostScript or PDF
Formulas of Hoare logic are asserted programs (phi Pi psi) where Pi is a program and phi, psi are assertions. The language of programs varies; in Apt's 1980 survey, one finds the language of while-programs and various extensions of it. But the assertions are traditionally expressed in first-order logic (or extensions of it). In that sense, first-order logic is the underlying logic of Hoare logic. We question the tradition and demonstrate, on the simple example of while-programs, that alternative assertion logics have some advantages. For some natural asertion logics, the expressivity hypothesis in Cook's completeness theorem is automatically satisfied.
Abstract State Machines and Pure Mathematics (Abstract State Machines: Theory and Applications, International Workshop, ASM 2000, Monte Verit\`a, Switzerland, March 2000, Proceedings (ed. Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele) Springer Lecture Notes in Computer Science 1912 (2000) 9-21)
PostScript or PDF
We discuss connections, similarities, and differences between the concepts and issues arising in the study of abstract state machines and those arising in pure mathematics, particularly in set theory and logic. Among the topics from pure mathematics are the foundational role of set theory, permutation models of set theory without the axiom of choice, and interpretations (between theories or vocabularies) regarded as transformations acting on structures.
Abstract State Machines and Computationally Complete Query Languages, joint with Yuri Gurevich and Jan Van den Bussche (Information and Computation, 174 (2002) 20-36) (An earlier version appeared in Abstract State Machines: Theory and Applications, International Workshop, ASM 2000, Monte Verit\`a, Switzerland, March 2000, Proceedings (ed. Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele) Springer Lecture Notes in Computer Science 1912 (2000) 22-33)
PostScript or PDF
Abstract state machines (ASMs) form a relatively new computation model holding the promise that they can simulate any computational system in lockstep. In particular, an instance of the ASM model has recently been introduced for computing queries to relational databases. This model, to which we refer as the BGS model, provides a powerful query language in which all computable queries can be expressed. In this paper, we show that when one is only interested in polynomial-time computations, BGS is strictly more powerful than both QL and while_new, two well-known computationally complete query languages. We then show that when a language such as while_new is extended with a duplicate elimination mechanism, polynomial-time simulations between the language and BGS become possible.
The Logic of Choice, joint with Yuri Gurevich (J. Symbolic Logic 65 (2000) 1264-1310)
PostScript or PDF
We study extensions of first-order logic with the choice construct (choose x : phi(x)). We prove some results about Hilbert's epsilon operator, but in the main part of the paper we consider the case when all choices are independent.
A Variation on the Zero-One Law, joint with Yuri Gurevich, Vladik Kreinovich, and Luc Longpre (Information Processing Letters 67 (1998) 29-30)
PostScript or PDF
Given a decision problem P and a probability distribution over binary strings, for each n, draw independently an instance x(n) of P of length n. What is the probability that there is a polynomial time algorithm that solves all instances x(n)? The answer is: zero or one.
Choiceless Polynomial Time, joint with Yuri Gurevich and Saharon Shelah (Ann. Pure Appl. Logic 100 (1999) 141-187)
PostScript
or
PDF
and addendum (ibid. 112 (2001) 117)PostScript
or
PDF
The question "Is there a computation model whose machines compute exactly polynomial time properties and do not distinguish between isomorphic structures?" became a central question of finite model theory. One of us conjectured the negative answer. A related question is what portion of Ptime can be naturally captured by a computation model. (Notice that we speak about computation whose inputs are arbitrary finite structures e.g. graphs. In the special case of ordered structures, the desired computation model is that of Ptime-bounded Turing machines.) Our idea is to capture the portion of Ptime where algorithms are not allowed arbitrary choice but parallelism is allowed and, in some cases, implements choice. Our computation model is a Ptime version of abstract state machines (formerly called evolving algebras). Our machines are able to Ptime simulate all other Ptime machines in the literature, and they are more programmer-friendly. A more difficult theorem shows that the computation model does not capture all Ptime.
Topoi and Computation (Bull. European Assoc. Theoret. Comp. Sci. 36 (1998) 57-65)
PostScript or PDF
This is the written version of a talk given at the C.I.R.M. Workshop on Logic in Computer Science at Marseille, France in June, 1988. Its purpose is to argue that there is a close connection between the theory of computation and the geometric side of topos theory. We begin with a brief outline of the history and basic concepts of topos theory.
The Linear Time Hierarchy for Abstract State Machines and RAMs, joint with Yuri Gurevich (J. Universal Comp. Sci. 3 (1997) 247-278)
PostScript or PDF
Unlike polynomial time, linear time badly depends on the computation model. In 1992, Neil Jones designed a couple of computation models where the linear-speed-up theorem fails and linear-time computable functions form a proper hierarchy. However, the linear time of Jones' models is too restrictive. We prove linear-time hierarchy theorems for random access machines and Gurevich abstract state machines (formerly called evolving algebras). The latter generalization is harder and more important because of the greater flexibility of the ASM model. One long-term goal of this line of research is to prove linear lower bounds for linear time problems.
Questions and Answers -- A Category Arising in Linear Logic, Complexity Theory, and Set Theory (Advances in Linear Logic (ed. J.-Y. Girard, Y. Lafont, and L. Regnier) London Math. Soc. Lecture Notes 222 (1995) 61-81)
PostScript or PDF
A category used by de Paiva to model linear logic also occurs in Vojtas's analysis of cardinal characteristics of the continuum. Its morphisms have been used in describing reductions between search problems in complexity theory. We describe this category and how it arises in these various contexts. We also show how these contexts suggest certain new multiplicative connectives for linear logic. Perhaps the most interesting of these is a sequential composition suggested by the set-theoretic application.
Evolving Algebras and Linear Time Hierarchy, joint with Yuri Gurevich (13th World Computer Congress 94, Vol.~1 (ed. B. Pehrson and I. Simon) (1994) 383-390)
PostScript or PDF
A precursor of "The Linear Time Hierarchy for Abstract State Machines and RAMs."
Matrix Transformation is Complete for the Average Case, joint with Yuri Gurevich (SIAM J. Computing 24 (1995) 3-29)
PostScript or PDF
We present the first algebraic problem complete for the average case under a natural probability distribution. The problem is this: Given a unimodular matrix X of integers, a set S of linear transformations of such unimodular matrices and a natural number n, decide if there is a product of at most n (not necessarily different) members of S that takes X to the identity matrix.
Randomizing Reductions of Search Problems, joint with Yuri Gurevich (SIAM J. Computing 22 (1993) 949-975)
PostScript or PDF
First, we clarify the notion of a (feasible) solution for a search problem and prove its robustness. Second, we give a general and usable notion of many-one randomizing reductions of search problems and prove that it has desirable properties. All reductions of search problems to search problems in the literature on average case complexity can be viewed as such many-one randomizing reductions. This includes those reductions in the literature that use iterations and therefore do not look many-one.
On the Reduction Theory for Average-Case Complexity, joint with Yuri Gurevich (CSL '90, 4th Workshop on Computer Science Logic (ed. E. Boerger, H. Kleine Buening, and M. Richter) Springer Lecture Notes in Computer Science 533 (1991) 17-30)
PostScript or PDF
A function from instances of one problem to instances of another problem is a reduction if together with any admissible algorithm for the second problem it gives an admissible algorithm for the first problem. This is an example of a decriptive definition of reductions. We simplify slightly Levin's usable definition of determinisitic average-case reductions and thus make it equivalent to the appropriate descriptive definition. Then we generalize this to randomized average-case reductions.