|
The articles are in reverse-chronological order, more or less. The
index, once assigned, does not change; hence some fractional indices and
indices like Na, Nb. There are also a book contribution list and a non-annotated publication list where publications are grouped by areas. For quicker navigation, use this: 10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 160, 170, 180, 190 [194]
Andreas Blass and Yuri Gurevich Existential fixed point logic (EFPL) is a natural fit for some applications, and the purpose of this talk is to attract attention to EFPL. The logic is also interesting in its own right as it has attractive properties. One of those properties is rather unusual: truth of formulas can be defined (given appropriate syntactic apparatus) in the logic. We mentioned that property elsewhere, and we use this opportunity to provide the proof. [193]
Andreas Blass and Yuri Gurevich 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. [192]
Andreas Blass, 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. [191a]
Yuri Gurevich and Itay Neeman [191]
Yuri Gurevich and Itay Neeman DKAL is an expressive declarative authorization language based on existential fixed-point logic. It is considerably more expressive than existing languages in the literature, and yet feasible. Our query algorithm is within the same bounds of computational complexity as e.g. that of SecPAL. DKAL's distinguishing features include [190]
Nikolaj Bjorner, Andreas Blass, and Yuri Gurevich When a file is to be transmitted from a sender to a recipient and when
the latter already has a file somewhat similar to it, remote differential
compression seeks to determine the similarities interactively so as to
transmit only the part of the new file not already in the recipient's old
file. Content-dependent chunking means that the sender and recipient chop
their files into chunks, with the cutpoints determined by some internal
features of the files, so that when segments of the two files agree
(possibly in different locations within the files) the cutpoints in such
segments tend to be in corresponding locations, and so the chunks
agree. By exchanging hash values of the chunks, the sender and recipient
can determine which chunks of the new file are absent from the old one and
thus need to be transmitted. [189]
Yuri Gurevich, Dirk Leinders and Jan Van den Bussche Data streams are modeled as infinite or finite sequences of data elements coming from an arbitrary but fixed universe. The universe can have various built-in functions and predicates. Stream queries are modeled as functions from streams to streams. Both timed and untimed settings are considered. Issues investigated include abstract definitions of computability of stream queries; the connection between abstract computability, continuity, monotonicity, and non-blocking operators; and bounded memory computability of stream queries using abstract state machines (ASMs). [188a]
Yuri Gurevich This is an extended abstract of the opening talk of CSR 2007. It is based on 188. [188]
Nachum Dershowitz and Yuri Gurevich Church's Thesis asserts that the only numeric functions that can be calculated by effective means are the recursive ones, which are the same, extensionally, as the Turing-computable numeric functions. The Abstract State Machine Theorem states that every classical algorithm is behaviorally equivalent to an abstract state machine. This theorem presupposes three natural postulates about algorithmic computation. Here, we show that augmenting those postulates with an additional requirement regarding basic operations gives a natural axiomatization of computability and a proof of Church's Thesis, as Goedel and others suggested may be possible. In a similar way, but with a different set of basic operations, one can prove Turing's Thesis, characterizing the effective string functions, and---in particular---the effectively-computable functions on string representations of numbers. [187]
Robert H. Gilman, Yuri Gurevich and Alexei Miasnikov Each relational structure X has an associated Gaifman graph, which endows X with the properties of a graph. If x is an element of X, let B n(x) be the ball of radius n around x. Suppose that X is infinite, connected and of bounded degree. A first-order sentence s in the language of X is almost surely true (resp. a.s. false) for finite substructures of X if for every x in X, the fraction of substructures of B n(x) satisfying s approaches 1 (resp. 0) as n approaches infinity. Suppose further that, for every finite substructure, X has a disjoint isomorphic substructure. Then every s is a.s. true or a.s. false for finite substructures of X. This is one form of the geometric zero-one law. We formulate it also in a form that does not mention the ambient infinite structure. In addition, we investigate various questions related to the geometric zero-one law. [186]
Andreas Blass and Yuri Gurevich In a computational process, certain entities (for example sets or arrays) and operations on them may be automatically available, for example by being provided by the programming language. We define background classes to formalize this idea, and we study some of their basic properties. The present notion of background class is more general than the one we introduced in an earlier paper, and it thereby corrects one of the examples in that paper. The greater generality requires a non-trivial notion of equivalence of background classes, which we explain and use. Roughly speaking, a background class assigns to each set (of atoms) a structure (for example of sets or arrays or combinations of these and similar entities), and it assigns to each embedding of one set of atoms into another a standard embedding between the associated background structures. We discuss several, frequently useful, properties that background classes may have, for example that each element of a background structure depends (in some sense) on only finitely many atoms, or that there are explicit operations by which all elements of background structures can be produced from atoms. [185]
Andreas Blass and Yuri Gurevich 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. [184]
Martin Grohe, Yuri Gurevich, Dirk Leinders, Nicole Schweikardt, Jerzy
Tyszkiewicz, and Jan Van den Bussche We introduce a new abstract model of database query processing, finite cursor machines, that incorporates certain data streaming aspects. The model describes quite faithfully what happens in so-called ``one-pass'' and ``two-pass query processing''. Technically, the model is described in the framework of abstract state machines. Our main results are upper and lower bounds for processing relational algebra queries in this model, specifically, queries of the semijoin fragment of the relational algebra. [183]
Dan Teodosiu, Nikolaj Bjorner, Yuri Gurevich, Mark Manasse, Joe
Porkka Remote Differential Compression (RDC) protocols can efficiently update files over a limited-bandwidth network when two sites have roughly similar files; no site needs to know the content of another's files a priori. We present a heuristic approach to identify and transfer the file differences that is based on finding similar files, subdividing the files into chunks, and comparing chunk signatures. Our work significantly improves upon previous protocols such as LBFS and RSYNC in three ways. Firstly, we present a novel algorithm to efficiently find the client files that are the most similar to a given server file. Our algorithm requires 96 bits of meta-data per file, independent of file size, and thus allows us to keep the metadata in memory and eliminate the need for expensive disk seeks. Secondly, we show that RDC can be applied recursively to signatures to reduce the transfer cost for large files. Thirdly, we describe new ways to subdivide files into chunks that identify file differences more accurately. We have implemented our approach in DFSR, a state-based multimaster file replication service shipping as part of Windows Server 2003 R2. Our experimental results show that similarity detection produces results comparable to LBFS while incurring a much smaller overhead for maintaining the metadata. Recursive signature transfer further increases replication efficiency by up to several orders of magnitude. [182]
Andreas Blass, Yuri Gurevich, Dean Rosenzweig
and Benjamin Rossman 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. In a companion paper 176 the axiomatisation was extended 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 here the definition of abstract state machines to incorporate explicit attention to the relative timing of replies and to the possible absence of replies. We prove the characterization theorem for extended ASMs with respect to general algorithms as axiomatised in 176. [181]
Yuri Gurevich We share our experience of using abstract state machines for teaching computation theory at the University of Michigan. [180]
Andreas Blass and Yuri Gurevich For every regular language of nested words, the underlying strings form a context-free language, and every context-free language can be obtained in this way. Nested words and nested-word automata are generalized to motley words and motley-word automata. Every motley-word automation is equivalent to a deterministic one. For every regular language of motley words, the underlying strings form a finite intersection of context-free languages, and every finite intersection of context-free languages can be obtained in this way. [179]
Yuri Gurevich, Margus Veanes and Charles Wallace
Extended Abstract in Proc. DLT 2006 (Developments in Language Theory) The abstract state machine (ASM) is a modern computation model. ASMs and ASM based tools are used in academia and industry, albeit in a modest scale. They allow you to give high-level operational semantics to computer artifacts and to write executable specifications of software and hardware at the desired abstraction level. In connection to the 2006 conference on Developments in Language Theory, we point out several ways that we believe abstract state machines can be useful to the DLT community. [178]
Andreas Blass and Yuri Gurevich The following known observation may be useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U1,...,Un then R is well-founded. A question arises how to bound the ordinal height |R| of the relation R in terms of the ordinals αi = |Ui|. We introduce the notion of the stature ||P|| of a well partial ordering P and show that |R| less than or equal to the stature of the direct product of ordinals α1,...,α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 the stature of the direct product of ordinals α1,...,αn is equal to the natural product of these ordinals. [177]
Yuri Gurevich and Tanya Yavorskaya This report consists of two separate parts, essentially two oversized footnotes to 141. In Chapter I, Yuri Gurevich and Tatiana Yavorskaya present and study a more abstract version of the bounded exploration postulate. In Chapter II, Tatiana Yavorskaya gives a complete form of the characterization, sketched in 141, of bounded-choice sequential algorithms. [176]
Andreas Blass, Yuri Gurevich, Dean Rosenzweig
and Benjamin Rossman 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, in a companion paper, 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. This is essentially part one of Microsoft Research Technical Report MSR-TR-2005-113, August 2005. 182 is essentially the remainder of the 2005 technical report. [175]
Yuri Gurevich and Paul Schupp The modular group plays an important role in many branches of mathematics. We show that the membership problem for the modular group is polynomial time in the worst case. We also show that the membership problem for a free group remains polynomial time when elements are written in a normal form with exponents. [174]
Yuri Gurevich Originally published, without the appendix, in A sequential algorithm just follows its instructions and thus cannot make a nondeterministic choice all by itself, but it can be instructed to solicit outside help to make a choice. Similarly, an object-oriented program cannot create a new object all by itself; a create-a-new-object command solicits outside help. These are but two examples of intra-step interaction of an algorithm with its environment. Here we motivate and survey recent work on interactive algorithms within the Behavioral Computation Theory project. [173]
Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes Testing tasks can be viewed (and organized!) as games against nature. We introduce and study reachability games. 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. We find out when exactly optimal strategies exist for a given reachability game, and how to construct them. [172]
Andreas Blass and Yuri Gurevich 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 related issues. [171]
Andreas Blass and Yuri Gurevich 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. The first two papers are
166 and 170
As in the first two papers of the series, we are
concerned here with ordinary, small-step, interactive algorithms.
This means that the algorithms [170]
Andreas Blass and Yuri Gurevich 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. The first papers is 166. As in the
first paper of the series, we are concerned here with ordinary,
small-step, interactive algorithms. This means that the algorithms [169]
Yuri Gurevich, Benjamin Rossman and Wolfram Schulte The Abstract State Machine Language, AsmL, is a novel executable specification language based on the theory of Abstract State Machines. AsmL is object-oriented, provides high-level mathematical data-structures, and is built around the notion of synchronous updates and finite choice. AsmL is fully integrated into the .NET framework and Microsoft development tools. In this paper, we explain the design rationale of AsmL and provide static and dynamic semantics for a kernel of the language. [169a]
Yuri Gurevich, Benjamin Rossman and Wolfram Schulte This is an extended abstract of article 169. [168]
Yuri Gurevich and Rostislav Yavorskiy Consider a multiple-agent transition system such that, for some basic types T1,...,Tn, the state of any agent can be represented as an element of the Cartesian product Ti. The system evolves by means of global steps. During such a step, new agents may be created and some existing agents may be updated or removed, but the total number of created, updated and removed agents is uniformly bounded. We show that, under appropriate conditions, there is an algorithm for deciding assume-guarantee properties of one-step computations. The result can be used for automatic invariant verification as well as for finite state approximation of the system in the context of test-case generation from AsmL specifications. [167]
Yuri Gurevich For a while it seemed possible to pretend that all interaction between an algorithm and its environment occurs inter-step, but not anymore. Andreas Blass, Benjamin Rossman and the speaker are extending the Small-Step Characterization Theorem (that asserts the validity of the sequential version of the ASM thesis) and the Wide-Step Characterization Theorem (that asserts the validity of the parallel version of the ASM thesis) to intra-step interacting algorithms. Editorial comment. This was my first talk on intra-step interactive algorithms. The intended audience was the ASM community. 174 is a later talk on this topic, and it is addressed to a general computer science audience. [166]
Andreas Blass and Yuri Gurevich 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 [165]
Yuri Gurevich We quickly survey the ASM project, from its foundational roots to industrial applications. [164]
Andreas Blass and Yuri Gurevich 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. [163]
Mike Barnett, Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte,
Nikolai Tillmann and Margus Veanes We present an approach for modeling use cases and scenarios in the Abstract State Machine Language and discuss how to use such models for validation and verification purposes. [162]
Yuri Gurevich and Saharon Shelah We prove that the spectrum of any monadic second-order formula F with
one unary function symbol (and no other function symbols) is eventually
periodic, so that there exist natural numbers p>0 (a period) and t (a
p-threshold) such that if F has a model of cardinality n>t then it has a
model of cardinality n+p. [161]
Yuri Gurevich and Nikolai Tillmann A datastructure instance, e.g. a set or file or record, may be modified independently by different parts of a computer system. The modifications may be nested. Such hierarchies of modifications need to be efficiently checked for consistency and integrated. This is the problem of partial updates in a nutshell. In our first paper on the subject, we developed an algebraic framework which allowed us to solve the partial update problem for some useful datastructures including counters, sets and maps. These solutions are used for the efficient implementation of concurrent data modifications in the specification language AsmL. The two main contributions of this paper are (i)~a more general algebraic framework for partial updates and (ii)~a solution of the partial update problem for sequences and labeled ordered trees. [160]
Andreas Blass and Yuri Gurevich 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. [159]
Uwe Glaesser, Yuri Gurevich and Margus Veanes In some distributed and mobile communication models, a message disappears in one place and miraculously appears in another. In reality, of course, there are no miracles. A message goes from one network to another; it can be lost or corrupted in the process. Here we present a realistic but high-level communication model where abstract communicators represent various nets and subnets. The model was originally developed in the process of specifying a particular network architecture, namely the Universal Plug and Play architecture. But it is general. Our contention is that every message-based distributed system, properly abstracted, gives rise to a specialization of our abstract communication model. The purpose of the abstract communication model is not to design a new kind of network; rather it is to discover the common part of all message-based communication networks. The generality of the model has been confirmed by its successful reuse for very different distributed architectures. The model is based on distributed abstract state machines. It is implemented in the specification language AsmL and is being used for testing distributed systems. [158]
Andreas Blass and Yuri Gurevich In a recent paper, the logician Yiannis Moschovakis argues that no state machine describes mergesort on its natural level of abstraction. We do just that. Our state machine is a recursive ASM. [157-2]
Andreas Blass and Yuri Gurevich We consider parallel algorithms working in sequential global time, for example circuits or parallel random access machines (PRAMs). Parallel abstract state machines (parallel ASMs) are such parallel algorithms, and the parallel ASM thesis asserts that every parallel algorithm is behaviorally equivalent to a parallel ASM. In an earlier paper 157-1, we axiomatized parallel algorithms, proved the ASM thesis and proved that every parallel ASM satisfies the axioms. It turned out that 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. [157-1]
Andreas Blass and Yuri Gurevich 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. See also 157-2. [156]
Yuri Gurevich and Nikolai Tillmann The partial update problem for parallel abstract state machines has manifested itself in the cases of counters, sets and maps. We propose a solution of the problem that lends itself to an efficient implementation and covers the three cases mentioned above. There are other cases of the problem that require a more general framework. [155]
Yuri Gurevich, Wolfram Schulte and Margus Veanes A powerful practical ASM language, called AsmL, is being developed in Microsoft Research by the group on Foundations of Software Engineering. AsmL extends the language of original ASMs in a number of directions. We describe some of these extensions. [154]
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte and Margus Veanes We give an algorithm that derives a finite state machine (FSM) from a given abstract state machine (ASM) specification. This allows us to integrate ASM specs with the existing tools for test case generation from FSMs. ASM specs are executable but have typically too many, often infinitely many states. We group ASM states into finitely many hyperstates which are the nodes of the FSM. The links of the FSM are induced by the ASM state transitions. [153]
Uwe Glaesser, Yuri Gurevich and Margus Veanes Recently, Microsoft took a lead in the development of a standard for peer-to-peer network connectivity of various intelligent appliances, wireless devices and PCs. It is called the Universal Plug and Play Device Architecture (UPnP). We construct a high-level Abstract State Machine (ASM) model for UPnP. The model is based on the ASM paradigm for distributed systems with real-time constraints and is executable in principle. For practical execution, we use AsmL, the Abstract state machine Language, developed at Microsoft Research and integrated with Visual Studio and COM. This gives us an AsmL model, a refined version of the ASM model. The third part of this project is a graphical user interface by means of which the runs of the AsmL model are controlled and inspected at various levels of detail as required for e.g. simulation and conformance testing. [152]
Anuj Dawar and Yuri Gurevich Fixed point logics are extensions of first order predicate logic with fixed point operators. A number of such logics arose in finite model theory but they are of interest to much larger audience, e.g. AI, and there is no reason why they should be restricted to finite models. We review results established in finite model theory, and consider the expressive power of fixed point logics on infinite structures. [151]
Yuri Gurevich Analysis of foundational problems like "What is computation?" leads to a sketch of the paradigm of abstract state machines (ASMs). This is followed by a brief discussion on ASMs applications. Then we present some theoretical problems that bridge between the traditional LICS themes and abstract state machines. [150a]
Andreas Blass and Yuri Gurevich [150]
Andreas Blass and Yuri Gurevich and Saharon Shelah 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. [149]
Andreas Blass and Yuri Gurevich 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. [144] is an abridged version of this paper, and [148] is a popular version of this paper. [148]
Andreas Blass and Yuri Gurevich This article is a part of the continuous 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 role 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 [95]. 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. [147]
Yuri Gurevich and Alex Rabinovich The paper deals with logically definable families of sets of rational numbers. In particular we are interested whether the families definable over the real line with a unary predicate for the rationals are definable over the rational order alone. Let f(X,Y) and g(Y) range over formulas in the first-order monadic language of order. Let Q be the set of rationals and F be the family of subsets J of Q such that f(Q,J) holds over the real line. The question arises whether, for every formula f, the family F can be defined by means of a formula g(Y) interpreted over the rational order. We answer the question negatively. The answer remains negative if the first-order logic is strengthen to weak monadic second-order logic. The answer is positive for the restricted version of monadic second-order logic where set quantifiers range over open sets. The case of full monadic second-order logic remains open. [146]
Andreas Blass and Yuri Gurevich 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 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 falseis partially correct on N but any loop invariant I(x,y,z) for this asserted program is undecidable. [145]
Mike Barnett, Egon Boerger, Yuri Gurevich,
Wolfram Schulte and Margus Veanes Our goal is to provide a rigorous method, clear notation and convenient tool support for high-level system design and analysis. For this purpose we use abstract state machines (ASMs). Here we describe a particular case study: modeling a debugger of a stack based runtime environment. The study provides evidence for ASMs being a suitable tool for building \emph{executable} models of software systems on various abstraction levels, with precise refinement relationships connecting the models. High level ASM models of proposed or existing programs can be used throughout the software development cycle. In particular, ASMs can be used to model inter component behavior on any desired level of detail. This allows one to specify application programming interfaces more precisely than it is done currently. [144]
Andreas Blass and Yuri Gurevich This paper is a sequel to [120], a commentary on [Saharon Shelah 634, "Choiceless polynomial time logic: inability to express", these proceedings], and an abridged version of [149] that contains complete proofs of all the results presented here. The BGS model of computation was defined in [120] 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 and promise to make the complete version available soon. [143]
Andreas Blass and Yuri Gurevich 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 [103], an infinite reserve. Although the reserve is a naked set, it is often desirable to have some external structure over it. For example, in [120] 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 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." [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. [141b]
Jessica Millar In the appendix of 141, Gurevich defines the notion of finite exploration for small-step algorithms which do not intrastep interact with the environment. Although satisfying finite exploration is a seemingly weaker property than satisfying bounded exploration, he proves the two notions are equivalent for this class of algorithms. We investigate what happens in the case of ordinary small-step algorithms -- in particular, these algorithms do intrastep interact with the environment -- as described by Blass and Gurevich in 166. Our conclusion is that every algorithm satisfying the appropriate version of finite exploration is equivalent to an algorithm satisfying bounded exploration. We provide a counterexample to the stronger statement that every algorithm satisfying finite exploration satisfies bounded exploration. This statement becomes true if the definition of bounded exploration is modified slightly. The proposed modification is natural for algorithms operating in isolation, but not for algorithms belonging to a larger systems of computation. We believe the results generalize to general interactive small-step algorithms. [141a]
Yuri Gurevich [141]
Yuri Gurevich What are sequential algorithms exactly? Our claim, known as the sequential ASM thesis, has been that, as far as behavior is concerned, sequential algorithms are exactly sequential abstract state machines: For every sequential algorithm A, there is a sequential abstract state machine B that is behaviorally identical to A. In particular B simulates A step for step. In this paper we prove the sequential ASM thesis, so that it becomes a theorem. But how can one possibly prove a thesis? Here is what we do. We formulate three postulates satisfied by all sequential algorithms (and in particular by sequential abstract state machines). This leads to the following definition: a sequential algorithm is any object that satisfies the three postulates. At this point the thesis becomes a precise statement. And we prove the statement. This is a non-dialog version of the dialog #136. An intermediate version was published as technical report MSR-TR-99-65, Microsoft Research, September 1999. [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 lock-step. 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 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 [This manuscript was never published. The work, done sporadically in 1996-98, was driven by the enthusiasm of Karl Stroetmann of Siemens. Eventually he was reassigned away from ASMs and the work stopped. The item wasn't removed from the list because some of its explorations may be useful. An additional minor reason was to avoid changing the numbers of the subsequent items.] [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 R be the integer order, that is the set of real numbers together with the standard order of reals. Let I be the set of integer numbers, let Y range over subsets of I, let P(I,X) be a monadic second-order formula about R, and let F be the collection of all subsets X of I such that P(I,X) holds in R. Even though F is a collection of subsets of I, its definition may involve quantification over reals and over sets of reals. In that sense, F is defined with the background of real order. Is that background essential or not? Maybe there is a monadic second-order formula Q(X) about I that defines F (so that F is the collection of all subsets X of I such that Q(X) holds in I). We prove that this is indeed the case, for any monadic second-order formula P(I,X). The claim remains true if the set I of integers is replaced above with any closed subset of R. The claim fails 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 corroboration problem, the simultaneous rigid E-unification problem and the prenex fragment of intuitionistic logic with equality. [125]
Anatoli Degtyarev, 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 intuitionistic 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. [Added in July 2006] The additional part on computer proofs vs. proofs by hand was a result of frustration that many computer scientists would not trust informal mathematical proofs, while many mathematicians would not trust computer proofs. I seemed obvious to me that, on large scale, proving is not only hard but also is imperfect and has engineering character. We need informal proofs and computer proofs and more, e.g. stratification, experimentation. [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 of 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 (pages 333-351), 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 decidability 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ω∞, ω sentence φ with counting quantifiers defines a linear order in all the structures. Furthermore, φ does not distinguish 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 Graedel 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 Boerger, 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 the 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 Graedel 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 shows 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 project on abstract state machines (a.k.a. evolving algebras) 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 ASM thesis asserts that ASMs are such versatile machines. The guide provided the definition of sequential and -- for the first time -- parallel and distributed ASMs. The denotational semantics of sequential and parallel ASMs is addressed in the Michigan guide 129. [102]
Yuri Gurevich This humorous article incorporates a bit of serious criticism of algebraic and logic approaches to software problems. [101]
Yuri Gurevich [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 [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 descriptive definition of reductions. We simplify slightly Levin's usable definition of deterministic 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 [90]
Yuri Gurevich This is a little essay on finite model theory. Section 1 gives some
counterexamples to classical theorems in the finite case. Section 2 gives
a finite version of the classical compactness theorem. Section 3 announces
two Gurevich-Shelah results.
[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σ solves the problem within time n1+τ if σ + 2τ < 1/2. [86]
Yuri Gurevich [85]
Yuri Gurevich 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 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]
Miklos Ajtai and Yuri 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 Matijasevich, 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 approach, we discover serious complications with it. [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
One contribution of the article was to formulate Kolmogorov-Uspensky
thesis. In "To the Definition of an Algorithm" [Uspekhi Mat. Nauk 13:4
(1958), 3--28 (Russian)] Kolmogorov and Uspensky wrote that they just
wanted to comprehend the notions of computable functions and algorithms,
and to convince themselves that there is no way to extend the notion of
computable function. In fact, they did more than that. It seems that
their thesis was this: every computation, performing only one restricted local action at a time, can be viewed as (not only being simulated by, but actually being) the computation of an appropriate KU machine (in the more general form).Uspensky agreed [J. Symb. Logic 57 (1992), page 396]. Another contribution of the paper was a popularization of a beautiful theorem of Leonid Levin Theorem. For every computable function F(w) = x from binary strings to binary strings, there exists a KU algorithm A such that A conclusively inverts F and (Time of A on x) = O(Time of B on x) for every KU algorithm B that conclusively inverts F.which had been virtually unknown, partially because it appeared (without a proof) in his article "Universal Search Problems" [Problems of Information Transmission 9:3 (1973), 265--266] which is hard to read. [77]
Yuri Gurevich and Jim Morris Jim Morris was a PhD student of Yuri Gurevich at the Electrical Engineering and Computer Science Department of the University of Michigan, the first PhD student working on the abstract state machine project. This is an extended abstract of 1988 Jim Morris's PhD thesis (with the same title) and the first example of the ASM semantics of a whole programming language. [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 chapter consists of two quite different parts. [73]
Andreas Blass and Yuri Gurevich The purpose of this paper is to draw attention to existential fixed-point logic (EFPL). Among other things, we show the following.
[72]
Miklos Ajtai and Yuri 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 fi |