Verification of Golog Programs over Description Logic Actions

Talk by Benjamin Zarrieß

Location: APB 3027
Start: 2. November 2017 at 9:15 am
End: 2. November 2017 at 10:15 am
Research group: Automata Theory
Event series: KBS Seminar
iCal

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.