Project Details
Projekt
Verification of Non-Terminating Action Programs (VERITAS)
Subject Area
Theoretical Computer Science
Term
from 2012 to 2021
Project identifier
Deutsche Forschungsgemeinschaft (DFG) - Project number 167839951
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.
DFG Programme
Research Units
