Computational Aspects of Reasoning about Dynamic Systems

搜索问题是实际问题的重要组成部分，特别是人工智能问题，如反应代理的调度、诊断、规划和合成。在许多应用程序中，会出现一些随时间变化的显式数据。例如，在医疗领域和业务流程建模中，这种设置很普遍。数据通常很大，而且会随着时间的推移而变化，而且这些问题在计算上很困难。问题的表示必须是这样的，即可以有效地执行关于数据大小的推理算法。在某些应用中，算法的复杂性还可能取决于公式的大小。一个耐人寻味的问题是，在规范语言的什么条件下，这个问题肯定有一个有效的算法。如果了解了这些条件，就可以开发出具有复杂性保证的规范语言。我计划发展理论基础，了解有效计算的条件的一般原理。这一基础性研究将有助于我们开发实用的算法。这些算法将从用户编写的高级规范开始自动解决问题，从而帮助完成这些具有智力挑战的任务。我的研究是关于如何弥合用户和先进技术之间的差距，这符合用令人兴奋的人工智能应用程序取代人工服务的总体趋势。这项研究使非专业用户能够解决很大比例的此类问题，从而降低了社会的总成本，并取得了显着的社会经济效益。

An important part of practical problems, and AI problems in particular, e.g. scheduling, diagnosis, planning and synthesis of reactive agents, are search problems. In many applications, some explicit data, that changes over time, is present. This setting is prevalent, e.g., in medical domains and in business process modelling. The data is, typically, large, and changes over time, and the problems are computationally hard. The representation of the problem must be such that reasoning algorithms could be executed efficiently with respect to the size of the data. In some applications, complexity of the algorithms may also depend on the size of the formula. An intriguing question is under what conditions on the specification language the problem definitely has an efficient algorithm. If the conditions are understood, then a specification language with a complexity guarantee can be developed. I plan to develop theoretical foundations and understand general principles, of the conditions for efficient computations. This foundational research will help us to develop practical algorithms. The algorithms will automate problem solving starting from a high-level specification written by the user, thus assisting in these intellectually challenging tasks. My research is about how to bridge the gap between user and advanced technology, and it is within the overall trend of replacing human services with exciting AI applications. The research leads towards making solving a large proportion of such problems accessible to a non-specialist user thus reducing the overall cost to the society and achieving a significant socio-economic benefit.