Applications of Algorithmic Techniques

本研究将涉及算法设计和实现中的许多不同主题。研究的共同主题是将先进的算法技术应用于实际问题。四个具体的问题领域正在调查中：(1)n体模拟：这是一个与华盛顿大学天文学部门合作的项目，研究n体模拟。基本目标是改进用于大规模模拟的算法和数据结构。模拟的规模提出了许多有趣的计算几何问题。(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.