Verification of Non-Terminating Action Programs (VERITAS)

点击翻译按钮获取中文摘要

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.