|
[150]
Andreas Blass and Yuri Gurevich and Saharon Shelah [146]
Andreas Blass and Yuri Gurevich [144]
Andreas Blass and Yuri Gurevich [142]
Andreas Blass and Yuri Gurevich Formulas of Hoare logic are asserted programs f P f' where P is a program and f, f' are assertions. The language of programs varies; in the survey [Apt 1980], 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 assertion logics, the expressivity hypothesis in Cook's completeness theorem is automatically satisfied. [141]
Yuri Gurevich We examine sequential algorithms and formulate a Sequential Time Postulate, an Abstract State Postulate, and a Bounded Exploration Postulate. Analysis of the postulates leads us to the notion of sequential abstract state machine and to the theorem in the title. First we treat sequential algorithms that are deterministic and noninteractive. Then we consider sequential algorithms that may be nondeterministic and that may interact with their environments. [140]
Yuri Gurevich, Wolfram Schulte and Charles Wallace We present a mathematically precise, platform-independent model of Java concurrency using the Abstract State Machine method. We cover all aspects of Java threads and synchronization, gradually adding details to the model in a series of steps. We motivate and explain each concurrency feature, and point out subtleties, inconsistencies and ambiguities in the official, informal Java specification. [139]
Andreas Blass, Yuri Gurevich and Jan Van den Bussche 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 [120]. 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. [138]
Yuri Gurevich and Dean Rosenzweig [138]
Yuri Gurevich and Dean Rosenzweig We look at some sources of insecurity and difficulty in reasoning about partially ordered runs of distributed abstract state machines, and propose some techniques to facilitate such reasoning. As a case study, we prove in detail correctness and deadlock--freedom for general partially ordered runs of distributed ASM models of Lamport's Bakery Algorithm. [137]
Giuseppe Del Castillo, Yuri Gurevich and Karl Stroetmann [136]
Yuri Gurevich The thesis is that every sequential algorithm, on any level of abstraction, can be viewed as a sequential abstract state machine. Abstract state machines (ASMs) used to be called evolving algebras. The sequential ASM thesis and its extensions inspired diverse applications of ASMs. The early applications were driven, at least partially, by the desire to test the thesis. Different programming languages were the obvious challenges. (A programming language L can be viewed as an algorithm that runs a given L program on given data.) From there, applications of (not necessarily sequential) ASMs spread into many directions. So far, the accumulated experimental evidence seems to support the sequential thesis. There is also a speculative philosophical justification of the thesis. It was barely sketched in the literature, but it was discussed at much greater length in numerous lectures of mine. Here I attempt to write down some of those explanations. This article does not presuppose any familiarity with ASMs. [135]
Andreas Blass and Yuri Gurevich 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. [134]
Thomas Eiter, Georg Gottlob and Yuri Gurevich We study existential second-order logic over finite strings. For every prefix class C, we determine the complexity of the model checking problem restricted to C. In particular, we prove that, in the case of the Ackermann class, for every formula f, there is a finite automaton A that solves the model checking problem for f. [133]
Erich Graedel, Yuri Gurevich and Colin Hirsch We study the reliability of queries on databases with uncertain information. It turns out that FP^#P is the typical complexity class and that many results generalize to metafinite databases which allow one to use common SQL aggregate functions. [132]
Andreas Blass, Yuri Gurevich, Vladik Kreinovich and
Luc Longpré 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. [131]
Yuri Gurevich We show that every polynomial-time full-invariant algorithm for graphs gives rise to a polynomial-time canonization algorithm for graphs. [130]
Yuri Gurevich and Alex Rabinovich Let phi(X,Y) and psi(Y) range over formulas in the monadic second-order language of order. Let I be the set of integers and F be the family of subsets J of I such that phi(I,J) holds over the real line. The question arises whether, for every phi, the same family F can be defined by means of an appropriate psi(Y) interpreted over the integer order. We answer the question positively. Furthermore, the answer remains positive for every closed subset X of reals, but may be negative for some open subsets. [129]
Yuri Gurevich The draft improves on the ASM syntax. (Appears here because it is used by the ASM community and it is not going to be published.) [128b]
Yuri Gurevich and Andrei Voronkov The journal version of [128a]. [128a]
Yuri Gurevich and Andrei Voronkov We study the monadic case of a decision problem known as simultaneous rigid E-unification. We show its equivalence to an extension of word equations. We prove decidability and complexity results for special cases of this problem. [127b]
A. Degtyarev, Y. Gurevich, P. Narendran, M. Veanes and A. Voronkov The journal version of [127a] containing also a decidability proof for the case of simultaneous rigid E-unification when each rigid equation either contains (at most) one variable or else has a ground left-hand side and the right-hand side of the form x=y where x and y are variables. [127a]
A. Degtyarev, Y. Gurevich, P. Narendran, M. Veanes and A. Voronkov The title problem is proved decidable and in fact EXPTime complete. Furthermore, the problem becomes PTime complete if the number of equations is bounded by any (positive) constant. It follows that the A*EA* fragment of intuitionistic logic with equality is decidable, which contrasts with the undecidability of the EE fragment [126]. Notice that simultaneous rigid E-unification with two variables and only three rigid equations is undecidable [126]. [126]
Yuri Gurevich and Margus Veanes Herbrand's theorem plays a fundamental role in automated theorem proving methods based on tableaux. The crucial step in procedures based on such methods can be described as the corroboration (or Herbrand skeleton) problem: given a positive integer m and a quantifier-free formula, find a valid disjunction of m instantiations of the formula. In the presence of equality (which is the case in this paper), this problem was recently shown to be undecidable. The main contributions of this paper are two theorems. Partisan Corroboration Theorem relates corroboration problems with different multiplicities. Shifted Pairing Theorem is a finite tree-automata formalization of a technique for proving undecidability results through direct encodings of valid Turing machine computations. The theorems are used to explain and sharpen several recent undecidability results related to the orroboration problem, the simultaneous rigid E-unification problem and the prenex fragment of intuitionistic logic with equality. [125]
Anatoli Degtiarev, Yuri Gurevich and Andrei Voronkov The article (written in a popular form) explains that a number of different algorithmic problems related to Herbrand's theorem happen to be equivalent. Among these problems are the intuitinistic provability problem for the existential fragment of first-order logic with equality, the intuitionistic provability problem for the prenex fragment of first-order with equality, and the simultaneous rigid E-unification problem (SREU). The article explains an undecidability proof of SREU and decidability proofs for special cases. It contains an extensive bibliography on SREU. [124]
Natasha Alechina and Yuri Gurevich Logic preservation theorems often have the form of a syntax/semantics correspondence. For example, the Tarski-Los theorem asserts that a first-order sentence is preserved by extensions if and only if it is equivalent to an existential sentence. Many of these correspondences break when one restricts attention to finite models. In such a case, one may attempt to find a new semantical characterization of the old syntactical property or a new syntactical characterization of the old semantical property. The goal of this paper is to provoke such a study. In particular, we give a simple semantical characterization of existential formulas on finite structures. [123]
Yuri Gurevich In one of Krylov's fables, a small dog Moska barks at the elephant who pays no attention whatsoever to Moska. This image comes to my mind when I think of constructive mathematics versus ``classical'' (that is mainstream) mathematics. In this article, we put a few words into the elephant's mouth. The idea to write such an article came to me in the summer of 1995 when I came across a fascinating 1917 bet between the constructivist Hermann Weyl and George Polya, a classical mathematician. An English translation of the bet (from German) is found in the article. Our main objection to the historical constructivism is that it has not been sufficiently constructive. The constructivists have been obsessed with computability and have not paid sufficient attention to the feasibility of algorithms. However, the constructivists' criticism of classical mathematics has a point. Instead of dismissing constructivism offhand, it makes sense to come up with a positive alternative, an antithesis to historical constructivism. We believe that we have found such an alternative. In fact, it is well known and very popular in computer science: the principle of separating concerns. [122]
Charles Wallace, Yuri Gurevich and Nandit Soparkar Previous version: Same authors Failure resilience is an essential requirement for transaction-oriented database systems, yet there has been little effort to specify and verify techniques for failure recovery formally. The desire to improve performance has resulted in algorithms of considerable sophistication, understood by few and prone to errors. In this paper, we show how the formal methodology of Gurevich Abstract State Machines can elucidate recovery and provide formal rigor to the design of a recovery algorithm. In a series of refinements, we model recovery at several levels of abstraction, verifying the correctness of each model. This initial work indicates that our approach can be applied to more advanced recovery mechanisms. [121]
Scott Dexter, Patrick Doyle and Yuri Gurevich We show that, in a strong sense, Schoenhage's storage modification machines are equivalent to unary basic abstract state machines without external functions. The unary restriction can be removed if the storage modification machines are equipped with a pairing function in an appropriate way.
[120]
Andreas Blass, Yuri Gurevich and Saharon Shelah The question "Is there a computation model whose machines do not distinguish between isomorphic structures and compute exactly polynomial time properties?" became a central question of finite model theory. One of us conjectured the negative answer [74]. 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 a 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. [119]
Yuri Gurevich and Marc Spielmann The abstract state machine (ASM) thesis, supported by numerous
applications, asserts that ASMs express algorithms on their natural
abstraction levels directly and essentially coding-free. The only
objection raised to date has been that ASMs are iterative in their
nature, whereas many algorithms are naturally recursive. There seems
to be an inherent contradiction between
Building upon this idea, we suggest a definition of recursive ASMs. The implicit use of distributed computing has an important side benefit: it leads naturally to concurrent recursion. In addition, we reduce recursive ASMs to distributed ASMs. If desired, one can view recursive notation as mere abbreviation. [118]
Andreas Blass and Yuri Gurevich Contrary to 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 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 or research is to prove linear lower bounds for linear time problems. [117]
Yuri Gurevich and James K. Huggins In a provocative paper "Processes are in the Eye of the Beholder" in the same issue of TCS, Lamport points out "the insubstantiality of processes" by proving the equivalence of two different decompositions of the same intuitive algorithm. More exactly, each of the two distributed algorithms is described by a formula in Lamport's favorite temporal logic and then the two formulas are proved equivalent. We point out that the equivalence of algorithms is itself in the eye of the beholder. In this connection, we analyse in what sense the two distributed algorithms are and are not equivalent. Our equivalence proof is direct and does not require formalizing algorithms as logic formulas. [116]
Yuri Gurevich and James K. Huggins We give an evolving algebra (= abstract state machine) solution for the well-known railroad crossing problem and use the occasion to experiment with computations where agents perform instantaneous actions in continuous time and some agents fire at the moment they are enabled. [115]
Thomas Eiter, Georg Gottlob and Yuri Gurevich We prove a new normal form for second-order formulas on finite structures and simplify the Kolaitis-Thakur hierarchy of NP optimization problems. [114]
Yuri Gurevich A decidable problem can be as hard as an undecidable one for all practical purposes. So what is the value of a mere decidablity result? That is the topic discussed in the paper. [113]
Yuri Gurevich and Saharon Shelah This is related to the problem of defining linear order on finite structures. If a linear order is definable on a finite structure A then A is rigid (which means that its only automorphism is the identity). There had been a suspicion that if K is a finitely axiomatizable class of finite structures (that is, more exactly, the collection of all finite structures of a finitely axiomatizable class) and every K structure is rigid, then K permits a relatively simple uniform definition of linear order. The main result of the paper is a probabilistic construction of finite rigid graphs. Using that construction, we exhibit a finitely axiomatizable class of finite rigid structures (called multipedes) such that no L^omega_{infty,omega} sentence phi with counting quantifiers defines a linear order in all the structures. Futhermore, phi does not distingush between a sufficiently large multipede M and a multipede M' obtained from M by moving a "shoe" to another foot of the same segment. [112]
Yuri Gurevich The opening talk at the first workshop on evolving algebras. Sections: Introduction, The EA Thesis, Remarks, Future Work. (Evolving algebras have been later renamed abstract state machines.) [111]
Yuri Gurevich and James K. Huggins The authors present an automated (and implemented) partial evaluator for sequential evolving algebras. (Evolving algebras have been later renamed abstract state machines.) [110]
Andreas Blass and Yuri Gurevich A precursor of [118] [109]
Erich Grädel and Yuri Gurevich Earlier the second author criticized database theorists for admitting arbitrary structures as databases: databases are finite structures [60]. However, a closer investigation reveals that databases are not necessarily finite. For example, a query may manipulate numbers that do not even appear in the database, which shows that a numerical structure is somehow involved. It is true nevertheless that database structures are special. The phenomenon is not restricted to databases; for example think about the natural structure to formalize the traveling salesman problem. To this end, we define metafinite structures. Typically such a structure consists of (i)~a primary part, which is a finite structure, (ii)~a secondary part, which is a (usually infinite) structure e.g. arithmetic or the real line, and (iii)~a set of "weight" functions from the first part into the second. Our logics do not allow quantification over the secondary part. We study definability issues and their relation to complexity. We discuss model-theoretic properties of metafinite structures, present results on descriptive complexity, and sketch some potential applications. [108]
Yuri Gurevich, Neil Immerman and Saharon Shelah Gregory McColm conjectured that, over any class K of finite structures, all positive elementary inductions are bounded if every FOL + LFP formula is equivalent to a first-order formula over K. Here FOL + LFP is the extension of first-order logic with the least fixed point operator. Our main results are two model-theoretic constructions --- one deterministic and one probabilistic --- each of which refutes McColm's conjecture. [107]
Egon Börger, Dean Rosenzweig and Yuri Gurevich The so-called bakery algorithm of Lamport is an ingenious and sophisticated distributed mutual-exclusion algorithm. First we construct a mathematical model A1 which reflects the algorithm very closely. Then we construct a more abstract model A2 where the agents do not interact and the information is provided by two oracles. We check that A2 is safe and fair provided that the oracles satisfy certain conditions. Finally we check that the implementation A1 of A2 satisfies the conditions and thus A1 is safe and fair. [106]
Yuri Gurevich and Raghu Mani An interesting and useful group membership protocol of Flavio Christian involves timing constraints, and its correctness is not obvious. We construct a mathematical model of the protocol and verify the protocol (and notice that tbe assumptions about the environment may be somewhat weakened). [105]
Yuri Gurevich This is a critical analysis of European logic activities in computer science based on a Fall 1992 European tour sponsored by the Office of Naval Research. [104]
Erich Grädel and Yuri Gurevich Complexity classes are easily generalized to the case when inputs of an algorithm are finite ordered structures of a fixed vocabulary rather than strings. A logic L is said to capture (or to be tailored to) a complexity class C if a class of finite ordered structures of a fixed vocabulary belongs to C if and only if it is definable in L. Traditionally, complexity tailored logics are logics of relations. In his FOCS'83 paper, Yuri Gurevich showes that, on finite structures, the class of Logspace computable functions is captured by the primitive recursive calculus, and the class of Ptime computable functions is captured by the classical calculus of partially recursive functions. Here we continue that line of investigation and construct recursive calculi for various complexity classes of functions, in particular for (more challenging) nondeterministic classes NLogspace and NPtime.
[103]
Yuri Gurevich Computation models and specification methods seem to be worlds apart. The evolving algebra project started as an attempt to bridge the gap by improving on Turing's thesis [92]. We sought more versatile machines which would be able to simulate arbitrary algorithms, on their natural abstraction levels, in a direct and essentially coding-free way. The evolving algebra thesis asserts that evolving algebras are such versatile machines. The guide provides the definition of sequential and -- for the first time -- concurrent and distributed evolving algebras. In the same volume, Egon Börger gives an annotated bibliography of evolving algebra applications. (Evolving algebras have been later renamed abstract state machines.) [102]
Yuri Gurevich This humorous article incorporates serious criticism of algebraic and logic approaches to software problems. [101]
Yuri Gurevich With one exception, the chapter is composed of articles published in my column of Bull. Euro. Assoc. for Theor. Comuter Sci. in the period 1988--1992. The only exception is an updated version of the evolving algebra tutorial [92]. [100]
Yuri Gurevich Some computer scientists, notably Steve Cook, identify feasibility with polynomial time computability. We argue against this point of view. [99]
Thomas Eiter, Georg Gottlob and Yuri Gurevich We introduce, study and analyze the complexity of a new nonmonotonic technique of common sense reasoning called curbing. Like circumscription, curbing is based on model minimality but, unlike circumscription, it treats disjunction inclusively. [98]
Yuri Gurevich and Jim Huggins The method of successive refinement is used. The observation that C expressions do not contain statements gives rise to the first evolving algebra which captures the command part of C; expressions are evaluated by an oracle. The second ealgebra implements the oracle under the assumptions that all the necessary declarations have been provided and user-defined functions are evaluated by another oracle. The third ealgebra handles declarations. Finally, the fourth ealgebra revises the combination of the first three by incorporating the stack discipline; it reflects all of C. [97]
Andreas Blass and Yuri Gurevich This is a full paper corresponding to the extended abstract [88] by the second author. 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. A revised and extended version of [88] [96]
Andreas Blass and Yuri Gurevich The journal version of an invited talk at FST&TCS'91, 11th Conference on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India; see Springer Lecture Notes in Computer Science 560 (1991), 10--24. 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. [95]
Yuri Gurevich [Reprinted in ``Current Trends in Theoretical Computer Science'' [94]
Yuri Gurevich We motivate, justify and survey the average case reduction theory. [93]
Andreas Blass and Yuri Gurevich 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. [92]
Yuri Gurevich Computation models and specification methods seem to be worlds apart. The evolving algebra project is as an attempt to bridge the gap by improving on Turing's thesis. We seek more versatile machines able to simulate arbitrary algorithms, on their natural abstraction levels, in a direct and essentially coding-free way. The evolving algebra thesis asserts that evolving algebras are such versatile machines. Here sequential evolving algebras are defined and motivated. In addition, we sketch a speculative ``proof'' of the sequential evolving algebra thesis: Every sequential algorithm can be lock-step simulated by an appropriate sequential evolving algebra on the natural abstraction level of the algorithm. [91]
Yuri Gurevich [Reprinted in ``Current Trends in Theoretical Computer Science'' [90]
Yuri Gurevich [89]
Yuri Gurevich and L. A. Moss We give evolving algebra semantics to the Occam programming language generalizing in the process evolving algebras to the case of distributed concurrent computations. [88]
Yuri Gurevich The first algebraic average-case complete problem is presented. See [97] in this connection. [87]
Yuri Gurevich and Saharon Shelah We develop a technique to prove time-space trade-offs and exhibit natural search problems (e.g. Log-size Clique Problem) that are solvable in linear time on polylog-space (and sometimes even log-space) nondeterministic Turing machine, but no deterministic machine (in a very general sense of this term) with sequential-access read-only input tape and work space n^sigma solves the problem within time n^{1+tau} if sigma + 2tau < 1/2. [86]
Yuri Gurevich [85]
Yuri Gurevich [Reprinted in ``Current Trends in Theoretical Computer Science'' The question P=?NP is the focal point of much research in theoretical computer science. But is it the right question? We find it biased toward the positive answer. It is conceivable that the negative answer is established without providing much evidence for the difficulty of NP problems in practical terms. We argue in favor of an alternative to P=?NP based on the average-case complexity. [84]
Yuri Gurevich [Reprinted in ``Current Trends in Theoretical Computer Science'' Infinite games are widely used in mathematical logic. Recently infinite games were used in connection to concurrent computational processes that do not necessarily terminate. For example, operating system may be seen as playing a game ``against" the disruptive forces of users. The classical question of the existence of winning strategies turns out to be of importance to practice. We explain a relevant part of the infinite game theory. [83]
M. Ajtai and Y. Gurevich First-order logic and datalog are two most important paradigms for relational database query languages. How different are they from the point of view of expressive power? What can be expressed both in first-order logic and datalog? It is easy to see that every existential positive first-order formula is expressible by a bounded datalog query, and the other way round. Cosmadakis suggested that there are no other properties expressible in first-order logic and in datalog, in other words, no unbounded datalog query is expressible in first-order logic. We prove the conjecture; that is our main theorem. It can be seen as a kind of compactness theorem for finite structures. In addition, we give counter-examples delimiting the main result. [82]
Yuri Gurevich and Saharon Shelah The notion of linear time is very sensitive to machine model. In this connection we introduce and study class NLT of functions computable in nearly linear time n(log n)^{O(1)} on random access computers or any other ``reasonable" machine model (with the standard multitape Turing machine model being ``unreasonable" for that low complexity class). This gives a very robust approximation to the notion of linear time. In particular, we give a machine-independent definition of NLT and a natural problem complete for NLT. [81]
Andreas Blass and Yuri Gurevich Yuri Matijasevitch, famous for completing the solution of Hilbert's tenth problem, suggested to use differential equations inspired by real phenomena in nature, to solve the satisfiability problem for boolean formulas. The initial conditions are chosen at random and it is expected that, in the case of a satisfiable formula, the process, described by differential equations, converges quickly to an equilibrium which yields a satisfying assignment. A success of the program would establish NP=R. Attracted by the interesting apprach, we discover serious complications. [80]
Yuri Gurevich and Saharon Shelah There are simple algorithms with large outputs; it is misleading to measure the time complexity of such algorithms in terms of inputs only. In this connection, we introduce the class PIO of functions computable in time polynomial in the maximum of the size of input and the size of output, and some other similar classes. We observe that there is no notation system for any extension of the class of total functions computable on Turing machines in time linear in output and give a machine-independent definition of partial PIO functions. [79]
Yuri Gurevich and Saharon Shelah The interpretation method is the main tool in proving negative results related logical theories. We examine the strength of the interpretation method and find a serious limitation. In one of our previous papers, we were able to reduce true arithmetic to the monadic theory of real line. Here we show that true arithmetic cannot be interpreted in the monadic theory of real line. [78]
Yuri Gurevich [Reprinted in ``Current Trends in Theoretical Computer Science'' [77]
Yuri Gurevich and Jim Morris [76]
Yuri Gurevich We explain and advance Levin's theory of average case complexity. In particular, we exhibit the second natural average-case-complete problem and prove that deterministic reductions are inadequate. [75]
Yuri Gurevich In the classical theory of algorithms, one addresses a computing agent with unbounded resources. We argue in favor of a more realistic theory of multiple addressees with limited resources. [74]
Yuri Gurevich The paper consists of two quite different parts. The first part is a survey (including some new results) on finite model theory. One particular point deserves a special attention. In computer science, the standard computation model is the Turing machine whose inputs are strings; other algorithm inputs are supposed to be encoded with strings. However, in combinatorics, database theory, etc., one usually does not distinguish between isomorphic structures (graphs, databases, etc.). For example, a database query should provide information about the database rather than its implementation. In such cases, there is a problem with string presentation of input objects: there is no known, easily computable string encoding of isomorphism classes of structures. Is there a computation model whose machines do not distinguish between isomorphic structures and compute exactly PTime properties? The question is intimately related to a question by Chandra and Harel in "Structure and complexity of relational queries", J. Comput. and System Sciences 25 (1982), 99-128. We formalize the question as the question whether there exists a logic that captures polynomial time (without presuming the presence of a linear order) and conjecture the negative answer. In the second part we introduce a new computation model: evolving algebras (later renamed abstract state machines). This new approach to semantics of computations and in particulur to semantics of programming languages emphasizes dynamic and resource-bounded aspects of computation. It is illustrated on the example of Pascal. (The second part builds on ``Reconsidering Turing's Thesis: Toward More Realistic Semantics of Programs'', by Yuri Gurevich, University of Michigan, Computing Research Lab, CRL-TR-36-84.) [73]
Andreas Blass and Yuri Gurevich It seems that, in computer science applications, first-order logic (FOL) is rarely the right logic for the purpose. After learning Cook's completeness theorem for Hoare logic, we wondered whether FOL is the right logic for post- and pre-conditiions. Recall that a formula of classical Hoare logic is a triple (F,P,G) where F,G are FOL sentences and P is a while-program. The triple is true (in the partial correctness interpretation) if it satisfies the following condition: For every state A, if A satisfies F and if P, started at A, halts at some state B, then B satisfies G. The states involve arithmetic on natural numbers (or some other basic structure). Hoare gave axioms and rules of inference for Hoare formulas. Since Hoare formula (true, do nothing, G) holds if and only if G is true in the basic structure, Hoare calculus cannot be complete in general. Cook's idea was that such formulas say nothing about programs; let's declare them axioms. That worked and Cook proved the completeness provided that the basic structure is expressive in some techincal sense; arithmetic is expressive. Cook's proof is involved. We have analyzed Cook's proof and distilled existential fixed point logic (EFPL). It turns out that Cook's theorem splits into two theorems. First, we have the completeness theorem, without any expressivity condition, for the version of Hoare's calculus with EFPL instead of FOL. The proof is straightforward. Second, we have a pure logic theorem: in every expressive structure, every FOL formula is equivalent to some EFPL formula. Moreover, EFPL turns out to be very interesting logic in its own right and we prove a number of theorems about it. However, we are not the first to encounter it. Under different names, it had a couple of previous appearances in the literature, in particular in work of Ashok Chandra and David Harel. [72]
M. Ajtai and Y. Gurevich A number of famous theorems about first-order logic were disproved in [60] in the case of finite structures, but Lyndon's theorem on monotone vs. positive resisted the attack. It is defeated here. The counter-example gives a uniform sequence of constant-depth polynomial-size (functionally) monotone boolean circuits not equivalent to any (however nonuniform) sequence of constant-depth polynomial-size positive boolean circuits. [71]
Yuri Gurevich and Saharon Shelah Let G(n,p) be a random graph with n vertices and the edge probability p. We give an algorithm for Hamiltonian Path Problem whose expected run-time on G(n,p) is cn/p + o(n) for any fixed p. This is the best possible result for the case of fixed p. The expected run-time of a slighty modified version of the algorithm remains polynomial if p = p(n) > n_{-c} where c is positive and small. [70]
Yuri Gurevich and Saharon Shelah We prove that the three extensions of first-order logic by means of positive, monotone and inflationary inductions have the same expressive power in the case of finite structures. An extended abstract of the above in Proc. 26th Annual Symposium on Foundation of Computer Science, IEEE Computer Society Press, 1985, 346--353 contains some additions. [69]
Yuri Gurevich [68]
Amnon Barak, Zvi Drezner and Yuri Gurevich Simple probabilistic algorithms enable each active node to find estimates of the fraction of active nodes in the system of n nodes (with a direct communication link between any two nodes) in time o(n). [67]
L. Denenberg, Y. Gurevich and S. Shelah We investigate the expressive power of constant-depth polynomial-size circuit models. In particular, we construct a circuit model whose expressive power is precisely that of first-order logic. [66]
Andreas Blass and Yuri Gurevich We show that almost any non-linear quantifier, applied to quantifier-free first-order formulas, suffices to express an NP- complete predicate; the remaining non-linear quantifiers express exactly co-NL predicates (NL is Nondeterministic Log-space). [65]
Andreas Blass, Yuri Gurevich and D. Kozen The zero-one law, known to hold for first-order logic but not for monadic or even existential monadic second-order logic, is generalized to the extension of first-order logic by the least (or iterative) fixed-point operator. We also show that the problem of deciding, for any pi, whether it is almost sure is complete for exponential time, if we consider only pi's with a fixed finite vocabulary (or vocabularies of bounded arity) and complete for double-exponential time if pi is unrestricted. [64]
Yuri Gurevich We make a case for monadic second-order logic as a rich source of expressive yet manageable theories. Two powerful decidability techniques --- one uses automata and games and the other uses generalized products a la Feferman-Vaught --- and an unusual undecidability method are illustrated. [63]
Yuri Gurevich and Saharon Shelah The main result of the two papers [62, 63] is the decidability of the theory of trees with additional unary predicates and quantification over nodes and branches. This gives the richest decidable branching time logic. [62]
Yuri Gurevich and Saharon Shelah [61]
J. P. Burgess and Yuri Gurevich The main result is the decidability of the temporal theory of the real order. [60]
Yuri Gurevich The pathos of this paper is that classical logic, developed to confront the infinite, is ill prepared to deal with finite structures whereas finite structures, e.g. databases, are of so much importance in computer science. We show that famous theorems about first-order logic fail in the finite case, and discuss various alternatives to classical logic. The message has been heard. [59]
Yuri Gurevich and H. R. Lewis We present an extension of first-order logic that captures precisely the computational complexity of (the uniform sequences of) constant-depth polynomial-time circuits. [58]
W. D. Goldfarb, Yuri Gurevich and Saharon Shelah [57]
Yuri Gurevich and Saharon Shelah Let r be a Cohen real over a model V of ZFC; then the second-order V[r]-theory of the integers (even the reals if V satisfies CH) is interpretable in the monadic V-theory of the real line. Contrast this with the result of [77]. [56]
Andreas Blass and Yuri Gurevich [55]
Andreas Blass and Yuri Gurevich [54]
Yuri Gurevich, L. J. Stockmeyer and Uzi Vishkin Imagine that you need to put service stations (or MacDonald's restaurants) on roads in such a way that every resident is within, say, 10 miles from the nearest station. What is the minimal number of stations and how to find an optimal placement? In general, the problem is NP hard, however in important special cases there are feasible solutions. [53]
Yuri Gurevich and H. R. Lewis The word problem is proven to be undecidable (which provided the necessary mathematical foundation for [41]). [52]
Yuri Gurevich and P. H. Schmitt [51]
Yuri Gurevich It is proven that, under a natural interpretation over finite domains, primitive recursiveness (resp. general recursiveness) coincides with logspace (resp. Ptime) computability. [50]
Yuri Gurevich [49]
A. M. W. Glass and Yuri Gurevich The problem is proven to be undecidable. [48]
Yuri Gurevich and Saharon Shelah We replace Gödel's sophisticated combinatorial argument with a simple probabilistic one. [47]
Yuri Gurevich and Saharon Shelah The negative solution is given. [46]
Yuri Gurevich and Saharon Shelah Under a weak set-theoretic assumption, we interpret full second-order logic in the monadic theory of order. [45]
Yuri Gurevich, Menachem Magidor and Saharon Shelah In a series of papers, Buechi proved the decidability of the monadic (second-order) theory of omega_0, of all countable ordinals, of omega_1, and finally of all ordinals < omega_2. Here, assuming the consistency of a weakly compact cardinal, we prove that, in different set-theoretic worlds, the monadic theory of omega_2 may be arbitrarily difficult (or easy). [44]
Yuri Gurevich [43] E. M. Clarke, N. Francez, Y. Gurevich and P. Sistla, ``Can message buffers be characterized in linear temporal logic?" , Symposium on Principles of Distributed Computing, ACM, 1982, 148--156 In the case of unbounded buffers, the negative answer follows from a result in [28]. [42]
Andreas Blass and Yuri Gurevich Papadimitriou and Yannakakis were interested whether Unique Sat is hard for {L - L' : L, L' are NP} when NP differs from co-NP (otherwise the answer is obvious). We show that this is true under one oracle and false under another. [41]
Yuri Gurevich and H. R. Lewis Answering a question of Jeffrey Ullman, the problem in the title is shown to be undecidable. [40]
Yuri Gurevich and Leo Harrington We prove an effective determinacy theorem and, as an application, give a transparent proof of the famous complementation lemma of Michael Rabin for tree automata. [39]
Yuri Gurevich [38]
I. Gertsbakh and Y. Gurevich [37]
Yuri Gurevich and Saharon Shelah Assuming the continuum hypothesis, Shelah interpreted true first-order arithmetic in the monadic theory of order (Annals of Math., 1975). The assumption is removed here. [36]
Yuri Gurevich [35]
S. O. Aandraa, E. Börger and Yuri Gurevich [34]
Yuri Gurevich Answering a question of Henson, Jockush, Rubel and Takeuti, we prove that the rationals, the irrationals and the Cantor set are all elementary equivalent as topological spaces. [33]
A. M. W. Glass, Y. Gurevich, W. C. Holland and M. Jambu-Giraudet [32]
A. M. W. Glass, Yuri Gurevich, W. C. Holland and Saharon Shelah [31]
Yuri Gurevich and W. C. Holland A first-order statement about the group of automorphisms of the real line characterizes the real line among all homogeneous chains. [30]
Yuri Gurevich [29]
Yuri Gurevich and Saharon Shelah We analyze the monadic theory of the rational line and the theory of real line with quantification over ``small" subsets. The results are in some sense the best possible. [28]
Yuri Gurevich The decomposition method of Feferman-Vaught is generalized and made more applicable. [27]
Yuri Gurevich The seminal paper ``The monadic theory of order" of Saharon Shelah in Annals of Math., 1975, contained numerous conjectures. Most of them were proved or, in some cases, disproved in [26, 27] (after long and hard work). [26]
Yuri Gurevich [25]
Yuri Gurevich The ``right" formalization of o. a. groups is introduced and proved decidable. It allows quantification over convex subgroups and expresses almost all relevant algebra. [24]
Yuri Gurevich A symmetric (with respect to True and False) conservative extension of first-order intuitionistic logic is introduced and studied; a Kripke-style completeness proof is given. [23]
I. Gertsbakh and Y. Gurevich A general method for constructing all optimal fleets is described. [22]
Yuri Gurevich [21]
Yuri Gurevich The classification of prefix-and-signature fragments of first-order logic, completed in [7], is extended to first-order logic with equality and at least one function symbol of positive arity. One case was solved (confirming a conjecture of this author) by Shelah. [20]
Yuri Gurevich [19]
Yuri Gurevich [18]
Yuri Gurevich The main result, announced in [9], is that the E*AE* class of first-order logic with functions but without equality has the finite model property (and therefore is decidable for satisfiability and finite satisfiabiity). This result had completed the classical decision problem for that logic. [17]
Yuri Gurevich and Tristan Turashvili [16]
Yuri Gurevich and Igor O. Koriakov We prove the recursive inseparability result for the unrestricted tiling (or domino) problem: the set I of instances that can cover a plain and the set J of instances that cannot cover even a torus are recursively inseparable. [15]
Yuri Gurevich An observation that Minsky machines may be more convenient than Turing machines for reduction purposes is illustrated by simplifying the proof from [7] that some [AEA&E*,(k,1)] is a reduction class. [14]
Yuri Gurevich Consider the collection D of first-order formulas alpha such that the first-order theory with axiom alpha is decidable. It is proven that D is neither r.e. nor co-r.e. (The second part has been known earlier.) [English translation in Algebra and Logic 8 (1969), 362--363] [13]
Yuri Gurevich First, the classifiability theorem for prefix-vocabulary classes is proved. Second, the decision problem for (the prefix-vocabulary fragments of) pure logic of predicates and functions is completed, though the treatment of the most difficult decidable class is deferred to [18]. In particular, the classes [A^2,(0,1),(1)] and [A^2,(1),(0,1)] are proved to be conservative reduction classes. [English translation in Algebra and Logic 8 (1969), 160--174] [12]
Yuri Gurevich [11]
Yuri Gurevich [10]
Yuri Gurevich [English translation in Soviet Mathematics 8 (1967), 987--989] [9]
Yuri Gurevich Delimiting the decidability result of [3] for linearly ordered abelian groups and answering Malcev's question, the theorem in the title is proved. [8]
Yuri Gurevich We prove that the word problem for finite semigroups (Do u_1=v_1,..., u_n=v_n imply u=v in all finite semigroups?) is undecidable. In fact the premise E := (u_1=v_1and ... and u_n=v_n) can be fixed. Furthermore, for this E, the following classes of implications I := (E implies u=v) are recursively inseparable: those which are (universally) true in every periodic semigroup and those that fail in some finite semigroup. The paper contains some additional undecidability results. [7]
Yuri Gurevich The solution is completed for the classical decision problem for (prefix-vocabulary fragments of) pure predicate logic. Specifically, the AEAE* fragment with one binary relation is shown to be undecidable for satisfiability and finite satisfiability. [6]
Yuri Gurevich The previous result is strengthen to k=0. See a more complete version in [7]. [English translation in Soviet Mathematics 7 (1966), 669--670] [5]
Yuri Gurevich The AEAE* fragment of pure predicate logic with one binary and some number k of unary predicates is proven to be a conservative reduction class. Superseded by [6]. [English translation in Soviet Mathematics 7 (1966), 217--219] [4]
Yuri Gurevich The method of existential interpretation is developed and used to prove the undecidability of E^rA* fragments of various popular first-order theories. [3]
Yuri Gurevich O. a. groups are classified by first-order properties, and (answering Tarski's question) the first-order theory of o. a. groups is proven to be decidable. [English translation in Amer. Math. Society Translations 46 (1965), 165--192] [2]
Yuri Gurevich and Ali I. Kokorin It is proved that no universal first-order property distinguishes between any o. a. groups. [1]
Yuri Gurevich |