Of many book projects, only one has come to fruition:
Classical Decision Problem.
The following list of articles and book chapters is in the reverse-chronological order more or less. It is followed by a short Afterthought that contains a few additional items, passed over at the time.
250,
240,
230,
220,
210,
200,
190,
180,
170,
160,
150,
140,
130,
120,
110,
100,
90,
80,
70,
60,
50,
40,
30,
20,
10
[256]
Yuri Gurevich and Andreas Blass
Primal logic of information
arXiv:2307.06454
ABSTRACT. Primal logic arose in access control; it has a remarkably efficient (linear time) decision procedure for its entailment problem. But primal logic is a general logic of information. In the realm of arbitrary items of information (infons), conjunction, disjunction, and implication may seem to correspond (set-theoretically) to union, intersection, and relative complementation. But, while infons are closed under union, they are not closed under intersection or relative complementation. It turns out that there is a systematic transformation of propositional intuitionistic calculi to the original (propositional) primal calculi; we call it Flatting. We extend Flatting to quantifier rules, obtaining arguably the right quantified primal logic, QPL. The QPL entailment problem is exponential-time complete, but it is polynomial-time complete in the case, of importance to applications (at least to access control), where the number of quantifiers is bounded.
[255]
Yuri Gurevich
The umbilical cord of finite model theory
Bulletin of the EATCS 139 February 2023
Journal of Logic and Computation September 2023
DOI
arXiv:2301.09145
ABSTRACT. Model theory was born and developed as a part of mathematical logic. It has various application domains but is not beholden to any of them. A priori, the research area known as finite model theory would be just a part of model theory but didn't turn out that way. There is one application domain -- relational database management -- that finite model theory had been beholden to during a substantial early period when databases provided the motivation and were the main application target for finite model theory. Arguably, finite model theory was motivated even more by complexity theory. But the subject of this paper is how relational database theory influenced finite model theory. This is NOT a scholarly history of the subject with proper credits to all participants. My original intent was to cover just the developments that I witnessed or participated in. The need to make the story coherent forced me to cover some additional developments.
[254]
Yuri Gurevich and Andreas Blass
Software science view on quantum circuit algorithms
Information and Computation 292 105024 2023,
DOI
arXiv:2209.13731
ABSTRACT. We show that, on the abstraction level of quantum circuit diagrams, quantum circuit algorithms belong to the species of interactive sequential algorithms that we studied in earlier work. This observation leads to a natural specification language for quantum circuit algorithms.
[253]
Yuri Gurevich
Novosibirsk algebra and logic in the mid 1960s:
A personal perspective
arXive: 2209.14701
to appear in a forthcoming book
ABSTRACT. Being asked to write about Asan D. Taimanov, I had a little problem. I knew Taimanov. I liked and respected him, and so I wanted to write something. But I didn't know him well. I didn't live in the Novosibirsk Akademgorodok where he lived and worked; I just visited Novosibirsk a number of times. So I decided to widen the topic and write about my own Novosibirsk experience, including interactions with Taimanov.
[252]
Andreas Blass, Yuri Gurevich, and Alexander Volberg
Wigner's quasidistribution and Dirac's kets
Bulletin of the EATCS 136 February 2021
arXiv:2201.05911
ABSTRACT. In every state of a quantum particle, Wigner's quasidistribution is the unique quasidistribution on the phase space with the correct marginal distributions for position, momentum, and all their linear combinations.
[251]
Yuri Gurevich and Andreas Blass
Simple circuit simulations of classical and quantum Turing machines
Proceedings of the Royal Society A 478 20210891 2021,
DOI
arXiv:2111.10830
ABSTRACT. We construct reversible Boolean circuits efficiently simulating reversible Turing machines. Both the circuits and the simulation proof are rather simple. Then we give a fairly straightforward generalization of the circuits and the simulation proof to the quantum case.
[250]
Yuri Gurevich and Andreas Blass
Quantum circuits with classical channels and the principle of deferred measurements
Theoretical Computer Science
920 (2022) 21-32,
DOI
arXiv:2107.08324
ABSTRACT. We define syntax and semantics of quantum circuits, allowing measurement gates and classical channels. We define circuit-based quantum algorithms and prove that, semantically, any such algorithm is equivalent to a single measurement that depends only on the underlying quantum circuit. Finally, we use our formalization of quantum circuits to state precisely and prove the principle of deferred measurements.
[249]
Andreas Blass and Yuri Gurevich
Input independence
arXiv:2105.14610v2
ABSTRACT. We establish the following input independence principle. If a quantum circuit C computes a unitary transformation along a computation path μ, then the probability that computation of C follows μ is independent of the input.
[248]
Yuri Gurevich
Reversify any sequential algorithm
Originally in Bulletin of the EATCS 134 June 2021
Then in
arXiv:2105.05626
ABSTRACT. To reversify an arbitrary sequential algorithm A, we gently instrument A with bookkeeping machinery. The result is a step-for-step reversible algorithm that mimics A step-for-step and stops exactly when A does. Without loss of generality, we presume that algorithm A is presented as an abstract state machine that is behaviorally identical to A. The existence of such representation has been proven theoretically, and the practicality of such representation has been amply demonstrated.
[247]
Yuri Gurevich
Logical foundations: Personal perspective
Bulletin of the EATCS 133 February 2021
arXiv:2103.03930
Logic Journal of IGPL, article jzac059, July 2022
ABSTRACT. This is an attempt to illustrate the glorious history of logical foundations and to discuss the uncertain future.
[246]
Yuri Gurevich and Vladimir Vovk
Negative probabilities
arXiv:2011.12393
ABSTRACT. We explain, on the example of Wigner's quasiprobability distribution, how negative probabilities may be used in the foundations of probability.
[245]
Andreas Blass and Yuri Gurevich
Negative probabilities:
What are they for?
Journal of Physics A: Mathematical and Theoretical
Volume 54, Number 31, article 315303, 2021
https://doi.org/10.1088/1751-8121/abef4d
The version at this webpage is a slight improvement on the journal version.
ABSTRACT. An observation space S is a family of probability distributions Pi, i in I, sharing a common sample space Ω in a consistent way. A grounding for S is a signed probability distribution P on Ω yielding the correct marginal distribution Pi for every i. A wide variety of quantum scenarios can be formalized as observation spaces. We describe all groundings for a number of quantum observation spaces. Our main technical result is a rigorous proof that Wigner’s distribution is the unique signed probability distribution yielding the correct marginal distributions for position and momentum and all their linear combinations.
[244]
Andreas Blass and Yuri Gurevich
Circuits: An abstract viewpoint
Originally in Bulletin of the EATCS 131 June 2020
Then in arXiv:2006.09488
ABSTRACT. Our primary purpose is to isolate the abstract, mathematical properties of circuits --- both classical Boolean circuits and quantum circuits --- that are essential for their computational interpretation. A secondary purpose is to clarify the similarities and differences between the classical and quantum situations. The general philosophy in this note is to include the mathematically essential aspects of circuits but to omit any of the additional structures that are usually included for convenience. We shall, however, retain the assumption that circuits are finite; this assumption does no harm to the applicability of our approach and is necessary for some of our work.
[243]
Yuri Gurevich
Means-fit effectivity
Originally in Bulletin of the EATCS 130 February 2020
Then in arXiv:2002.03145
ABSTRACT. Historically, the notion of effective algorithm is closely related to the Church-Turing thesis. But effectivity imposes no restriction on computation time or any other resource; in that sense, it is incompatible with engineering or physics. We propose a natural generalization of it, \emph{means-fit effectivity}, which is effectivity relative to the (physical or abstract) underlying machinery of the algorithm. This machinery varies from one class of algorithms to another. Think for example of ruler-and-compass algorithms, arithmetical algorithms, and Blum-Shub-Smale algorithms. We believe that means-fit effectivity is meaningful and useful independently of the Church-Turing thesis. Means-fit effectivity is definable, at least in the theory of abstract state machines (ASMs). The definition elucidates original effectivity as well. Familiarity with the ASM theory is not assumed. We tried to make the paper self-contained.
[242]
Andreas Blass and Yuri Gurevich
Circuit pedantry
Originally in Bulletin of the EATCS 129 October 2019
Then in arXiv:1910.06145
ABSTRACT. Boolean and quantum circuits have commonalities and differences. To formalize the syntactical commonality we introduce syntactic circuits where the gates are black boxes. Syntactic circuits support various semantics. One semantics is provided by Boolean circuits, another by quantum circuits. Quantum semantics is a generalization of Boolean but, because of entanglement, the generalization is not straightforward. We consider only unitary quantum circuits here.
[241]
Yuri Gurevich
Unconstrained Church-Turing thesis cannot possibly be true
Originally in Bulletin of the EATCS 127 February 2019
Then in arXiv:1901.04911
ABSTRACT. The Church-Turing thesis asserts that if a partial strings-to-strings function is effectively computable then it is computable by a Turing machine. In the 1930s, when Church and Turing worked on their versions of the thesis, there was a robust notion of algorithm. These traditional algorithms are known also as classical or sequential. In the original thesis, effectively computable meant computable by an effective classical algorithm. Based on an earlier axiomatization of classical algorithms, the original thesis was proven in 2008. Since the 1930s, the notion of algorithm has changed dramatically. New species of algorithms have been and are being introduced. We argue that the generalization of the original thesis, where effectively computable means computable by an effective algorithm of any species, cannot possibly be true.
[240]
Andreas Blass and Yuri Gurevich
An invitation to quantum computing
Bulletin of the EATCS
126 October 2018
ABSTRACT. When a computer scientist attempts to understand quantum computing, he may stumble over the physics that seems to be a prerequisite. As a result, the attempt may be abandoned. This little pedagogical essay is aimed to help with this problem. We present the specific example of Grover’s search algorithm, but we put computation first and postpone physics.
[239]
Andreas Blass and Yuri Gurevich
Witness algebra and anyon braiding
Mathematical Structures in Computer Science
30:3 (March 2020) 234-270
DOI
arXiv:1807.10414
ABSTRACT. Topological quantum computation employs two-dimensional quasiparticles called anyons. The generally accepted mathematical basis for the theory of anyons is the framework of modular tensor categories. That framework involves a substantial amount of category theory and is, as a result, considered rather difficult to understand. Is the complexity of the present framework necessary? The computations of associativity and braiding matrices can be based on a much simpler framework, which looks less like category theory and more like familiar algebra. We introduce that framework here.
[238]
Andreas Blass and Yuri Gurevich
Braided distributivity
Theoretical Computer Science 807 (2020) 73-94
Prepublication at
arXiv:1807.11403
ABSTRACT. In category-theoretic models for the anyon systems proposed for topological quantum computing, the essential ingredients are two monoidal structures, additive and multiplicative. The former is symmetric but the latter is only braided, and multiplication is required to distribute over addition. What are the appropriate coherence conditions for the distributivity isomorphisms? We came to this question working on a simplification of the category-theoretical foundation of topological quantum computing, which is the intended application of the research reported here. This question above was answered by Laplaza when both monoidal structures are symmetric, but topological quantum computation depends crucially on multiplication being only braided, not symmetric. We propose coherence conditions for distributivity in this situation, and we prove that our conditions are (a) strong enough to imply Laplaza's when the latter are suitably formulated, and (b) weak enough to hold when --- as in the categories used to model anyons --- the additive structure is that of an abelian category and the braided multiplication is additive. Working on these results, we found a new redundancy in Laplaza's conditions.
[237]
Andreas Blass and Yuri Gurevich
Negative probabilities II:
What they are and what they are for
Bulletin of the EATCS
125 June 2018
arXiv:1807.10382
ABSTRACT. A signed probability distribution may extend a given traditional probability from observable events to all events. We formalize and illustrate this approach. We argue that the right question is not what negative probabilities are but what they are for.
[236]
Andreas Blass and Yuri Gurevich
Optimal no-go theorem on hidden-variable predictions of effect expectations
Physical Review A, Vol. 97, No. 3 2018
DOI: 10.1103/PhysRevA.97.032126
ABSTRACT. No-go theorems prove that, under reasonable assumptions, classical hidden-variable theories cannot reproduce the predictions of quantum mechanics. Traditional no-go theorems proved that hidden-variable theories cannot predict correctly the values of observables. Recent expectation no-go theorems prove that hidden-variable theories cannot predict the expectations of observables. We prove the strongest expectation-focused no-go theorem to date. It is optimal in the sense that the natural weakenings of the assumptions and the natural strengthenings of the conclusion make the theorem fail. The literature on expectation no-go theorems strongly suggests that the expectation-focused approach is more general than the value-focused one. We establish that the expectation approach is not more general.
(Re Spekkens's papers in PRA 71 (2005) and PRL 101:2 (2008), we point out: (i) The generalization of Kochen-Specker contextuality isn't a generalization in the sense of being implied by, as in the concept of mammal being more general than that of dog. (ii) The title "Negativity and contextuality are equivalent notions of nonclassicality" of one of the papers is misleading.)
[235]
Andreas Blass and Yuri Gurevich
Who needs category theory?
Bulletin of the EATCS
124 Feb 2018
arXiv:1807.11399
ABSTRACT. In computer science, category theory remains a contentious issue, with enthusiastic fans and a skeptical majority. Categories were introduced by Samuel Eilenberg and Saunders Mac Lane as an auxiliary notion in their general theory of natural equivalences. Here we argue that something like categories is needed on a more basic level. As you work with operations on structures, it may be necessary to coherently manipulate isomorphism (or more generally homomorphism) witnesses for various properties of these operations, e.g. associativity, commutativity and distributivity. A working mathematician, to use Mac Lane's term, is well advised to be aware of the coherent witness-manipulation problem and to know that category theory is an appropriate framework to address the problem. Of course, the working mathematician in question may be a computer scientist or physicist.
[234]
Andreas Blass and Yuri Gurevich
Common denominator for value and expectation no-go
theorems
Presented at QPL 2017,
14th International Conference on Quantum Physics and Logic
Radboud University, Nijmegen, The Netherlands, 3-7 July 2017
ABSTRACT. Hidden-variable (HV) theories allege that a quantum state describes an ensemble of systems distinguished by the values of hidden variables. No-go theorems assert that HV theories cannot match the predictions of quantum theory. The present work started with repairing flaws in the literature on no-go theorems asserting that HV theories cannot predict the expectation values of measurements. That literature gives one an impression that expectation no-go theorems subsume the time-honored no-go theorems asserting that HV theories cannot predict the possible values of measurements. But the two approaches speak about different kinds of measurement. This hinders comparing them to each other. Only projection measurements are common to both. Here, we sharpen the results of both approaches so that only projection measurements are used. This allows us to clarify the similarities and differences between the two approaches. Neither one dominates the other.
[233]
Andreas Blass and Yuri Gurevich
On the rectilinear Steiner problem
Bulletin of the EATCS
121 Feb 2017
ABSTRACT. This is a gentle introduction to the Rectilinear Steiner Problem. The interest in the Rectilinear Steiner Problem is related to the Very Large-Scale Integration (VLSI) technology that combines thousands of transistors into a single chip. Our note is based on the pioneering paper of Maurice Hanan. The main result of Hanan is an algorithm reducing any solution to a solution within a so-called Hanan grid. We simplify Hanan's algorithm.
[232]
Yuri Gurevich and Vladimir Vovk
Test statistics and p-values
Proceedings of Machine Learning Research 105 2019 89–104
COPA 2019: 8th Symposium on Conformal and Probabilistic Prediction with Applications,
also arXiv:1702.02590v2
ABSTRACT. We point out that the traditional notion of test statistic is too narrow, and we propose a natural generalization that is arguably maximal. The study is restricted to simple statistical hypotheses.
[231]
Yuri Gurevich
The 1966 International Congress of Mathematicians: A micro-memoir
Bulletin of the EATCS 120 October 2016
also arXiv:2112.04900
Fundamenta Informaticae 186 (1--4) 133--141 2022
DOI 10.3233/FI-222122
ABSTRACT. To an extent, the 1966 congress was a hole in the iron curtain. At least that how a young Soviet mathematician saw it.
[230]
Yuri Gurevich, Neta Haiby, Efim Hudis, Jeannette M. Wing and Elad Ziklik
Biggish: A solution for the inverse privacy problem
Microsoft Research, MSR-TR-2016-24 (May 2016)
An item of your personal information is inversely private if some party has access to it but you do not. Inverse privacy is ubiquitous. Each interaction you have with commercial and other institutions generates inversely private data. The inverse privacy problem is unjustified inaccessibility of your inversely private data to you. Elsewhere a subset of these authors determined that the problem has a market-based solution that provides consumers with large amounts of their personal data to be mined and processed to benefit them. Here we sketch a particular solution.
[229]
Yuri Gurevich and Vladimir Vovk
Fundamentals of p-values: Introduction
arXiv:1603.03952
We explain the concept of p-values presupposing only rudimentary probability theory. We also use the occasion to introduce the notion of p-function, so that p-values are values of a p-function. The explanation is restricted to the discrete case with no outcomes of zero probability. We are going to address the general case elsewhere.
[228]
Andreas Blass and Yuri Gurevich
On Hidden Variables: Value and Expectation No-Go Theorems
arXiv:1509.06896
No-go theorems assert that hidden-variable theories, subject to appropriate hypotheses, cannot reproduce the predictions of quantum theory. We examine two species of such theorems, value no-go theorems and expectation no-go theorems. The former assert that hidden-variables cannot match the predictions of quantum theory about the possible values resulting from measurements; the latter assert that hidden-variables cannot match the predictions of quantum theory about the expectation values of measurements. We sharpen the known results of both species, which allows us to clarify the similarities and differences between the two species. We also repair some flaws in existing definitions and proofs.
[227]
Yuri Gurevich
Past Present
International Journal of Foundations of Computer Science
27:2 (2016) 103–107
In 2014, the Development in Language Theory conference took place in the city of Yekaterinburg, in the Ural mountains of Russia. I used to live there. In Soviet times, there were no international conferences in the city. The whole region of the Urals was closed to foreigners. As I walked the streets of Yekaterinburg, I thought of my friends there and of Faulkner's lines ``The past is never dead. It isn't even past.''
[226]
Andreas Blass and Yuri Gurevich
Spekkens's Symmetric No-Go Theorem
arXiv:1503.08084
In a 2008 paper, Spekkens improved the traditional notions of non-negativity of Wigner-style quasi-probability distributions and non-contextuality of observations. He showed that the two improved notions are equivalent to each other. Then he proved what he called an even-handed no-go theorem. The paper contains some minor inaccuracies and one false claim, in the proof of the no-go theorem. This claim, early in the proof, is used in an essential way in the rest of the argument. Here we analyze carefully Spekkens's proof of the no-go theorem, explain the inaccuracies, reduce the task of proving the no-go theorem to the special case of a single qubit, and then prove the special case. This gives us a complete proof of Spekkens's no-go theorem.
[225]
Andreas Blass and Yuri Gurevich
On quantum computation, anyons, and categories
Chapter in "Martin Davis on Computability, Computational Logic,
and Mathematical Foundations," Pages 209-241
Springer 2016, DOI 10.1007/978-3-319-41842-1
We explain the use of category theory in describing certain sorts of anyons. Yoneda's lemma leads to a simplification of that description. For the particular case of Fibonacci anyons, we also exhibit some calculations that seem to be known to the experts but not explicit in the literature.
[224]
Andreas Blass and Yuri Gurevich
Negative probabilities
Bulletin of the EATCS 115 February 2014
arXiv:1502.00666
The uncertainty principle asserts a limit to the precision with which position x and momentum p of a particle can be known simultaneously. You may know the probability distributions of x and p individually but the joint distribution makes no physical sense. Yet Wigner exhibited such a joint distribution f(x,p). There was, however, a little trouble with it: some of its values were negative. Nevertheless Wigner's discovery attracted attention and found applications. There are other joint distribution, all with negative values, which produce the correct marginal distributions of x and p. But only Wigner's distribution produces the correct marginal distributions for all linear combinations of position and momentum. We offer a simple proof of the uniqueness and discuss related issues.
[223]
Andreas Blass, Alex Bocharov and Yuri Gurevich
Optimal Ancilla-free Pauli+V Circuits for Axial Rotations
Journal of Mathematical Physics 56 (2015) 122201
arXiv:1412.1033
Recently Neil Ross and Peter Selinger analyzed the problem of approximating z-rotations by means of single-qubit Clifford+T circuits. Their main contribution is a deterministic-search technique which allowed them to make approximating circuits shallower.
We adapt the deterministic-search technique to the case of Pauli+V circuits and prove similar results. Because of the relative simplicity of the Pauli+V framework, we use much simpler geometric methods.
[222]
Yuri Gurevich, Efim Hudis, and Jeannette Wing
Inverse Privacy
Communications of ACM 50:7 (July 2016) 38--42
We say that an item of your personal information is private if you have it but nobody else does. It is inversely private if somebody has it but you do not. We analyze the provenance of inverse privacy and argue that technology and appropriate public policy can reduce inverse privacy to a minimum.
[221]
Carlos Cotrini, Yuri Gurevich, Ori Lahav, and Artem Melentyev
Primal Infon Logic with Conjunctions as Sets
Springer Lecture Notes in Computer Science 8705 (2014), 236-249
TCS 2014, 8th IFIP International Conference
on Theoretical Computer Science
Primal infon logic was proposed by Gurevich and Neeman as an effcient yet expressive logic for policy and trust management. It is a propositional multimodal subintuitionistic logic decidable in linear time. However in that logic the principle of the replacement of equivalents fails. For example, (x ∧ y) → z does not entail (y ∧ x) → z, and similarly w → ((x ∧ y) ∧ z) does not entail w → (x ∧ (y ∧ z)). Imposing the full principle of the replacement of equivalents leads to an NP-hard logic according to a recent result of Beklemishev and Prokhorov. In this paper we suggest a way to regain the part of this principle restricted to conjunction: We introduce a version of propositional primal logic that treats conjunctions as sets, and show that the derivation problem for this logic can be decided in linear expected time and quadratic worst-case time.
[220]
Andreas Blass and Yuri Gurevich
Ancilla approximable quantum state transformations
Journal of Mathematical Physics 56:4, 042201 (2015)
arXiv:1403.7815v1
We consider the transformations of quantum states obtainable by a process of the following sort. Combine the given input state with a specially prepared initial state of an auxiliary system. Apply a unitary transformation to the combined system. Measure the state of the auxiliary subsystem. If (and only if) it is in a specified final state, consider the process successful, and take the resulting state of the original (principal) system as the result of the process. We review known information about exact realization of transformations by such a process. Then we present results about approximate realization of finite partial transformations. We consider primarily the issue of approximation to within a specified positive ε, but we also address the question of arbitrarily close approximation.
[219a]
Yuri Gurevich
On semantics-to-syntax analyses of algorithms
In PhML-2014, Philosophy, Mathematics, Linguistics: Aspects of Interaction 2014
International interdisciplinary conference, April 21-25, 2014, St. Petersburg, Russia
This paper was conceived as an extended abstract, an appetizer of a kind, for 219. But it was written after the fact and contains a number of observations not present in 219.
[219]
Yuri Gurevich
Semantics-to-syntax analyses of algorithms
A chapter in G. Sommaruga and T. Strahm (eds.),
Turing's Revolution - The Impact of His Ideas about Computability,
Birkhäuser/Springer 2015, pages 187-206.
This article is a much revised and extended version of 210.
Alan Turing pioneered semantics-to-syntax analysis of algorithms. You start with a large species of algorithms, and you finish up with a syntactic artifact that characterizes the species, typically a kind of machines that compute all and only the algorithms of the species.
The task of analyzing a large species of algorithms seems daunting if not impossible. As in quicksand, one needs a rescue point, a fulcrum. In computation analysis, a fulcrum is a particular viewpoint on computation that clarifies and simplifies things to the point that analysis become possible.
We review from that point of view Turing's analysis of human-executable computation, Kolmogorov's analysis of sequential bit-level computation, Gandy's analysis of a species of machine computation, and our own analysis of sequential computation.
[218]
Rui Wang, Yuchen Zhou, Shuo Chen, Shaz Qadeer, David Evans, and Yuri Gurevich
Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization
Proc. 22nd USENIX Security Symposium (USENIX Security '13), 399-414
held August 14-16, 2013, at Washington, D.C.
Preliminary version:
Microsoft Research technical report
MSR-TR-2013-37, March 2013
Most modern applications are empowered by online services, so application developers frequently implement authentication and authorization. Major online providers, such as Facebook and Microsoft, provide SDKs for implementing authentication and authorization. This paper considers whether those SDKs enable typical developers to build secure apps. Our work focuses on explicating implicit assumptions that are necessary for secure use of an SDK. Understanding these assumptions depends critically on not just the SDK itself, but on the underlying runtime systems with which the SDK interacts. Our work develops a systematic process for identifying critical implicit assumptions by building semantic models that capture both the logic of the SDK and the essential aspects of underlying systems. These semantic models provide the explicit basis for reasoning about the SDK's security. We use a formal analysis tool, along with the semantic models, to reason about all apps that can be built using the SDK. In particular, we formally check whether the SDK, along with the explicitly-captured assumptions, is sufficient to imply the desired security properties. We applied our approach to several widely used authentication/authorization SDKs. Our approach led to the discovery of several implicit assumptions in each SDK, including issues deemed serious enough to receive Facebook bug bounties and change the OAuth 2.0 specification. We verified that many apps constructed with these SDKs (indeed, the majority of apps in our study) are vulnerable to serious exploits because of these implicit assumptions, and we built a prototype testing tool that can detect several of the vulnerability patterns we identified.
[217]
Alex Bocharov, Yuri Gurevich and Krysta M. Svore
Efficient Decomposition of Single-Qubit Gates into V Basis Circuits
Physical Review A 88:1, 012313 (2013) [13 pages]
Preliminary version at
arXiv:1303.1411
We develop efficient algorithms for compiling single-qubit unitary gates into circuits over the universal V basis. The V basis is an alternative universal basis to the more commonly basis consiting of Hadamard and π/8 gates. We propose two classical algorithms for quantum circuit compilation: the first algorithm has expected polynomial time (in precision log(1/ε)) and produces an ε approximation to a single-qubit unitary with circuit depth ≤ 12 log5(2/ε). The second algorithm performs optimized direct search and yields circuits a factor of 3 to 4 times shorter than our first algorithm, but requires time exponential in log(1/ε); however, we show that in practice the runtime is reasonable for an important range of target precisions. Decomposing into the V basis may offer advantages when considering the fault-tolerant implementation of quantum circuits.
[216]
Andreas Blass, Guido de Caso and Yuri Gurevich
An Introduction to DKAL
Microsoft Research technical report MSR-TR-2012-108
We describe the current version of the Distributed Knowledge Authorization Language (DKAL) and some proposed extensions. The changes, in comparison with previous versions on DKAL, include an extension of primal infon logic to include a weak form of disjunction, the explicit binding of variables in infons and in rules, the possibility of updating a principal's policy, a more detailed treatment of a principal's datasources, and the introduction of DKAL communities.
[215]
Carlos Cotrini and Yuri Gurevich
Basic primal infon logic
Journal of Logic and Computation 26:1 (February 2016) 117-141
doi:10.1093/logcom/ext021
Preliminary version:
Microsoft Research technical report
MSR-TR-2012-88
Primal infon logic (PIL) was introduced in 2009 in the framework of policy and trust management. In the meantime, some generalizations appeared, and there have been some changes in the syntax of the basic PIL. This paper is on the basic PIL, and one of our purposes is to ``institutionalize'' the changes. We prove a small-model theorem for the propositional fragment of basic primal infon logic (PPIL), give a simple proof of the PPIL locality theorem, and present a linear-time decision algorithm (announced earlier) for PPIL in a form convenient for generalizations. For the sake of completeness, we cover the universal fragment of basic primal infon logic. We wish that this paper becomes a standard reference on basic primal infon logic.
[214]
Yuri Gurevich
Datalog: A perspective and the potential
Published in "Datalog 2.0," P. Barceló and R. Pichler (Eds.)
Springer Lecture Notes in Computer Science 7494 (2012), pp. 9-20.
Preliminary version: Microsoft Research technical report MSR-TR-2012-64
Our main goal is to put Datalog into a proper logic perspective. It may be too early to put Datalog into a proper perspective from the point of view of applications; nevertheless we discuss why Datalog pops up so often in applications.
[213]
Cristian S. Calude
"Yuri Gurevich: Mathematics, Computer Science and Life"
Chapter 23 in
The Human face of computing,
Imperial College Press 2015
Published first as
A Dialogue with Yuri Gurevich about Mathematics, Computer Science and Life
Bulletin of the EATCS 107 June 2012 30-40
[212]
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, and Nikhil Swamy
DKAL*: Constructing Executable Specifications of Authorization Protocols
In: Engineering Secure Software and Systems
5th International Symposium, ESSoS 2013
Lecture Notes in Computer Science 7781 (2013), 139-154
Preliminary version:
Microsoft Research technical report MSR-TR-2012-24
Many prior trust management frameworks provide authorization logics for specifying policies based on distributed trust. However, to implement a security protocol using these frameworks, one usually resorts to a general-purpose programming language. When reasoning about the security of the entire system, one must study not only policies in the authorization logic but also hard-to-analyze implementation code.
This paper proposes DKAL*, a language for constructing executable specifications of authorization protocols. Protocol and policy designers can use the DKAL* authorization logic for expressing distributed trust relationships, and its small rule-based programming language to describe the message sequence of a protocol. Importantly, many low-level details of the protocol (e.g., marshaling formats or management of state consistency) are left abstract in DKAL*, but sufficient details must be provided in order for the protocol to be executable.
We formalize the semantics of DKAL*, giving it both an operational semantics and a type system. We prove various properties of DKAL*, including type soundness and a decidability property for its underlying logic. We also present an interpreter for DKAL*, mechanically verified for correctness and security. We evaluate our work experimentally on several examples. Using our semantics, DKAL* programs can be analyzed for various protocol-specific properties of interest. Using our interpreter, programmers obtain an executable version of their protocol which can readily be tested and then deployed.
[211]
Carlos Cotrini and Yuri Gurevich
Transitive Primal Infon Logic: the Propositional Case
The Review of Symbolic Logic 6:2 (2013), 281-304
Preliminary version:
Microsoft Research technical report
MSR-TR-2012-15
Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives "p said" indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for many common access control scenarios. The most obvious limitation on its expressivity is the failure of the transitivity law for implication: x → y and y → z do not necessarily yield x → z. Here we introduce and investigate equiexpressive "transitive" extensions TPIL and TPIL* of propositional primal infon logic as well as their quote-free fragments TPIL0 and TPIL0* respectively. We prove the subformula property for TPIL0* and a similar property for TPIL*; we define Kripke models for the four logics and prove the corresponding soundness-and-completeness theorems; we show that, in all these logics, satisfiable formulas have small models; but our main result is a quadratic-time derivation algorithm for TPIL*.
[210]
Yuri Gurevich
Foundational Analyses of Computation
in How the World Computes (eds. S. Barry Cooper et al.)
Turing Centenary Conference and 8th Conf. on Computability in Europe (CiE 2012)
held in Cambridge, England, in June 2012
Springer Lecture Notes in Computer Science 7318, 264-275
Originally appeared as Microsoft Research Tech Report MSR-TR-2012-14
How can one possibly analyze computation in general? The task seems daunting if not impossible. There are too many different kinds of computation, and the notion of general computation seems too amorphous. As in quicksand, one needs a rescue point, a fulcrum. In computation analysis, a fulcrum is a particular viewpoint on computation that clarifies and simplifies things to the point that analysis become possible.
We review from that point of view the few foundational analyses of general computation in the literature: Turing's analysis of human computations, Gandy's analysis of mechanical computations, Kolmogorov's analysis of bit-level computation, and our own analysis of computation on the arbitrary abstraction level.
[209a]
Yuri Gurevich
What is an Algorithm? (Revised)
In Church's Thesis: Logic, Mind and Nature
(eds. A. Olszewski et al.)
Copernicus Center Press 2014.
This is a revised version of article 209.
[209]
Yuri Gurevich
What is an Algorithm?
in SOFSEM 2012: Theory and Practice of Computer Science (eds. M. Bielikova et al.)
Springer Lecture Notes in Computer Science 7147 (2012), 31-42
Originally appeared as Microsoft Research Tech Report MSR-TR-2011-116
We attempt to put the title problem and the Church-Turing thesis into a proper perspective and to clarify some common misconceptions related to Turing's analysis of computation. We examine two approaches to the title problem, one well-known among philosophers and another among logicians.
[208]
Nikolaj Bjorner, Guido de Caso and Yuri Gurevich
From Primal Infon Logic with Individual Variables to Datalog
Springer Lecture Notes in Computer Science 7265 (2012), 72-86
Preliminary version: Microsoft Research technical report
MSR-TR-2011-84, July 2011
The logic core of Distributed Knowledge Authorization Logic, DKAL, is constructive logic with a quotation construct "said". This logic is known as the logic of infons. The primal fragment of infon logic is amenable to linear time decision algorithms when policies and queries are ground. In the presence of policies with variables and implicit universal quantification, but no functions of positive arity, primal infon logic can be reduced to Datalog. We here present a practical reduction of the entailment problem for primal infon logic with individual variables to the entailment problem of Datalog.
[207]
Yuri Gurevich
Two notes on propositional primal logic
Microsoft Research technical report MSR-TR-2011-70, May 2011
Propositional primal logic, as defined by Gurevich and Neeman,
has two kinds of quotations: p said φ, and p implied φ.
Note 1. The derivation problem for propositional primal logic with one
kind of quotations is solvable linear time.
Note 2. In the Hilbertian calculus for propositional primal logic, the
shortest derivation of a formula φ from hypotheses H may be
exponential in the length of (H,φ).
[206]
Yuri Gurevich and Grant Olney Passmore
Impugning Randomness, Convincingly
[206a]
Tech report MSR-TR-2011-64
Microsoft Research technical report, May 2011
[206b]
BEATCS article (same text)
Bulletin of the EATCS 104 June 2011
[206c] Same text + a Prologue
Studia Logica 82 (2012), a special issue devoted to the memory of Leo Esakia, 1-31
Here is that Prologue all by itself.
John organized a state lottery and his wife won the main prize. You may feel that the event of her winning wasn't particularly random, but how would you argue that in a fair court of law? Traditional probability theory does not even have the notion of random events. Algorithmic information theory does, but it is not applicable to real-world scenarios like the lottery one. We attempt to rectify that.
[205]
Lev Beklemishev and Yuri Gurevich
Propositional primal logic with disjunction
Journal of Logic and Computation 24(1) 257-282 2014
Oxford University Press
(First published online May 29, 2012; doi: 10.1093/logcom/exs018)
Gurevich and Neeman introduced Distributed Knowledge Authorization Language (DKAL). The world of DKAL consists of communicating principals computing their own knowledge in their own states. DKAL is based on a new logic of information, the so-called infon logic, and its efficient subsystem called primal logic. In this paper we simplify Kripkean semantics of primal logic and study various extensions of it in search to balance expressivity and efficiency. On the proof-theoretic side we develop cut-free Gentzen-style sequent calculi for the original primal logic and its extensions.
[204]
Andreas Blass and Yuri Gurevich
Hilbertian Deductive Systems, Infon Logic, and Datalog
Information and Computation 231 21-37 2013
An earlier version appeared in the Bull. of EATCS, 102 (October 2010), 122-150
ABSTRACT. In the first part of the paper, we discuss abstract Hilbertian deductive systems; these are systems defined by abstract notions of formula, axiom, and inference rule. We use these systems to develop a general method for converting derivability problems, from a broad range of deductive systems, into the derivability problem in a quite specific system, namely the Datalog fragment of universal Horn logic. In this generality, the derivability problems may not be recursively solvable, let alone feasible; in particular, we may get Datalog ``programs'' with infinitely many rules. We then discuss what would be needed to obtain computationally useful results from this method. In the second part of the paper, we analyze a particular deductive system, primal infon logic with variables, which arose in the development of the authorization language DKAL. A consequence of our analysis of primal infon logic with variables is that its derivability problems can be translated into Datalog with only a quadratic increase of size.
[203]
Andreas Blass, Yuri Gurevich, Michal Moskal and Itay Neeman
Evidential Authorization
In
The Future of Software Engineering
Sebastian Nanz (ed.), Springer, 2011, pages 77-99.
Consider interaction of principals where each principal has its own policy and different principals may not trust each other. In one scenario the principals could be pharmaceutical companies, hospitals, biomedical labs and health related government institutions. In another scenario principals could be navy fleets of different and not necessarily friendly nations. In spite of the complexity of interaction, one may want to prove that certain properties remain invariant. For example, in the navy scenario, each fleet should have enough assurances from other fleets to avoid unfortunate incidents. Furthermore, one want to use automated provers to prove invariance. A natural approach to this problem is to provide a high-level logic-based language for the principals to communicate. We do just that. Three years ago two of us presented the first incarnation of Distributed Knowledge Authorization Language (DKAL). Here we present a new and much different incarnation of DKAL that we call Evidential DKAL. Statements communicated in Evidential DKAL are supposed to be accompanied with sufficient justifications.
[202]
Andreas Blass, Yuri Gurevich and Efim Hudis
The Tower-of-Babel Problem, and Security Assessment Sharing
1. Microsoft Research technical report MSR-TR-2010-57, May 2010
2. Bulletin of the EATCS 101 June 2010 161-182
The tower-of-Babel problem is rather general: How to enable a collaboration among experts speaking different languages? A computer security version of the tower-of-Babel problem is rather important. A recent Microsoft solution for that security problem, called Security Assessment Sharing, is based on this idea: A tiny common language goes a long way. We construct simple mathematical models showing that the idea is sound.
[201]
Andreas Blass, Nachum Dershowitz and Yuri Gurevich
Exact Exploration and Hanging Algorithms
In CSL 2010, 19th EACSL Annual Conference on Computer Science Logic
Springer Lecture Notes in Computer Science 6247, 2010, 140-154
Recent analysis of sequential algorithms resulted in their axiomatization and in a representation theorem stating that, for any sequential algorithm, there is an abstract state machine (ASM) with the same states, initial states and state transitions. That analysis, however, abstracted from details of intra-step computation, and the ASM, produced in the proof of the representation theorem, may and often does explore parts of the state unexplored by the algorithm. We refine the analysis, the axiomatization and the representation theorem. Emulating a step of the given algorithm, the ASM, produced in the proof of the new representation theorem, explores exactly the part of the state explored by the algorithm. That frugality pays off when state exploration is costly. The algorithm may be a high-level specification, and a simple function call on the abstraction level of the algorithm may hide expensive interaction with the environment. Furthermore, the original analysis presumed that state functions are total. Now we allow state functions, including equality, to be partial so that a function call may cause the algorithm as well as the ASM to hang. Since the emulating ASM does not make any superfluous function calls, it hangs only if the algorithm does.
[200]
Yuri Gurevich and Itay Neeman
DKAL 2 --- A Simplified and Improved Authorization Language
Microsoft Research Tech Report MSR-TR-2009-11, February 2009.
Knowledge and information are central notions in DKAL, a logic based authorization language for decentralized systems, the most expressive among such languages in the literature. Pieces of information are called infons. Here we present DKAL 2, a surprisingly simpler version of the language that expresses new important scenarios (in addition to the old ones) and that is built around a natural logic of infons. Trust became definable, and its properties, postulated earlier as DKAL house rules, are now proved. In fact, none of the house rules postulated earlier is now needed. We identify also a most practical fragment of DKAL where the query derivation problem is solved in linear time.
[199]
Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte, and Margus Veanes
Symbolic Bounded Model Checking of Abstract State Machines
International Journal of Software and Informatics
Vol.3, No.2-3, June/September 2009, pp. 149-170
Abstract State Machines (ASMs) allow us to model system behaviors at any desired level of abstraction, including levels with rich data types, such as sets or sequences. The availability of high-level data types allows us to represent state elements abstractly and faithfully at the same time. AsmL is a rich ASM-based specification and programming language. In this paper we look at symbolic analysis of model programs written in AsmL with a background T of linear arithmetic, sets, tuples, and maps. We first provide a rigorous account of the update semantics of AsmL in terms of background T, and we formulate the problem of bounded path exploration of model programs, or the problem of Bounded Model Program Checking (BMPC), as a satisfiability modulo T problem. Then we investigate the boundaries of decidable and undecidable cases for BMPC. In a general setting, BMPC is shown to be highly undecidable (Σ11-complete); restricted to finite sets, the problem remains RE-hard (Σ01-hard). On the other hand, BMPC is shown to be decidable for a class of basic model programs that are common in practice. We apply Satisfiability Modulo Theories (SMT) tools to BMPC. The recent SMT advances allow us to directly analyze specifications using sets and maps with specialized decision procedures for expressive fragments of these theories. Our approach is extensible; background theories need in fact only be partially solved by the SMT solver; we use simulation of ASMs to support additional theories that are beyond the scope of available decision procedures.
[198]
Yuri Gurevich and Itay Neeman
Infon Logic: the Propositional Case
ACM Transactions on Computational Logic 12:2, article 9, January 2011
The version available here corrects an oversight in the paper. An earlier version of the paper was published in Bulletin of the EATCS 98 (2009).
Infons are statements viewed as containers of information (rather then representations of truth values). In the context of access control the logic of infons is a conservative extension of logic known as constructive or intuitionistic. Distributed Knowledge Authorization Language uses additional unary connectives "p said" and "p implied" where p ranges over principals. Here we investigate infon logic and a narrow but useful primal fragment of it. In both cases, we develop model theory and analyze the derivability problem: Does the given query follow from the given hypotheses? Our more involved technical results are on primal infon logic. We construct an algorithm for the multiple derivability problem: Which of the given queries follow from the given hypotheses? Given a bound on the quotation depth of the hypotheses, the algorithm works in linear time. We quickly discuss the significance of this result for access control.
[197]
Yuri Gurevich and Arnab Roy
Operational Semantics for DKAL: Application and Analysis
TrustBus 2009, 6th International Conference on
Trust, Privacy and Security in Digital Business
Springer Lecture Notes in Computer Science 5695, pp. 149-158, 2009
DKAL is a new authorization language based on existential fixed-point logic and more expressive than existing authorization languages in the literature. We present some lessons learned during the first practical application of DKAL and some improvements that we made to DKAL as a result. We develop operational semantics for DKAL and present some complexity results related to the operational semantics.
[196]
Andreas Blass and Yuri Gurevich
Persistent Queries in the Behavioral Theory of Algorithms
ACM Transactions on Computational Logic
Volume 12, Issue 2, Article No. 16, January 2011.
An earlier version appeared as
Microsoft Research Tech Report MSR-TR-2008-150
We propose a syntax and semantics for interactive abstract state machines to deal with the following situation. A query is issued during a certain step, but the step ends before any reply is received. Later, a reply arrives, and later yet the algorithm makes use of this reply. By a persistent query, we mean a query for which a late reply might be used. Syntactically, our proposal involves issuing, along with a persistent query, a location where a late reply is to be stored. Semantically, it involves only a minor modification of the existing theory of interactive small-step abstract state machines.
[195]
Nikolaj Bjørner, Andreas Blass, Yuri Gurevich,
and Madan Musuvathi
Modular difference logic is hard
Microsoft Research Tech Report MSR-TR-2008-140
In connection with machine arithmetic, we are interested in systems of constraints of the form x + k ≤ y + l. Over integers, the satisfiability problem for such systems is polynomial time. The problem becomes NP complete if we restrict attention to the residues for a fixed modulus N.
[194]
Andreas Blass and Yuri Gurevich
One Useful Logic That Defines Its Own Truth
33rd International Symposium on
Mathematical Foundations of Computer Science (MFCS 2008)
Springer Lecture Notes in Computer Science 5162, pages 1-15, 2008.
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
Two Forms of One Useful Logic:
Existential Fixed Point Logic and Liberal Datalog
Bulletin of the EATCS 95 June 2008 164-182
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
When Are Two Algorithms the Same?
Bulletin of Symbolic Logic 15:2 (2009), 145-168.
An earlier verion was published as
Microsoft Research technical report MSR-TR-2008-20, February 2008.
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.
[191conf]
Yuri Gurevich and Itay Neeman
DKAL: Distributed-Knowledge Authorization Language
21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 149-162.
Extended abstract of 191tr.
DKAL is a new declarative authorization language for distributed systems. It is based on existential fixed-point logic and is considerably more expressive than existing authorization languages in the literature. Yet its query algorithm is within the same bounds of computational complexity as e.g. that of SecPAL. DKAL's communication is targeted which is beneficial for security and for liability protection. DKAL enables flexible use of functions; in particular principals can quote (to other principals) whatever has been said to them. DKAL strengthens the trust delegation mechanism of SecPAL. A novel information order contributes to succinctness. DKAL introduces a semantic safety condition that guarantees the termination of the query algorithm.
[191tr]
Yuri Gurevich and Itay Neeman
DKAL: Distributed-Knowledge Authorization Language
First appeared as
Microsoft Research technical report MSR-TR-2007-116, August 2007.
This version is
Microsoft Research technical report MSR-TR-2008-09, January 2008.
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 Bjørner, Andreas Blass, and Yuri Gurevich
Content-Dependent Chunking for Differential Compression,
the Local Maximum Approach
Journal of Computer and System Sciences
Volume 76, Issues 3-4, May-June 2010, Pages 154-203
Originally published as
Microsoft Research technical report MSR-TR-2007-109, July 2007
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.
We propose two new algorithms for content-dependent chunking, and we compare their behavior, on random files, with each other and with previously used algorithms. One of our algorithms, the local maximum chunking method, has been implemented and found to work better in practice than previously used algorithms.
Theoretical comparisons between the various algorithms can be based on several criteria, most of which seek to formalize the idea that chunks should be neither too small (so that hashing and sending hash values become inefficient) nor too large (so that agreements of entire chunks become unlikely). We propose a new criterion, called the slack of a chunking method, which seeks to measure how much of an interval of agreement between two files is wasted because it lies in chunks that don't agree.
Finally, we show how to efficiently find the cutpoints for local maximum chunking.
[189]
Yuri Gurevich, Dirk Leinders and Jan Van den Bussche
A Theory of Stream Queries
11th International Symposium on Database Programming
Languages (DBPL 2007)
Springer Lecture Notes in Computer Science 4797 (2007), 153-168.
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
Proving Church's Thesis
Computer Science --- Theory and Applications
CSR 2007, 2nd International Symposium on Computer Science in Russia
Springer Lecture Notes 4649 (2007), 1-3
This is an extended abstract of the opening talk of CSR 2007. It is based on 188.
[188]
Nachum Dershowitz and Yuri Gurevich
A natural axiomatization of computability
and proof of Church's Thesis
Bulletin of Symbolic Logic 14:3 (Sept. 2008), 299-350
An earlier version was published as
Microsoft Research technical report MSR-TR-2007-85, July 2007
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
A Geometric Zero-One Law
The Journal of Symbolic Logic 74:3, Sep. 2009.
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
Background of Computation
Bulletin of the EATCS 92 June 2007
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 143, 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
Zero-One Laws: Thesauri and Parametric Conditions
Bulletin of the EATCS 91 February 2007 125-144
Reprinted in
Logic at the Crossroads: An Interdisciplinary View
Amitabha Gupta, Rohit Parikh, Johan van Benthem, eds.
Allied Publishers, New Delhi, 2007, pages 187-206
Reprinted in
Proof, Computation and Agency: Logic at the Crossroads
Amitabha Gupta, Rohit Parikh, Johan van Benthem, eds.
Springer 2011, pages 99-114
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 parametric conditions (Springer Lecture Notes in Mathematics 969, 1982) and our thesauri of 149. 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
Database Query Processing Using Finite Cursor Machines
Theory of Computing Systems 44:4 (April 2009), pages 533-560
An earlier version appeared in
ICDT 2007, International Conference on Database Theory
Springer Lecture Notes in Computer Science 4353 (2007), 284-298
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 Bjørner, Yuri Gurevich, Mark Manasse, Joe
Porkka
Optimizing File Replication over Limited-Bandwidth Networks
using Remote Differential Compression
Microsoft Research technical report MSR-TR-2006-157, November 2006
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
Interactive Small-Step Algorithms II:
Abstract State Machines and the Characterization Theorem
Logical Methods in Computer Science 3:4 (2007), paper 4.
Preliminary version:
Microsoft Research technical report
MSR-TR-2006-171, November 2006
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
ASMs in the Classroom: Personal Experience
in Logics of Specification Languages
editors Dines Bjørner and Martin C. Henson
Springer, 2008, pages 599-602
We share our experience of using abstract state machines for teaching computation theory at the University of Michigan.
[180]
Andreas Blass and Yuri Gurevich
A Note on Nested Words
Tech report MSR-TR-2006-139, Microsoft Research, October 2006
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
Can Abstract State Machines Be Useful in Language Theory?
Theoretical Computer Science 376 (2007) 17-29
Extended Abstract in Proc. DLT 2006 (Developments in Language Theory)
Eds. O.H. Ibarra and Z. Dang
Springer Lecture Notes in Computer Science 4036 (2006), pp. 14-19.
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
Program Termination, and Well Partial Orderings
ACM Transactions on Computational Logic 9:3 (July 2008)
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 α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 α1×...×αn is equal to the natural product of these ordinals.
[177a]
Yuri Gurevich and Tanya Yavorskaya
A more abstract bounded exploration postulate
arXiv:2201.05911 (June 2022)
In the technical report below (#177) we gave a more abstract form of the bounded exploration postulate that is in the spirit of the abstract state postulate and that is equivalent to the original bounded exploration postulate in the presence of the sequential time and abstract state postulates. We republish, with slight modifications, the relevant part (Part~1) of the technical report to make it easier to access.
[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 T1×...×Tn. 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.
A later 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. Main area: Finite model theory [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 156, 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 Main area: finite model theory 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, Fürer, 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 continuing column on Logic in Computer Science. One of the previous articles in the column was devoted to the zero-one laws for a number of logics playing prominent 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 φ(X,Y) and ψ(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 φ(Q,J) holds over the real line. The question arises whether, for every formula φ, the family F can be defined by means of a formula ψ(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 function H(x) that is equal x/2 rounded
down. There is a single-loop program P using only three variables x,y,z
such that the asserted program
is 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 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 φ P ψ where P is a program and φ, ψ are assertions. The language of programs varies; in the 1980 survey of K. Apt, 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 Str\"otmann of Siemens. Eventually he was reassigned away from ASM applications, 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 φ, there is a finite automaton A that solves the model checking problem for φ.
[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, do this: 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 upon the ASM syntax (and 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 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 Main area: finite model theory 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 But consider recursion more closely. When an algorithm A calls an algorithm B, a clone of B is created and this clone becomes a slave of A. This raises the idea of treating recursion as an implicitly multi-agent computation. Slave agents come and go, and the master/slave hierarchy serves as the stack.
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 we 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 the collection of all finite structures of a finitely axiomatizable class and if every K structure is rigid, then K permits a relatively simple uniform definition of linear order. That happens to be not the case. 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 Main area: finite and metafinite model theory 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 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, the second author showed 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 and Guest Authors [100]
Yuri Gurevich Main area: Computational complexity theory 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 Main area: AI 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 Areas: ASM, programming languages The method of successive refinement is used. The observation that C expressions do not contain statements gives rise to the first evolving algebra (ealgebra) 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 Main area: Average case complexity 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 Main area: Average case complexity 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 Main area: Logic We explain the zero-one laws for first-order logic and their generalizations to richer logics.
[94]
Yuri Gurevich Main area: Average case complexity We motivate, justify and survey the average case reduction theory.
[93]
Andreas Blass and Yuri Gurevich Main area: Average case complexity 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 Main area: ASM 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 Areas: Classical decision problem, logic A discussion on classical decision problem and related issues.
[90]
Yuri Gurevich Main area: Finite model theory 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.
While Theorem 3.1 is true, our proof of it fell through -- a unique such case in the history of the Gurevich-Shelah collaboration. Theorem 3.1 was later proved by Benjamin Rossman; see Proceedings of LICS 2005.
[89]
Yuri Gurevich and L. A. Moss Areas: ASM, programming languages 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 Main area: Computational complexity theory The first algebraic average-case complete problem is presented. See [97] in this connection.
[87]
Yuri Gurevich and Saharon Shelah Main area: Computational complexity theory 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 Areas: Game theory, logic Büchi's approah to the determinay of infinite games was original and not without a ontroversy. He resented determinacy proofs that did not live up to his standards of construtivity. We desribe the infinite games in question, disuss the onstrutivity of determinacy proofs and comment on Büchii's contributions to determinacy.
[85]
Yuri Gurevich Main area: Average case complexity 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 Areas: Game theory, logic 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 Areas: Database theory, finite model theory Our main result is that every datalog query expressible in first-order logic is bounded; in terms of classical model theory this is a kind of compactness theorem for finite structures. In
addition, we give some counter-examples delimiting the main result. [82]
Yuri Gurevich and Saharon Shelah Main area: Computational complexity theory 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 Main area: Computational complexity theory 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 Main area: Computational complexity theory 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 Main area: Model theory 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 57, 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 Main area: Computational complexity theory 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 Areas: ASM, programming languages 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 Main area: Average case complexity 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.
(The original FOCS'87 presentation can be found
here.)
[75]
Yuri Gurevich Main area: Computation theory 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 Areas: Finite model theory, computation theory The chapter consists of two quite different parts. [73]
Andreas Blass and Yuri Gurevich Main area: Logic 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 Areas: Computational complexity theory, finite model theory 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 Main area: Computational complexity theory 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.
The paper is based on a 1984 technical report.
[70]
Yuri Gurevich and Saharon Shelah Main area: Finite model theory 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 Main area: Distributed computing 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 Areas: Computational complexity theory, finite model theory 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 Main area: Finite model theory 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 Main area: Finite model theory 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 Main area: Model theory
In this chapter we make a case for the monadic second-order logic (that is
to say, for the extension of first-order logic allowing quantification
over monadic predicates) as a good source of theories that are both
expressive and manageable. [63]
Yuri Gurevich and Saharon Shelah Main area: Model theory Define a tree to be any partial order satisfying the following requirement: if (y < x and z < x) then (y < z or y = z or y > z). 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 temporal logic.
[62]
Yuri Gurevich and Saharon Shelah Main area: Model theory [61]
J. P. Burgess and Yuri Gurevich Main area: Model theory The main result is the decidability of the temporal theory of the real order.
[60]
Yuri Gurevich Main area: Finite model theory 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 Areas: Computational complexity theory, finite model theory 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 Main area: Classical decision problem [57]
Yuri Gurevich and Saharon Shelah Areas: Model theory, set theory 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 79.
[56]
Andreas Blass and Yuri Gurevich Main area: Computational complexity theory We consider the questions whether polynomial time
solutions for the easier problems of the list for 55 yield NP solutions for the harder
ones, or vice versa. We show that affirmative answers to several of these questions are equivalent to natural principles like NP = co-NP, (NP intersect co-NP) = P, and the shrinking principle for NP sets. We supplement known oracles with enough new ones to show that all questions considered have negative answers relative to some oracles. In other words, these questions cannot be answered affirmatively by means of relativizable polynomial-time Turing reductions. Finally, we show that the analogous questions in the framework where Borel sets play the role of polynomial time decidable sets have negative answers.
[55]
Andreas Blass and Yuri Gurevich Main area: Computational complexity theory
For an equivalence relation E on the words in some finite alphabet, we consider the recognition problem (decide whether two words are equivalent), the invariant problem (calculate a function constant on precisely the equivalence classes), the normal form problem (calculate a particular member of an equivalence class, given an arbitrary member) and the first member problem (calculate the first member of an equivalence class, given an arbitrary member). A solution for any of these problems yields solutions for all earlier ones in the list. We show that, for polynomial time recognizable E, the first member problem is always in the class ΔP2 (solvable in polynomial time with an oracle for an NP set) and can be complete for this class even when the normal form problem is solvable in polynomial time. To distinguish between the other problems in the list, we construct an E whose invariant problem is not solvable in polynomial time with an oracle for E (although the first member problem is in NPE ∩ co-NPE), and we construct an E whose normal form problem is not solvable in polynomial time with an oracle for a certain solution of its invariant problem.
[54]
Yuri Gurevich, L. J. Stockmeyer and Uzi Vishkin Main area: Computational complexity theory 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 Main area: Model theory In 1947, Post showed the word problem for semigroups to be undecidable. In 1950, Turing strengthened this result to cancellation semigroups, i.e. semigroups satisfying the cancellation property [52]
Yuri Gurevich and P. H. Schmitt Main area: Model theory [51]
Yuri Gurevich Areas: Computational complexity theory, finite model theory We prove that, under a natural interpretation over finite domains, [50]
Yuri Gurevich [49]
A. M. W. Glass and Yuri Gurevich Main area: Model theory The problem is proven to be undecidable.
[48]
Yuri Gurevich and Saharon Shelah Main area: Model theory
We replace Goedel's sophisticated combinatorial argument with a simple
probabilistic one.
[47]
Yuri Gurevich and Saharon Shelah Main area: Model theory
The negative solution is given.
[46]
Yuri Gurevich and Saharon Shelah Areas: Model theory, set theory 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 Areas: Model theory, set theory In a series of papers, Büchi proved the decidability of the monadic (second-order) theory of ω0, of all countable ordinals, of ω1, and finally of all ordinals < ω2. Here, assuming the consistency of a weakly compact cardinal, we prove that, in different set-theoretic worlds, the monadic theory of ω2 may be arbitrarily difficult (or easy).
[44]
Yuri Gurevich Main area: Model theory
It is well known that for all recursively enumerable sets X1, X2 there are disjoint recursively enumerable sets Y1, Y2 such that Yi is a subset of Xi and (Y1 ∪ Y2) = (X1 ∪ X2). Alistair Lachlan called distributed lattices satisfying this property separated. He proved that the first-order theory of finite separated distributed lattices is decidable. We prove here that the first-order theory of all separated distributed lattices is undecidable.
[43]
Clarke, N. Francez, Y. Gurevich and P. Sistla Areas: Distributed computing, model theory In the case of unbounded buffers, the negative answer follows from a result in [28].
[42]
Andreas Blass and Yuri Gurevich Main area: Computational complexity theory 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 Main area: Database theory Answering a question of Jeffrey Ullman, we prove that the problem in the title is shown to be undecidable.
[40]
Yuri Gurevich and Leo Harrington Areas: Game theory, model theory We prove a forgetful determinacy theorem saying that, for a wide class of infinitary games, one of the players has a winning strategy that is virtually memoryless: the player has to remember only bounded many bits of information. We use forgetful determinacy to give a transparent proof of Rabin's celebrated result that the monadic second-order theory of the infinite tree is decidable.
[39]
Yuri Gurevich Main area: Classical decision problem [38]
I. Gertsbakh and Y. Gurevich Main area: Transportation science [37]
Yuri Gurevich and Saharon Shelah Main area: Model theory In 1975 Annals of Mathematics Shelah interpreted true first-order arithmetic in the monadic theory of order under the assumption of the continuum hypothesis. The assumption is removed here.
[36]
Yuri Gurevich Main area: Model theory [35]
S. O. Aandraa, E. Boerger and Yuri Gurevich Main area: Classical decision problem [34]
Yuri Gurevich Main area: Model theory 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. "Unfortunately, Gurevich's proof ... contains a small gap, which we take the opportunity to fill. The oversight does not affect the core of the argument, but occurs at an 'obvious' place," kindly wrote Lutz Heindorf in his article "Moderate Families in Boolean Algebras" in Annals of Pure and Applied Logic 57 (1992), 217-250.
[33]
A. M. W. Glass, Y. Gurevich, W. C. Holland and M. Jambu-Giraudet Main area: Model theory [32]
A. M. W. Glass, Yuri Gurevich, W. C. Holland and Saharon Shelah Main area: Model theory [31]
Yuri Gurevich and W. C. Holland Main area: Model theory We exhibit a first-order statement about the automorphisms group of the real line that characterizes the real line among all homogeneous chains.
[30]
Yuri Gurevich Main area: Model theory [29]
Yuri Gurevich and Saharon Shelah Main area: Model theory 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 Main area: Model theory The composition (or decomposition) method of Feferman-Vaught is generalized and made much more applicable.
[27]
Yuri Gurevich Main area: Model theory Assuming the Continuum Hypothesis, we interprete the theory of (the cardinal of) continuum with quantification over constructible (monadic, dyadic, etc.) predicates in the monadic (second-order) theory of real line, in the monadic theory of any other short non-modest chain, in the monadic topology of Cantor's Discontinuum and some other monadic theories. We exhibit monadic sentences defining the real line up to isomorphism under some set-theoretic assumptions. There are some other results.
[26]
Yuri Gurevich Main area: Model theory We disprove two Shelah's conjectures and prove some more results on the monadic theory of linearly orderings and topological spaces. In particular, if the Continuum Hypothesis holds then there exist monadic formulae expressing the predicates ``X is countable'' and ``X is meager'' over the real line and over Cantor's Discontinuum.
[25]
Yuri Gurevich Main area: Model theory The first-order theory of ordered abelian groups was analyzed in 3. However, algebraic results on ordered abelian groups in the literature usually cannot be stated in first-order logic. Typically they involve so-called convex subgroups. Here we introduce an expanded theory of ordered abelian groups that allows quantification over convex subgroups and expresses almost all relevant algebra. We classify ordered abelian groups by the properties expressible in the expanded theory, and we prove that the expanded theory of ordered abelian groups is decidable. Curiously, the decidability proof is simpler than that in 3. Furthermore, the decision algorithm is primitive recursive.
This is a journal version of 19 which could not be published in USSR for non-scientific reasons.
[24]
Yuri Gurevich Main area: Proof theory Classical logic is symmetric with respect to True and False but intuitionistic logic is not. We introduce and study a conservative extension of first-order intuitionistic logic that is symmetric with respect to True and False.
[23]
I. Gertsbakh and Y. Gurevich Main area: Transportation science A general method for constructing all optimal fleets is described.
[22]
Yuri Gurevich Main area: Classical decision problem Let K and L be classses of first-order formulas and f an algorithm with inputs in K and outputs in L. Recall that f is a concervative reduction of K to L if the following four conditions hold: [21]
Yuri Gurevich Main area: Classical decision problem The classification of prefix-signature fragments of (first-order) predicate logic with equality, completed in [7], is extended to first-order logic with equality and functions. One case was solved (confirming a conjecture of this author) by Saharon Shelah.
[20]
Yuri Gurevich Main area: Classical decision problem
This was supposed to be a book but the publication was aborted when the author left USSR. A German translation can be found (at least was found in past) in Universitaetsbibliothek Dortmund (Ostsprachen-Übersetzungsdienst) und TIB Hannover.
[19]
Yuri Gurevich Main area: Model theory The story of this manuscript may be of interest to the students of the Antisemitism in Soviet Mathematics. In 1971, the manuscript was submitted to the Siberian Mathematical Journal (SMJ) but the SMJ has never replied to me (even though Ali Kokorin told me confidentially that he was the referee and wrote a great report). Eventually the paper appeared as a technical report of sorts at the Soviet Institute of Scientific and Technical Information (VINITI), number 6708-73, 1974, 1-31 (Russian). Later yet I published the paper on the West; see 25.
[18]
Yuri Gurevich Main area: Classical decision problem 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 satisfiability). This result completes the solution in 9 for the classical decision problem for first-order logic with functions but without equality.
[17]
Yuri Gurevich and Tristan Turashvili Main area: Classical decision problem [16en]
Yuri Gurevich and Igor O. Koriakov Main area: Classical decision problem [16]
Yuri Gurevich and Igor O. Koriakov Main area: Classical decision problemc
Berger proved that the decision problem for the unrestricted tiling problem (a.k.a. the unrestricted domino problem) is undecidable. We strengthen Berger's result. The following two collection of domino sets are recursively inseparable: Igor Koriakov was student of mine at the Ural State University.
[15]
Yuri Gurevich Main area: Classical decision problem
Using Minsky machines (rather than Turing machines), we give a simpler proof of the result in [7] that [AEA&E*,(k,1)] is a reduction class for some k.
[14en]
Yuri Gurevich Main area: Logic [14]
Yuri Gurevich Main area: Logic Consider the collection D of first-order formulas α such that the first-order theory with axiom α is decidable. It is proven that D is neither r.e. nor co-r.e. (The second part has been known earlier.)
[13en]
Yuri Gurevich Main area: Classical decision problem [13]
Yuri Gurevich Main area: Classical decision problem The article consists of two chapters. In the first part of the first chapter, the author rediscovers well-partial-orderings and well-quasi-orderings, which he calls tight partial orders and tight quasi orders, and develops a theory of such orderings. (In this connection, it may be appropriate to point out Joseph B. Kruskal's article ``The theory of well-quasi-ordering: A frequently discoverred concept'' in J. Comb. Theory A, vol. 13 (1972), 297-305.) To understand the idea behind the term "tight", think of a boot: you cannot move your foot far down or sidewise -- only up. This is similar to tight partial orders where infinite sequences have no infinite descending subsequences, no infinite antichains, but always have infinite ascending subsequences.
In the second part of the first chapter, the author applies the theory of tight orders to prove a classifiability theorem for prefix-vocabulary classes of first-order logic. The main part of the classifiability theorem is that the partial order of prefix-vocabulary classes (ordered by inclusion) is tight. But there is an additional useful part of the classifiability theorem, about the form of the minimal classes outside a downward closed collection, e.g. the minimal classes that are undecidable in one way or another.
In the second chapter, the author completes the decision problem for (the prefix-vocabulary fragments of) pure logic of predicates and functions, though the treatment of the most difficult decidable class is deferred to 18. In particular, the classes [∀2,(0,1),(1)] and [∀2,(1),(0,1)] are proved to be conservative reduction classes. (This abstract is written in January 2006.)
[12]
Yuri Gurevich Areas: Classical decision problem, Model theory
Extended Abstract of the thesis in Russian
September 2017. I believe that: [11]
Yuri Gurevich Main area: Model theory
This is a precursor of 19 [10en]
Yuri Gurevich Main area: Model theory This is an English translation of 10.
[10]
Yuri Gurevich Main area: Classical decision problem This is essentially an extended abstract of 9 in the Proceedings of the Soviet Academy of Sciences.
[9]
Yuri Gurevich Main area: Classical decision problem Delimiting the decidability result of [3] for linearly ordered abelian groups and answering Malcev's question, we prove the theorem in the title.
[8]
Yuri Gurevich Main area: Model theory The word problem for finite semigroups is the following decision problem: given some number n of word pairs (u1,v1), ..., (un,vn) and an additional word pair (u0,v0), decide whether the n equations u1=v1,..., un=vn impliy the additional equation u0=v0 in all finte semigroups. We prove that the word problem for finite semigroups is undecidable.
In fact, the undecidability result holds for a particular premise E =
(u1=v1 and ... and un=vn).
Furthermore, this particular E can be chosen so that the following classes K1 and K2 of word pairs are recursively inseparable: [7]
Yuri Gurevich Main area: Classical decision problem
This is a detailed exposition of the results announced in 6.
[6a]
Yuri Gurevich Main area: Classical decision problem This is an English translation of 6.
[6]
Yuri Gurevich Main area: Classical decision problem
The ∀∃∀∃* fragment of pure predicate logic with one binary and no unary predicates is a conservative reduction class and therefore undecidable for satisfiability and for finite satisfiability. This completes the solution of the classical decision problem for pure predicate logic: the prefix-vocabulary classes of pure predicate logic are fully classified into decidable and undecidable. See a more complete exposition in [7].
[5en]
Yuri Gurevich Main area: Classical decision problem This is an English translation of 5.
[5]
Yuri Gurevich Main area: Classical decision problem
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].
[4]
Yuri Gurevich Main area: Model theory We introduce a method of existential interpretation, and we use the method to prove the undecidability of fragments of the form ErA* of several popular first-order theories.
The results can be found in English in 12.8 and 36.
[3a]
Yuri Gurevich Main area: Model theory This is an English translation of 3.
[3]
Yuri Gurevich Main area: Model theory We classify ordered abelian groups are by first-order properties. Using that classification, we prove that the first-order theory of ordered abelian groups is decidable; this answers a question of Alfred Tarski.
[2]
Yuri Gurevich and Ali I. Kokorin Main area: Model theory We prove that no universal first-order property distinguishes between any two ordered abelian groups.
[1]
Yuri Gurevich Main area: Group theory Instead of abstract: I wrote my 3rd year term paper, a "coursework", with Valentin Konstantinovich Ivanov, the most known mathematician of the Ural State University, on the approximation theory of real functions. But Ivanov was a vice-rector and thus had little time. He advised me to go to computational mathematics (because "this is the future") or to join the group theory seminar (because "it was most active, and you need interaction"). The seminar, conducted by Petr Grigorievich Kontorovich, was indeed lively and well attended. Joining the seminar was a challenge. There was no tutorial introduction. You just attend the seminar and eventually you start to understand what they are talking about. On the wall, there was a list of open problems. The second of them asked whether there is a finite group with this property: every element belongs to a nontrivial characteristic subgroup. The positive answer is one of the results in the thesis.
Afterthought Items
in reverse-chronological order: [_2002] Yuri Gurevich for the Foundations of Software Engineering group Microsoft has been amazingly successful in shipping complex software within tight time constraints. But the time-tested development approach faces the challenges of large-scale, trustworthy, distributed computing. We describe some of the problems and argue that software modeling can and should play a greater role in solving the problems. To this end, we propose the AsmL language for writing software models: [_2001b]
Yuri Gurevich, Wolfram Schulte, and Margus Veanes Software industry can use a good executable specification language which allows one to integrate specifications with existing technologies. To meet this need, the Foundations of Software Engineering group at Microsoft Research builds a powerful extension of the original abstract state machines (for short ASMs). We call it ASML (for “ASM Language”).
[_2001a]
Colin Campbell and Yuri Gurevich Ideally, a good specification becomes the basis for implementing, testing and documenting the system it defines. In practice, producing a good specification is hard. [_1985] Yuri Gurevich The first announcement of the "new thesis" which evolved into
the Evolving Algebra thesis renamed later to the "Abstract State Machine thesis", for short the "ASM thesis".
[_1984] Yuri Gurevich The earliest (and rather naive) publication on the abstract state machine project.
Tech report MSR-TR-2006-07, Microsoft Research, January 2006
Interactive Small-Step Algorithms I: Axiomatization
Logical Methods in Computer Science 3:4 (2007), paper 3.
Preliminary version:
Microsoft Research technical report
MSR-TR-2006-170, November 2006
Membership Problem for Modular Group
SIAM Journal on Computing 37:2 (2007), 425-459
Interactive Algorithms 2005 with Added Appendix
Proceedings of MFCS 2005
Math Foundations of Computer Science, 2005, Gdansk, Poland
Editors J. Jedrzejowicz and A. Szepietowski
Springer Lecture Notes in Computer Science 3618 (2005), 26-38
Reprinted, with the appendix, in
Interactive Computation: The New Paradigm
eds. Dina Goldin, Scott A. Smolka, Peter Wegner
Springer-Verlag, 2006, pages 165-182
Play to Test
Microsoft Research, technical report MSR-TR-2005-04, January 2005
5th International Workshop on
Formal Approaches to Testing of Software (FATES 2005)
Edinburgh, July 2005
Why Sets?
Originally published in
Bulletin of the European Association for Theoretical Computer Science
Number 84 (October 2004)
Revised and published as
Microsoft Research technical report
MSR-TR-2006-138, September 2006
Reprinted in
"Pillars of Computer Science:
Essays Dedicated to Boris (Boaz)
Trakhtenbrot on the Occasion of His 85th Birthday"
Editors Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich
Lecture Notes in Computer Science 4800
Springer-Verlag, Berlin, 2008.
Ordinary Interactive Small-Step Algorithms, III
ACM Transactions on Computational Logic 8:3 (July 2007), article 16
a preliminary version was published as a part of MSR-TR-2004-88
(1) proceed in discrete, global steps,
(2) perform only a bounded amount of work in each step,
(3) use only such information from the environment as can be regarded as answers to queries, and
(4) never complete a step until all queries from that step have been answered.
After reviewing the previous papers' definitions of such algorithms, of behavioral equivalence, and of abstract state machines (ASMs), we prove the main result: Every ordinary, interactive, small-step algorithm is behaviorally equivalent to an ASM.
We also discuss some possible variations of and additions to the ASM semantics.
Ordinary Interactive Small-Step Algorithms, II
ACM Transactions on Computational Logic 8:3 (July 2007), article 15
a preliminary version was published as a part of MSR-TR-2004-88
(1) proceed in discrete, global steps,
(2) perform only a bounded amount of work in each step,
(3) use only such information from the environment as can be regarded as answers to queries, and
(4) never complete a step until all queries from that step have been answered.
After reviewing the previous paper's formal description of such algorithms and the definition of behavioral equivalence, we define ordinary, interactive, small-step abstract state machines (ASM's). Except for very minor modifications, these are the machines commonly used in the ASM literature. We define their semantics in the framework of ordinary algorithms, and we show that they satisfy the postulates for these algorithms.
This material lays the groundwork for the final paper in the series, in which we shall prove the Abstract State Machine Thesis for ordinary, intractive, small-step algorithms: All such algorithms are equivalent to ASMs.
Semantic Essence of AsmL
Theoretical Computer Science
Volume 343, issue 3, 17 October 2005, pages 370-412
Originally published as
Microsoft Research TR-2004-27, March 2004
Semantic Essence of AsmL: Extended Abstract
In Formal Methods of Components and Objects, FMCO 2003
Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf,
Willem-Paul de Roever, Editors
Springer Lecture Notes in Computer Science 3188 (2004), 240-259
Observations on the Decidability of Transitions
Abstract State Machines 2004
W. Zimmerman and B. Thalheim, editors
Springer Lecture Notes in Computer Science 3052 (2004), 161-168
Intra-Step Interaction
Abstract State Machines 2004
W. Zimmerman and B. Thalheim, editors
Springer Lecture Notes in Computer Science 3052 (2004), 1-5
Ordinary Interactive Small-Step Algorithms, I
ACM Transactions on Computational Logic
Vol. 7, no. 2 (April 2006), pages 363 - 419
a preliminary version was published as MSR-TR-2004-16
(1) proceed in discrete, global steps,
(2) perform only a bounded amount of work in each step,
(3) use only such information from the environment as can be regarded as
answers to queries, and
(4) never complete a step until all queries from that step have been
answered.
We indicate how a great many sorts of interaction meet these
requirements. We also discuss in detail the structure of queries and
replies and the appropriate definition of equivalence of
algorithms.
Finally, motivated by our considerations concerning queries, we discuss a
generalization of first-order logic in which the arguments of function
and relation symbols are not merely tuples of elements but orbits of such
tuples under groups of permutations of the argument places.
Abstract State Machines: An Overview of the Project
in "Foundations of Information and Knowledge Systems"
editors Dietmar Seipel and Jose Maria Turull-Torres
Springer Lecture Notes in Computer Science 2942 (2004), pages 6-13
Algorithms: A Quest for Absolute Definitions
Originally published in
Bulletin of the EATCS 81 October 2003 195-225
Reprinted in
"Current Trends in Theoretical Computer Science
Volume 2: Formal Models and Semantics"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 283-311, 2004
Reprinted in
Church's Thesis After 70 Years
(eds. A. Olszewski et al.)
Ontos Verlag, pages 24-57, 2006
Scenario-oriented Modeling in AsmL and Its Instrumentation for
Testing
Proc. of 2nd International Workshop on Scenarios and
State Machines:
Models, Algorithms, and Tools (pages 8-14)
held at ICSE 2003, International Conference on Software Engineering 2003
Spectra of Monadic Second-Order Formulas with One Unary
Function
18th Annual IEEE Symposium on Logic in Computer
Science
IEEE Computer Society, 2003, pages 291-300.
(In the web version, some additional proof details are provided because some readers asked for them.)
Partial Updates
Theoretical Computer Science
Volume 336, Issues 2-3 , 26 May 2005, Pages 311-342
(A preliminary version was published in "Abstract State Machines 2003"
Springer Lecture Notes in Computer Science 2589 (2003), pages 57-86.)
Pairwise Testing
Originally published in
Bulletin of the EATCS 78 October 2002 100-132
Reprinted in
"Current Trends in Theoretical Computer Science
Volume 2: Formal Models and Semantics"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 237-266, 2004
Abstract Communication Model for Distributed Systems
IEEE
Transactions on Software Engineering
Vol. 30, no. 7, July 2004,
pages 458-472.
Algorithms vs. Machines
Originally published in
Bulletin of the EATCS 77 June 2002 96-118
Reprinted in
"Current Trends in Theoretical Computer Science
Volume 2: Formal Models and Semantics"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 215-236, 2004
Abstract State Machines Capture Parallel Algorithms:
Correction and Extension
ACM Transactions on Computational Logic
Vol. 9, No. 3, Article 19, Publication date: June 2008
Abstract State Machines Capture Parallel Algorithms
Technical report MSR-TR-2001-117
ACM Transactions on Computational Logic
Volume 4, Number 4 (October 2003), pages 578-651
Partial Updates: Exploration
Springer J. of Universal Computer Science 7:11 (2001), 918-952.
Toward Industrial Strength Abstract State Machines
Technical report MSR-TR-2001-98
Microsoft Research, October 2001
Generating Finite State Machines from Abstract State Machines
ISSTA 2002, International Symposium on Software Testing and Analysis
ACM Software Engineering Notes 27:4 (2002), 112-122.
Universal Plug and Play Machine Models
Technical report MSR-TR-2001-59
Microsoft Research, June 2001
Fixed Point Logics
The Bulletin of Symbolic Logic 8:1 (2002), 65-88.
Logician in the land of OS: Abstract State Machines at Microsoft
Sixteenth Annual IEEE Symposium on Logic in Computer Science
IEEE Computer Society, 2001, 129-136.
A Quick Update on the Open Problems in article
[150]
December 2005.
On Polynomial Time Computation Over Unordered Structures
The Journal of Symbolic Logic 67:3 (2002), 1093-1125.
Strong Extension Axioms and
Shelah's Zero-One Law for Choiceless Polynomial Time
The Journal of Symbolic Logic 68:1 (2003), 65-131.
A New Zero-One Law and Strong Extension Axioms
Originally published in
Bulletin of the EATCS 72 October 2000 103-122
Reprinted in
"Current Trends in Theoretical Computer Science
Volume 2: Formal Models and Semantics"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 99-118, 2004
Definability in Rationals with Real Order in the Background
Journal of Logic and Computation 12:1 (2002), pp. 1-11
Inadequacy of Computable Loop Invariants
ACM Transactions on Computational Logic
Volume 2, Number 1 (January 2001), 1-11
Using Abstract State Machines at Microsoft: A Case Study
Proceedings of ASM'2000
in "Abstract State Machines: Theory and Applications"
Eds. Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele
Springer Lecture Notes in Computer Science 1912 (2000), 367-379
Choiceless Polynomial Time Computation and the Zero-One Law
Proceedings of CSL'2000
Editors Peter Clote and Helmut Schwichtenberg
Springer Lecture Notes in Computer Science 1862 (2000), 18-40.
Background, Reserve, and Gandy Machines
Proceedings of CSL'2000
Editors Peter Clote and Helmut Schwichtenberg
Springer Lecture Notes in Computer Science 1862 (2000), 1-17.
The Underlying Logic of Hoare Logic
Originally published in
Bulletin of the EATCS 70 February 2000 82-110
Reprinted in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 409-436, 2001
Finite Work
Tech report MSR-TR-2006-06, Microsoft Research, January 2006
Sequential Abstract State Machines capture Sequential Algorithms
Russian translation
Translated to Russian by P.G. Emelyanov
In System Informatics, vol. 9, pages 7-50. Ed. A.G. Marchuk
The Siberian Branch of the Russian Academy of Sciencies (1940)
Sequential Abstract State Machines capture Sequential Algorithms
ACM Transactions on Computational Logic
Volume 1, Number 1 (July 2000), pages 77-111
The paper also can be found at
the journal's webpage.
Investigating Java Concurrency Using Abstract State Machines
Proceedings of ASM'2000
in Abstract State Machines: Theory and Applications
Eds. Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele
Springer Lecture Notes in Computer Science 1912 (2000), 151-176.
Abstract state machines and
computationally complete query languages
Information and Computation 174:1 20-36 2002
---
An earlier version published in Proceedings of ASM'2000
"Abstract State Machines: Theory and Applications"
Eds. Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele
Springer Lecture Notes in Computer Science 1912 (2000), 22-33
Partially Ordered Runs: a Case Study
in "Abstract State Machines: Theory and Applications"
Eds. Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele
Springer Lecture Notes in Computer Science 1912 (2000), 131-150
Typed Abstract State Machines
Unfinished manuscript, 1998.
The Sequential ASM Thesis
Originally published in
Bulletin of the EATCS 67 February 1999 93-124
Reprinted in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 363-392, 2001
#141 is a much revised and polished journal version of this paper.
The Logic of Choice
The Journal of Symbolic Logic
Vol. 65, no. 3, September 2000, pages 1264-1310.
Existential Second-Order Logic over Strings
Journal of the ACM, vol. 47, no. 1, Jan. 2000, 77-131.
The Complexity of Query Reliability
1998 ACM Symposium on Principles of Database Systems (PODS'98).
A Variation on the Zero-One Law
Information Processing Letters 67 (1998) 29-30.
From Invariants to Canonization
Originally published in
Bulletin of the EATCS 63 October 1997
Reprinted in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 327-331, 2001
Definability and Undefinability with Real Order at the Background
J. of Symbolic Logic, vol. 65, no. 2 (2000), 946-958
May 1997 Draft of the ASM Guide
Tech Report CSE-TR-336-97, EECS Dept, University of Michigan, 1997
Monadic Simultaneous Rigid E-Unification
Theoretical Computer Science
volume 222, number 1-2 (1999), 133-152.
Monadic Simultaneous Rigid E-Unification and Related Problems
24th Intern. Colloquium on Automata, Languages and Programming
ICALP'97, Bologna, Italy, July 1997
Springer Lecture Notes in Computer Science 1256 (1997), 154-165
Decidability and Complexity of Simultaneous Rigid E-Unification
with One Variable and Related Results
Theoretical Computer Science
volume 243/1-2 (August 2000), 167-184.
The Decidability of Simultaneous Rigid E-Unification with One Variable
Tech. Rep. 139, March 1997
Computing Science Department, Uppsala University, Sweden
RTA'98, 9th Conf. on Rewriting Techniques and Applications
Tsukuba, Japan, March 30 --- April 1, 1998.
Logic with Equality: Partisan Corroboration and Shifted Pairing
Information and Computation 152:2 205-235 1999.
Herbrand's Theorem and Equational Reasoning: Problems and
Solutions
Originally published in
Bulletin of the EATCS 60 October 1996 78-95
Reprinted in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 303-326, 2001
Syntax vs. Semantics on Finite Structures
in "Structures in Logic and Computer Science:
A Selection of Essays in Honor of Andrzej Ehrenfeucht"
Editors J. Mycielski, G. Rozenberg and A. Salomaa
Lecture Notes in Computer Science 1261, 14-33
Springer-Verlag, Heidelberg, 1997.
Platonism, Constructivism, and Computer Proofs vs. Proofs by Hand
Originally published in
Bulletin of the EATCS 57 October 1995 145-166.
A slightly revised version is published in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 281-302, 2001
A Formal Approach to Recovery in Transaction-Oriented Database Systems
Springer J. of Universal Computer Science 3:4 (April 1997), 320-340.
Gurevich Abstract State Machines and
Schoenhage Storage Modification Machines
Springer J. of Universal Computer Science 3:4 (April 1997), 279-303.
Choiceless Polynomial Time
Annals of Pure and Applied Logic 100 (1999), 141-187.
Recursive Abstract State Machines
Springer J. of Universal Computer Science 3:4 (April 1997) 233-246.
(i) the ASM idea of explicit and comprehensive states, and
(ii) higher level recursion with its hiding of the stack.
The Linear Time Hierarchy Theorems for RAMs and Abstract State Machines
Springer J. of Universal Computer Science 3:4 (April 1997) 247-278
Equivalence is in the Eye of the Beholder
Theoretical Computer Science 179, 1-2 (1997), 353-380.
The Railroad Crossing Problem:
An Experiment with Instantaneous Actions and Immediate Reactions
in "Computer Science Logics, Selected papers from CSL'95"
ed. H. Kleine-Buening
Springer Lecture Notes in Computer Science 1092 (1996) 266-290
Normal Forms for Second-Order Logic over Finite Structures
and Classification of NP Optimization Problems
Annals of Pure and Applied Logic, 78 (1996), 111-125.
The Value, if any, of Decidability
Originally published in
Bulletin of the EATCS 55 February 1995 129-135
Reprinted in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 274-280, 2001
On Rigid Structures
The Journal of Symbolic Logic , vol. 61, no. 2, June 1996, 549-562.
Evolving Algebras
in "IFIP 1994 World Computer Congress,
Volume I: Technology and Foundations"
Eds. B. Pehrson and
I. Simon, Elsevier, Amsterdam, 423-427.
Evolving Algebras and Partial Evaluation
in "IFIP 1994 World Computing Congress, Volume 1:
Technology and Foundations"
Eds. B. Pehrson and I. Simon, Elsevier, Amsterdam, 587-592.
Evolving Algebras and Linear Time Hierarchy
in "IFIP 1994 World Computer Congress, Volume I:
Technology and Foundations"
Eds. B. Pehrson and I. Simon, North-Holland, Amsterdam, 383-390.
Metafinite Model Theory
Information and Computation 140:1 26-81 1998.
Preliminary version in
Logic and Computational Complexity, Selected Papers,
ed. D. Leivant
Springer Lecture Notes in Computer Science 960 (1995) 313-366
McColm's Conjecture
Symposium on Logic in Computer Science,
IEEE Computer Society Press, 1994, 10-19.
The Bakery Algorithm: Yet Another Specification and Verification
in Specification and Validation Methods
(ed. E. Boerger)
Oxford University Press, pages 231-243, 1995
Group Membership Protocol: Specification and Verification
in Specification and Validation Methods
(ed. E. Boerger)
Oxford University Press, pages 295-328, 1995
Logic Activities in Europe
ACM SIGACT NEWS, vol. 25, no. 2 (June 1994), 11-24.
Tailoring Recursion for Complexity
J. Symbolic Logic, vol. 60, no. 3, Sept. 1995, 952-969.
Evolving Algebra 1993: Lipari Guide
in Specification and Validation Methods
(ed. E. Boerger)
Oxford University Press, pages 9-36, 1995
Reprinted as arXiv:1808.06255
The AMAST Phenomenon
Originally published in
Bulletin of the EATCS 51 October 1993 295-299
Reprinted in
"Current Trends in Theoretical Computer Science:
Entering the 21st Century"
(eds. G. Paun, G. Rozenberg and A. Salomaa)
World Scientific, pages 247-253, 2001
Logic in Computer Science
Chapter in
"Current Trends in Theoretical Computer Science"
(eds. G. Rozenberg and A. Salomaa)
World Scientific Series in Computer Science
Volume 40, pages 223-394, 1993
Feasible Functions
London Mathematical Society Newsletter,
No. 206, June 1993, 6-7.
Curb Your Theory! A Circumscriptive Approach
for Inclusive Interpretation of Disjunctive Information
Proc. 13th Intern. Joint Conf. on AI (IJCAI'93)
ed. R. Bajcsy, Morgan Kaufman, 1993, 634-639.
The Semantics of the C Programming Language
CSL'92 (Computer Science Logics), Eds. E. Boerger et al.
Springer Lecture Notes in Computer Science 702 (1993) 274-308.
Matrix Transformation is Complete for the Average Case
SIAM Journal on Computing 24:1, 1995, 3-29.
Randomizing Reductions of Search Problems
SIAM Journal on Computing 22 (1993), no. 5, 949-975.
Zero-One Laws
Originally published in
Bulletin of the EATCS 51 February 1991 90-106
Reprinted in
"Current Trends in Theoretical Computer Science:
Essays and Tutorials"
(eds. G. Rozenberg and A. Salomaa)
World Scientific, pages 293-309, 1993
Average Case Complexity
ICALP'91,
International Colloquium on Automata, Languages and Programming
Madrid, Springer Lecture Notes in Computer Science 510 (1991) 615-628.
On the Reduction Theory for Average-Case Complexity
CSL'90, 4th Workshop on Computer Science Logic
Springer Lecture Notes in Computer Science 533 (1991) 17-30.
Evolving Algebras: An Introductory Tutorial
Originally in
Bulletin of the EATCS 43 February 1991 264-284
This slightly revised version appeared in
"Current Trends in Theoretical Computer Science:
Essays and Tutorials"
(eds. G. Rozenberg and A. Salomaa)
World Scientific, pages 266-292, 1993
On the Classical Decision Problem
Originally in
Bulletin of the EATCS 42 October 1990 140-150
Reprinted in
"Current Trends in Theoretical Computer Science:
Essays and Tutorials"
(eds. G. Rozenberg and A. Salomaa)
World Scientific, pages 254-265, 1993
On Finite Model Theory
in "Feasible Mathematics"
Ed. Samuel R. Buss and Philip J. Scott,
Birkhäuser, Boston, 1990, 211-219.
Algebraic Operational Semantics and Occam
CSL'89, 3rd Workshop on Computer Science Logic
Springer Lecture Notes in Computer Science 440 (1990) 176-192.
Later note: the first example of a distributed abstract state machine.
Matrix Decomposition Problem is Complete for the Average Case
FOCS'90, 31st Annual Symposium on Foundations of Computer Science
IEEE Computer Society Press, 1990, 802-811.
Nondeterministic linear-time tasks may require substantially nonlinear deterministic time in the case of sublinear work space
JACM 37:3 (1990), 674-687.
Games people play
in "Collected Works of J. Richard Büchi"
ed. Saunders Mac Lane and Dirk Siefkes
Springer-Verlag, 1990, 517-524.
The Challenger-Solver game: Variations on the Theme of P=?NP
Originally in
Bulletin of the EATCS 39 October 1989 112-121
Reprinted in
"Current Trends in Theoretical Computer Science:
Essays and Tutorials"
(eds. G. Rozenberg and A. Salomaa)
World Scientific, pages 245-253, 1993
Infinite Games
Originally in
Bulletin of the EATCS 38 June 1989 93-100
Reprinted in
"Current Trends in Theoretical Computer Science:
Essays and Tutorials"
(eds. G. Rozenberg and A. Salomaa)
World Scientific, pages 235-244, 1993
Datalog vs First-Order Logic
Journal of Computer and System Sciences
Vol 49, no 3, Dec 1994, 562-588
(Extended abstract in FOCS'89, 142-147.)
In the infinite case, that is if structures may be infinite, the main result is a simple consequence of the compactness theorem. The finite case much harder. It turned out, as Bruno Courcelle pointed out to us, that we reinvented the notion of finite width to establish the main result.
Nearly linear time
Symposium on Logical Foundations of Computer Science
in Pereslavl-Zalessky, USSR
Springer Lecture Notes in Computer Science 363 (1989) 108-118
On Matiyasevich's non-traditional approach to search problems
Information Processing Letters 32 (1989), 41-45.
Time polynomial in input or output
J. Symbolic Logic 54:3 (1989), 1083-1088.
On the strength of the interpretation method
The Journal of Symbolic Logic 54:2 (1989), 305-323.
On Kolmogorov machines and related issues
Originally published in
Bulletin of the EATCS 35 June 1988 71-82
Reprinted in
"Current Trends in Theoretical Computer Science:
Essays and Tutorials"
(eds. G. Rozenberg and A. Salomaa)
World Scientific, pages 225-234, 1993
Algebraic operational semantics and Modula-2
CSL'87, 1st Workshop on Computer Science Logic
Springer Lecture Notes in Computer Science 329 (1988) 81-101
Average case completeness
Journal of Computer and System Sciences 42:3 346-398 1991
(a special issue with selected papers of FOCS'87)
Algorithms in the world of bounded resources
In "The universal Turing machine - a half-century story"
(ed. R. Herken), Oxford University Press, 1988, 407-416.
Logic and the Challenge of Computer Science
in E.Boerger (ed)
"Current Trends in Theoretical Computer Science" 1-57
Computer Science Press, pages 1-57, 1988
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. The first part is based on lectures given at the 1984 Udine Summer School on Computation Theory and summarized in the technical report "Logic and the Challenge of Computer Science", CRL-TR-10-85, Sep. 1985, Computing Research Lab, University of Michigan, Ann Arbor, Michigan.
The second part is an early discussion of a new computation model, later called evolving algebras and 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 technical report mentioned above contained an earlier version of part 2. The final version was written in 1986.
Existential fixed-point logic
In "Logic and complexity" (ed. E. Boerger)
Springer Lecture Notes in Computer Science 270 (1987) 20-36
Monotone versus positive
Journal of ACM 34 1004-1015 1987
Expected computation time for Hamiltonian Path Problem
SIAM Journal on Computing 16:3 (1987) 486-502
Fixed-point extensions of first-order logic
Annals of Pure and Applied Logic 32 (1986), 265-280
What does O(n) mean?
SIGACT NEWS 17 (1986), Number 4, 61-63
On the number of active nodes in a multicomputer system
Networks 16 (1986), 275- 282
Definability by constant-depth polynomial-size circuits
Information and Control 70 (1986), 216-240
Henkin quantifiers and complete problems
Annals of Pure and Applied Logic 32 (1986), 1-16
A zero-one law for logic with a fixed-point operator
Information and Control 67 (1985), 70-90
Monadic second-order theories
Chapter in book
"Model-Theoretical Logics"
eds. Jon Barwise and Sol Feferman
Springer-Verlag, Perspective in Mathematical Logic, 1985, 479-506
We illustrate two powerful decidability
techniques here. One makes use of automata and games. The other is an
offshot of a composition theory where one composes models as well as their
theories. Monadic second-order logic appears to be the most natural match
for the composition theory.
Undecidability proofs must be thought
out anew in this area; for, whereas true first-order arithmetic is
reducible to the monadic theory of the real line R, it is nevertheless not
interpretable in the monadic theory of R. A quite unusual undecidability
method is another subject of this chapter.
In the last section we briefly review
the history of the methods thus far developed and mention numerous
results obtained by the methods.
The decision problem for branching time logic
The Journal of Symbolic Logic , 50 (1985), 668-681
To the decision problem for branching time logic
In "Foundations of Logic and Linguistics:
Problems and their Solutions"
(ed. P. Weingartner and G. Dold), Plenum, 1985, 181-198
The decision problem for linear temporal logic
Notre Dame Journal of Symbolic Logic 26 115-128 1985
Toward logic tailored for computational complexity
In "Computation and Proof Theory" (Ed. M. Richter et al.)
Springer Lecture Notes in Mathematics 1104 175-216 1984
A logic for constant depth circuits
Information and Control 61 (1984), 65-74
A decidable subclass of the minimal Goedel case with identity
The Journal of Symbolic Logic 49 (1984), 1253-1261
The monadic theory and the `next world'
Israel Journal of Mathematics 49 (1984), 55-68
Equivalence relations, invariants, and normal forms, II
Springer Lecture Notes in Computer Science 171 (1984), 24-42
Equivalence relations, invariants, and normal forms
SIAM Journal on Computing 13 (1984), 682-689
Solving NP-hard problems on graphs that are almost trees,
and an application to facility location problems
Journal of ACM 31:3 (1984), 459-473
The word problem for cancellation semigroups with zero
The Journal of Symbolic Logic 49 (1984), 184-191
(1)
if xy = xz or yx = zx then y = z.
No semigroups with zero satisfies (1). The cancellation property for semigroups with zero and identity is
(2)
if xy = xz \neq 0 or yx = zx \neq 0 then y = z.
The cancellation property for semigroups with zero bur without identity is the conjunction of (2) and
(3)
if xy = x or yx = x then x = 0.
Whether or not a semigroup with zero has an identity, we refer to it as a cancellation semigroup with zero if it satisfies the appropriate cancellation property. It is shown in 8, that the word problem for finite semigroups is undecidable. Here we show that the word problem is undecidable for finite cancellation semigroups with zero; this holds for semigroups with identity and also for semigroups wihtout identity. (In fact, we prove a stronger effective inseparabilit result.) This provides the necessary mathematical foundation for 41).
The theory of ordered abelian groups
does not have the independence property
Transactions of American Mathematical Society 284 (1984), 171-182
Algebras of feasible functions
24th Annual Symposium on Foundations of Computer Science
IEEE Computer Society Press, 1983, 210-214
(i) a function is primitive recursive if and only if it is logspace computable, and
(ii)a function is general recursive if and only if it is polynomial time computable.
Critiquing a critique of Hoare's programming logics
Communications of ACM, May 1983, p. 385 (Tech. communication)
The word problem for lattice-ordered groups
Transactions of American Mathematical Society 280 (1983), 127-138
Random models and the Goedel case of the decision problem
The Journal of Symbolic Logic 48 (1983), 1120-1124
Rabin's Uniformization Problem
The Journal of Symbolic Logic 48 (1983), 1105-1119
Interpreting second-order logic in the monadic theory of order
The Journal of Symbolic Logic 48 (1983), 816-828
The monadic theory of ω2
The Journal of Symbolic Logic 48 (1983), 387-398
Decision problem for separated distributive lattices
The Journal of Symbolic Logic 48 (1983), 193-196
E. M. Can message buffers be characterized in linear temporal logic?
Symposium on Principles of Distributed Computing, ACM, 1982, 148-156
On the unique satisfiability problem
Information and Control 55 (1982), 80-88
The inference problem for template dependencies
Information and Control 55 (1982), 69-79
Automata, trees, and games
14th Annual Symposium on Theory of Computing, ACM, 1982, 60-65
A review of two books on the decision problem
Bulletin of the American Mathematical Society 7 (1982), 273-277
Homogeneous optimal fleet
Transportation Research 16B (1982), 459-470
Monadic theory of order and topology in ZFC
Annals of Mathematical Logic 23 (1982), 179-198
Existential interpretation, II
Archiv für Math. Logik und Grundlagenforschung 22 (1982), 103-120
Prefix classes of Krom formulas with identity
Archiv für Math. Logik und Grundlagenforschung
volume 22 (1982), 43-49
Crumbly spaces
Sixth International Congress for
Logic, Methodology and Philosophy of Science (1979)
North-Holland, 1982, 179-191
Elementary theory of automorphism groups of doubly homogeneous chains
Springer Lecture Notes in Mathematics 859 (1981), 67-82
Rigid homogeneous chains
Math. Proceedings of Cambridge Phil. Society 89 (1981), 7-17
Recognizing the real line
Transactions of American Mathematical Society 265 (1981), 527-534
Two notes on formalized topology
Fundamenta Mathematicae 57 (1980), 145-148
Modest theory of short chains, II
The Journal of Symbolic Logic 44 (1979), 491-502
Modest theory of short chains, I
The Journal of Symbolic Logic 44 (1979), 481-490
Monadic theory of order and topology, II
Israel Journal of Mathematics 34 (1979), 45-71
Monadic theory of order and topology, I
Israel Journal of Mathematics 27 (1977), 299-319
Expanded theory of ordered abelian groups
Annals of Mathematical Logic 12 (1977), 193-228.
Intuitionistic logic with strong negation
Studia Logica 36 (1977), 49-59
Constructing an optimal fleet for a transportation schedule
Transportation Science 11 (1977), 20-36
Semi-conservative reduction
Archiv für Math. Logik und Grundlagenforschung 18 (1976), 23-25
(a) if A is satisfiable then so is f(A),
(b) if A is finitely satisfiable then so is f(A),
(c) if f(A) is satisfiable then so is A,
(d) if f(A) is finitely satisfiable then so is A.
K is conservative if there is a conservative reduction of the class of all formulas to K.
f is a semi-conservative reduction of K to L if conditions (b) and (c) hold.
Theorem: If a conservative K semi-conservatively reduces to L then L is conservative too.
The decision problem for standard classes
The Journal of Symbolic Logic 41 (1976), 460-464
The decision problem for first-order logic
Manuscript, 1971, 124 pages (Russian)
The decision problem for the expanded theory of ordered abelian groups
Formulas with one universal quantifier
Pages 97-110 in book
"Selected Questions of Algebra and Logic"
dedicated to the memory of A.I.\ Malcev
Publishing house ``Nauka" --- Siberian Branch
Novosibirsk, 1973 (Russian)
Strengthening a result of Suranyi
Bulletin of the Georgian Academy of Sciences
Volume 70, Number 2 (1973), 289-292 (Russian)
A remark on Berger's paper on the domino problem
Siberian Mathematical Journal 13 (1972), 319-321
(English translation of 16)
A remark on Berger's paper on the domino problem
Siberian Mathematical Journal, 13 (1972), 459-463 (Russian)
(1) those that can tile the plane periodically (equivalently, can tile a torus), and
(2) those that cannot tile the plane at all.
It follows that the collection of domino sets that can cover a torus is undecidable.
Minsky machines and the AEA&E* case of the decision problem
Trans. of Ural State University 7:3 (1970), 77-83 (Russian)
The decision problem for decision problems
Algebra and Logic 8 (1969), 362-363
(English translation of 14)
The decision problem for decision problems
Algebra and Logic 8 (1969), 640-642 (Russian)
The decision problem for logic of predicates and operations
Algebra and Logic 8 (1969), 160-174
(English translation of 13)
The decision problem for logic of predicates and operations
Algebra and Logic 8 (1969), 284-308 (Russian)
The decision problem for some algebraic theories
Doctor of Physico-Mathematical Sciences Thesis
Ural State University, Sverdlovsk, USSR, 1968 (Russian)
Chapter 8 (English)
is an English translation of Chapter~8 of the thesis, and
Some algorithmic questions of algebraic theories is an abstract in Russian of an earlier talk on related topics.
A new decision procedure for the theory of ordered abelian groups
Algebra and Logic 6:5 (1967), 5-6 (Russian)
which is by itself a precursor of 25
Lattice-ordered abelian groups and K-lineals
Soviet Mathematics 8 (1967), 987-989
Lattice-ordered abelian groups and K-lineals
Doklady 175 (1967), 1213-1215 (Russian)
Hereditary undecidability of the theory of
lattice-ordered abelian groups
Algebra and Logic 6:1 (1967), 45-62 (Russian)
The word problem for some classes of semigroups
Algebra and Logic 5:2 (1966), 25-35 (Russian)
K1 is the class of word pairs (u0,v0) such that E implies u0=v0 in every periodic semigroup.
K2 is the class of word pairs (u0,v0) such that E fails to imply u0=v0 in some finite semigroup.
The paper contains some additional undecidability results.
Recognizing satisfiability of predicate formulas
Algebra and Logic 5:2 (1966), 25-35 (Russian)
The decision problem for predicate logic
Soviet Mathematics 7 (1966), 669-670
The decision problem for predicate logic
Doklady 168 (1966), 510-511 (Russian)
On the decision problem for pure predicate logic
Soviet Mathematics 7 (1966), 217-219
On the decision problem for pure predicate logic
Doklady 166 (1966), 1032-1034 (Russian)
Existential interpretation
Algebra and Logic 4:4 (1965), 71-85 (Russian)
Elementary properties of ordered abelian groups
AMS Translations 46 (1965), 165-192
Elementary properties of ordered abelian groups
Algebra and Logic 3:1 (1964), 5-39 (Russian, Ph.D. Thesis)
Universal equivalence of ordered abelian groups
Algebra and Logic 2:1 (1963), 37-39 (Russian)
Groups covered by proper characteristic subgroups
Trans. of Ural University 4:1 (1963), 32-39 (Russian, Master Thesis)
Specification and Testing at Microsoft
Executive summary
• Produce designs that are themselves testable.
• Test and enforce the design by means of AsmL-based tools.
Rich Sequential-Time ASMs
In "Formal Methods and Tools for Computer Science"
(Proceedings of Eurocast 2001)
eds. R. Moreno-Diaz and A. Quesada-Arencibia,
Universidad de Las Palmas de Gran Canaria
Canary Islands, Spain, February 2001, 291-293
Table ASMs
in "Formal Methods and Tools for Computer Science"
(Proceedings of Eurocast 2001)
eds. R. Moreno-Diaz and A. Quesada-Arencibia,
Universidad de Las Palmas de Gran Canaria
Canary Islands, Spain, February 2001, 286-290
Formal methods have been shown to be helpful in strengthening the meaning of specifications but despite their power, few development teams have successfully incorporated them into their software processes. This experience indicates that producing a usable formal method is also hard.
This paper is the story of how a particular theoretical result, namely the normal forms of Abstract State Machines, motivated a genuinely usable form of specification that we call ASM Tables.
We offer it for two reasons. The first is that the result is interesting in and of itself and --- it is to be hoped --- useful to the reader. The second is that our result serves as a case study of a more general principle, namely, that in bringing rigorous methods into everyday practice, one should not follow the example of Procrustes: we find that it is indeed better to adapt the bed to the person than the other way round.
We also offer a demonstration that an extremely restricted syntactical form can still contain sufficient expressive power to describe all sequential machines.
A New Thesis
Abstracts, American Mathematical Society
Vol. 6, no. 4 (August 1985), page 317, abstract 85T-68-203.
Reconsidering Turing's thesis (toward more realistic semantics of programs)
Technical report CRL-TR-36-84
University of Michigan, September 1984