Applications of Algorithmic Techniques

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