Decidable Verification of Golog Programs | (Statusvortrag)

Date

Nov 16, 2015

Time

2:00 PM - 3:00 PM

Speaker

Benjamin Zarrieß

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 talk, we consider the problem of achieving decidability of verification in fragments of Golog based on Description Logics (DLs). Recently, DL-based action languages have been introduced as fragments of the Situation Calculus where reasoning about the consequences of actions can be reduced to decidable standard DL reasoning tasks. An overview of how to use DL-actions in Golog programs and how to specify properties of such programs using temporal DLs is presented. Furthermore, an outlook on the results obtained so far is given and the general method for proving decidability of verification is briefly introduced. Betreuer: Prof. Dr.-Ing. Franz Baader Fachreferent: Prof. Steffen Hölldobler

Last modified: Nov 16, 2015, 8:59:00 AM