Verification of Non-Terminating Action Programs (VERITAS)

动作语言GOLOG主要用于规范代理（包括移动机器人）的高级行为。由于此类自治系统的任务通常是开放式的，因此它们的GOLOG程序通常是非终止的。为了确保程序执行导致预期的行为，通常需要正式指定，然后自动验证所需的属性，这些属性通常是临时性质的。承认完全一阶表达的GOLOG验证的一般问题是不确定的。在这个项目的第一阶段，我们已经确定了一些有趣的片段，这些片段可以进行可确定的验证，但尽可能多地保留了GOLOG的表现力。在第二阶段，我们计划将我们的验证方法的适用性推进到更现实的场景，特别关注机器人应用。特别是，我们将超越单纯的可决定性，研究验证的可行性，结合连续变化的概念以及概率不确定性，并考虑环境动力学模型也存在的情况。

The action language GOLOG is primarily intended for the specification of the high-level behaviour of agents, including mobile robots. Since the task of such autonomous systems is typically open-ended, their GOLOG programs are often non-terminating. To ensure that program execution leads to intended behaviour, it is often desirable to formally specify and then automatically verify the desired properties, which are often of a temporal nature. The general problem of the verification of GOLOG, which admits full first-order expressiveness, is undecidable. In the first phase of this project we have identified a number of interesting fragments that admit decidable verification, yet retain as much of GOLOG¿s expressiveness as possible. In the second phase, we plan to advance the applicability of our verification methods towards more realistic scenarios, with a special focus on robotics applications. In particular, we will go beyond mere decidability and study the feasibility of verification, incorporate notions of continuous change as well as probabilistic uncertainty, and consider the case where models of the dynamics of the environment exist as well.