Freiburg; and Torsten Schaub, University of Potsdam.
To increase the practical impact of the Research
Unit, robotics, bioinformatics (phase I), and logistics
(phase II) were included as application areas. In
robotics, the quantitative aspects of reasoning
include dealing with noisy sensors and continuous
robot arm trajectories. In bioinformatics, they
include learning formal ontologies from text databases and modeling protein interaction networks.
The applications in logistics are developed in cooperation with Fraunhofer IML in Dortmund, one of Germany’s leading research institutes in logistics.
The Research Unit currently consists of four projects, each involving researchers from at least two universities. This way, there’s a diversity of competencies
and background, which benefits the projects. We
briefly describe each of the projects below. Fig. 1 illustrates the thematic connections among the projects.
Verification of Nonterminating
GOLOG is a high-level language for the specification
of the behavior of agents, including mobile robots.
The language is based on an underlying action theory expressed in the situation calculus.
Modern variants of GOLOG allow, among other
things, for programs with stochastic actions and
noisy sensors. The programs are typically nonterminating, that is, they describe what the robot should
In many situations, it is essential to guarantee that
“nothing goes wrong.” In other words, one has to
ensure that the execution of the program leads to
intended behavior. One way to achieve this alignment is to formally specify and then automatically
verify the desired (temporal) properties. This project
investigates this kind of verification of GOLOG robot
Unfortunately, GOLOG verification in general is
undecidable due to the formalism’s high expressiveness in terms of first-order quantification and program constructs. We therefore looked at and identified a number of interesting fragments that admit
decidable verification, yet retain as much of GOLOG’s
expressiveness as possible.
In our studies, verification was tackled from two
directions: on the one hand, by means of nontrivial
Verification of Robot
Planning in Dynamic
Figure 1. Hybris Overview.