November – 2002 ^December

Since its introduction in 1977 [Pnu77], the temporal logic approach to the specification and verification of reactive systems has matured into an engineering field, practiced in most of the leading VLSI designs industries such as Intel, IBM, Motorola, Siemens etc'. In this presentation I will first introduce the specification language of linear temporal language and the algorithmic verification method of symbolic model checking, used for the verification of finite-state systems. I then consider the problem of verifying infinite-state systems. These were traditionally verified by theorem provers. However, while algorithmic (automatic) verification methods are already being used in industry, theorem provers are considered impractical for the industrial environment. it is generally recognized that the only way formal verification can ever scale up to handle industrialize designs is by the extensive use of abstraction and modularization, which break the task of verifying a large system into several smaller tasks of verifying simpler systems. An interesting example is the problem of uniform verification of reactive parameterized systems: Given a reactive parameterized system $S(n): P[1] || ....|| P[n]$ and a temporal property $p$, verify that $S(n)$ satisfies p for every $n>1$. I present the method of network invariant that can be used to verify a wide spectrum of LTL properties, including liveness, using the industrial automatic tools of symbolic model checking.

The effectiveness of the network invariant method is illustrated on several examples, including a deterministic and probabilistic versions of the dining philosophers problem.

The consideration of combinatorial objects from a geometric perspective has been a very powerful idea in discrete mathematics in recent years. One of the most successful realizations of this general concept concerns the (shortest path or geodetic) metric on the vertex set of a graph. A good deal of information can be inferred by approximating a given graph metric within some known (usually infinite) metric spaces. Much of this carries over from graph metrics to the general context of finite metric spaces. The most thoroughly studied parameter is the distortion of a map from one metric space to another . It is defined as distortion

A fundamental question that we consider is: Given a finite metric space and a class of "nice" metric spaces, find a metric and a map so that distortion is minimized. Among the classes of interest here are the (metrics of) normed spaces, especially spaces; The graph metrics of trees or other restricted classes of graphs, such as planar graphs. To give the reader some idea on the progress in this field, we mention some results on embeddings into , currently the most developed part of the theory. Every -point metric space can be embedded in with distortion . The bound is tight for (the metric of) constant-degree expander graphs. The metric of every -vertex tree embeds in with distortion . This bound is attained for the complete binary tree. The metric of an -vertex planar graph embeds in with distortion , and the bound is tight. There is a polynomial time algorithm that finds, for a given metric space, an embedding into of least possible distortion. Let be a -regular () graph of girth (smallest cycle length) . Then every embedding of into has distortion . This is not known to be tight, and the truth may be . Every -point set in can be mapped to -dimensional space with distortion where . The bound on the dimension is nearly tight. The field is still at its early stages of development and is very rich with fascinating open questions. Here are several illustrations.

Does the metric of every planar graph embed in with distortion for some absolute constant ? Even more daringly: Does a similar statement hold for every minor-closed family of graphs? Can -regular () graphs of arbitrarily high girth be embedded into with bounded distortion? What is the lowest such that every -point set in can be mapped into with distortion ? What is the smallest such that for every -vertex graph there is a distribution on 's spanning trees so that for every two vertices ? (The left expression is the expected distance in a randomly chosen tree and on the right is the distance in ). If in the previous question we allow the 's to be general tree metrics that dominate , this is known to hold with , which is nearly tight. This last statement has many beautiful algorithmic applications. Indeed, among the most pleasing aspects of this field, are the many applications it has found in the theory of algorithms, especially in the context of polynomial-time approximations to NP-hard problems. Among others, applications were found to problems on multi commodity flows, on line computation and graph bandwidth.

Finite metric spaces are not only useful for the theory of algorithms. They are a very powerful tool in the study and analysis of large data-sets, e.g. those coming from computational molecular biology.

Modeling data sets as points in a high dimensional vector space is a trendy theme in modern information retrieval and data mining. Among the numerous drawbacks of this approach is the fact that many of the required processing tasks are computationally hard in high dimension. We survey several algorithmic ideas that have applications to the design and analysis of polynomial time approximation schemes for nearest neighbor search and clustering of high dimensional data. The main lesson from this line of research is that if one is willing to settle for approximate solutions, then high dimensional geometry is easy.