Logic and Dynamic Computation

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

Descriptive Complexity measures the richness of a language or sentence needed to describe a given property. The languages are variants of first-order logic and their targets are finite, ordered structures. There is a profound relationship between the traditional computational complexity of a problem and the descriptive complexity of the problem; indeed, all major complexity classes have been shown to have natural descriptive characterizations. Thus complexity can be understood entirely from a logical point of view. Important new understandings about complexity have arisen from the descriptive point of view. In particular, new insights about dynamic complexity and the first complete problems for dynamic complexity classes have grown out of the approach. Insights from descriptive complexity have recently led to progress on the Three-Valued-Logic Analysis Engine (TVLA), a tool that automatically deduces properties of real programs and program modules using three-valued logic. TVLA was originally the brain child of Sagiv, Reps, and Wilhelm, among others. It successfully handles the very difficult case of programs that use dynamic data structures, including allocation and deallocation of memory cells. TVLA uses three-valued logical structures to summarize a potentially infinite set of real data structures. In doing so, it is sometimes necessary to use the truth value of "1 2" meaning "unknown". A key technical challenge for TVLA is to use the value 1 2 as little as possible, so that the summaries are as precise as possible. The proposed research has several thrusts, the first two involve TVLA and the remaining three concern other directions in descriptive complexity: (1) Extend previous work to maintain TVLA abstractions that are as precise as possible. Part of this proposed work makes use of results from dynamic complexity. (2) Employ dual-vocabulary, three-valued TVLA structures to automatically summarize the effects of recursive procedures. Algorithms to do this precisely and to compose these descriptions efficiently will be used to scale up the applications of TVLA to larger programs whose procedures can call each other recursively. (3) Add group theory to logic. The resulting family of logical languages will likely characterize all graphs in the classes known to have polynomial-time isomorphism algorithms. This will improve our understanding of this important algorithmic problem and also shed light on a question in descriptive complexity concerning the capturing of all polynomial-time order-independent properties. (4) Extend and develop further characterizations of the relationships between dynamic complexity classes. (5) Use the recently developed game for proving lower bounds on the size of formulas to learn more about a fundamental trade-off in descriptive complexity: formula size versus number of variables. The broader impact of the above work is four fold: (1) The work related to TVLA will have direct, practical use in building tools that can automatically reason about real programs, thus improving software maintenance and reliability, a huge national and international need. (2) All the work will improve our understanding of the fundamental nature of computation. (3) Results from this work will be widely distributed. They will be presented at conferences, published in journals, and taught in seminars. (4) Graduate students will be trained to do research in this combination of very pure theory and quite applied theory.