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.