Find out about the people who work in the lab Papers written by our lab members Current research activities in the lab A list of our seminars can be found here Software tools developed by lab members A comprehensive list of links
Dr. Yuri Gurevich - PIMS Distinguised Chair
Office: N/A

Visit the PIMS site dedicated to Dr. Gurevich's visit.

Yuri Gurevich is a senior scientist heading the Foundations of Software Engineering group at Microsoft Research in Redmond, WA. He is Professor Emeritus of Electrical Engineering and Computer Science at the University of Michigan. Originally, he started his career as an algebraist. Later he became a logician. Then he moved to computer science, where his main projects have been Abstract State Machines, Average Case Computational Complexity, and Finite Model Theory. Dr. Gurevich has been honored as a Dr. Honoris Causa of the University of Limburg, Belgium (1998), as a Fellow of the Association for Computing Machinery (1996), as well as a Fellow of the John Simon Guggenheim Memorial Foundation (1995).

Contributions to Algebra and Logic
For the first twenty years of his career Yuri Gurevich worked in algebra and mathematical logic. One of the landmark results he obtained was the decidability of the first-order theory of ordered abelian groups which answered a question posed by the great logician Alfred Tarski. (Interestingly, Tarski announced that he had that decidability result, but then acknowledged that the proof fell through). Another landmark result of Gurevich relates to the Classical Decision Problem: Classify the standard fragments of predicate logic into decidable and undecidable. The problem attracted attention of many famous logicians
including Gödel himself. Gurevich completed the desired classification. Alongside Saharon Shelah, Gurevich made a major contribution into the study of the monadic second-order theory of orders and trees. His work in this early period addressed a wide spectrum of problems, some involving advanced set theory, and showed enormous versatility. In the early eighties he had become one of the world's leading mathematical logicians.

Contributions to Average Case Computational Complexity
In applications, NP problems often come with probability distribution on instances. Typically, it suffices to solve the problem fast on average. It turns out that many NP complete (and thus worst-case intractable) problems do have feasible average-case solutions with respect to natural probability distributions. For example, Gurevich and Shelah constructed an algorithm that solves the Hamiltonian circuit problem in linear time on average with respect to the uniform probability distribution. However, the situation is not always so rosy. Leonid Levin and Yuri Gurevich developed a theory of average-case complexity and provided numerous examples of average-case intractable NP problems with natural probability distributions.

Contributions to Finite Model Theory
Yuri Gurevich is one of the founders of and major contributors to finite model theory. He discovered that numerous classical model-theoretic results fail in the finite case. He showed that, over finite models, primitive recursive functions are exactly those logspace computable, and that recursive (a la Herbrand-Gödel-Kleene) functions are exactly those polynomial time computable. Gurevich and Shelah showed that, over finite models, first-order logic with the least fixed-point operator is exactly as expressible as first-order logic with the inflationary fixed-point operator. Ajtai and Gurevich showed that, as far as expressivity over finite models is concerned, first-order logic and datalog have trivial intersection. In 1988, Gurevich published a conjecture that, in the case of arbitrary finite models (as opposite to ordered finite models), there is no logic that captures polynomial time. These are only some of the important results of Gurevich in the area.

Contributions to the Theory of Abstract State Machines
Dr. Gurevich's fundamental work on the theory of Abstract State Machines (ASMs), originally called evolving algebras, is of fundamental importance for theoretical and applied computing science. He formulated the ASM thesis according to which ASMs provide a universal model of computation in a stronger sense than Turing Machines. ASMs step-for-step simulate arbitrary algorithms on their natural levels of abstraction. The ASM thesis applies to sequential, parallel and distributed algorithms. Recently Gurevich was able to prove the version of the thesis for sequential algorithms. After that, Andreas Blass and Yuri Gurevich proved the version of the thesis for parallel algorithms.

The significance of the theoretical concepts developed by Gurevich is confirmed by the substantial impact they have on mathematical modeling of discrete dynamic systems. Indeed, the definition of ASMs have triggered hundreds of research papers in applied computer science. This success is well documented in the annotated ASM bibliography on the ASM web site. There is a well-established international ASM community which holds regular conferences and workshops.

Beyond academic research, ASMs have been used in industry as a practical tool for system modeling by leading companies such as Siemens (Munich), and Microsoft (Redmond). Furthermore, ASMs have been adopted as a basis for international standardization of complex modeling and programming languages. For instance, the International Telecommunication Union (former CCITT) has approved the ASM-based model of their specification and design language SDL as the current standard.

Last updated on April 12, 2003