Verification of Golog Programs over Description Logic Actions

Date

Nov 2, 2017

Time

9:15 AM - 10:15 AM

Speaker

Dipl.-Inf. Benjamin Zarrieß

Affiliation

Institut für Theoretische Informatik, Automatentheorie

Language

en

Main Topic

Informatik

Other Topics

Informatik

Description

Golog is a powerful programming language for logic-based agents. The primitives of the language are actions whose preconditions and effects are defined in a Situation Calculus action theory using first-order logic. To describe possible courses of actions the programmer can freely combine imperative control structures with constructs for non-deterministic choice, leaving it to the system to resolve the non-determinism in a suitable manner. Golog has been successfully used for high-level decision making in the area of cognitive robotics. Obviously, it is important to verify certain properties of a Golog program before executing it on a physical robot. However, due to the high expressiveness of the language the verification problem is in general undecidable. In this thesis, we study the verification problem for Golog programs over actions defined in action languages based on Description Logics and explore the boundary between decidable and undecidable fragments.

Last modified: Nov 2, 2017, 8:49:05 AM