Applications of Algorithmic Techniques

这项研究将解决一些不同的主题在算法的设计和实现。 研究的共同主题是将先进的算法技术应用于实际问题。 四个具体的问题领域正在调查中：（1）N体模拟：这是一个合作项目，与天文学研究N体模拟的UW部门。 基本目标是改进用于大规模模拟的算法和数据结构。模拟的规模提出了不少有趣的计算几何问题。 (2)约束满足：开发图形用户界面的一种方法是使用约束系统来指定界面的行为。 将开发算法来解决在这一领域出现的约束系统的类型。 将特别强调约束层次结构和解决方案的效率。(3)旅游问题：这个问题是在最短的时间内访问一组城市，旅行被限制在一个周期性的时间表。换句话说，这是限制在公共交通的旅行推销员问题。 这个问题的启发式和精确的算法将被开发和实施。(4)模型检查软件规范：一种来自硬件验证的技术将应用于软件工程中的一个主要问题。 在过去的几年里，符号模型检测已经成为硬件验证的一个非常重要的工具。 这个项目是调查是否模型检查也可以成功地应用于评估软件规格。 TCAS是一种用于商用飞机的防撞系统，其规范将是该项目的主要案例研究。

This research will address a number of different topics in the design and implementation of algorithms. The common theme of the research is application of advanced algorithmic techniques techniques to practical problems. Four specific problem areas are under investigation: (1) N-body Simulation: This is a collaborative project with the UW Department of Astronomy studying N-body simulation. The basic objective is to improve the algorithms and data structures used for massive simulations. The scale of simulations raise quite a few interesting computational geometry problems. (2) Constraint Satisfaction: One method of developing graphical user interfaces is to use a system of constraints to specify the behavior of the interface. Algorithms will be developed to solve the types of constraint systems which arise in this domain. There will be particular emphasis on constraint hierarchies, and on the efficiency of solutions. (3) The Traveling Tourist Problem: The problem is to visit a set of cities in minimum time where travel is restricted to a periodic timetable. In other words, it is the traveling salesman Problem restricted to public transportation. Heuristic and exact algorithms for this problem will be developed and implemented. (4) Model Checking Software Specification: A technique from hardware verification will be applied to a major problem in software engineering. In the last several years, symbolic model checking has become a very important tool for hardware verification. This project is to investigate whether model checking can also be applied successfully to evaluate software specifications. The specification of TCAS, a collision avoidance system used in commercial aircraft will be a major case study for the project.