The action language GOLOG has been used, among other things, for the specification of the behaviour of mobile robots. Since the task of such autonomous systems is typically open-ended, their GOLOG programs are usually non-terminating. To ensure that the program will let the robot exhibit the intended behaviour, it is often desirable to be able to formally specify and then verify the desired properties, which are often of a temporal nature. This task has been studied within our preliminary work from two perspectives: On the one hand, the problem was tackled for very expressive specification and action program formalisms, but without the goal of achieving decidability, i.e. the developed verification methods were not guaranteed to terminate. On the other hand, the verification problem was studied for action formalisms based on decidable description logics and very limited means of specifying admissible sequences of actions, which allowed us to show decidability and complexity results for the verification problem. The purpose of this project is to combine the advantages of both approaches by, on one hand, developing verification methods for GOLOG programs that are effective and practically feasible and, on the other hand, going beyond the formalisms with very limited expressiveness to enhance their usefulness. Among other things, both qualitative and quantitative temporal program properties will be addressed.
Submitted by Jens Claßen on 1. February 2013 - 18:00 categories [ ]
Humanity has crossed the line from being a rural to urban species since 2007. For the first time in history, more people live in cities and urban areas than in the countryside. Starting in the developed ations, where the urbanisation process has been significantly decelerated in the meantime, urbanisation has especially increased in Asia and South America as well as in Africa to a substantial extent in the second half of the last century. Processes of urbanisation have a negative influence on the availability and quality of water resources. Especially in developing and emerging countries, the hydrological and hydrogeological setting of each region is deteriorated through the growing urbanization processes. Often the hydrological and hydrogeological basis of an area is strongly affected by rocesses of urbanisation in these countries. Changes of the structure of urban development going along with the urbanisation will not be without consequences for the environment and water resources.
In frame of this background the Department of Engineering Geology and Hydrogeology of the RWTH Aachen University analysis the interaction between high speed urbanisation/mega-urbanisation and water resources in China and India. In context to this we want to develop a knowledge-based planning and simulation framework.
Submitted by Martin Liebenberg on 12. January 2015 - 17:33 categories [ ]
Submitted by Jens Claßen on 12. January 2015 - 10:57 categories [ ]
The goal of this thesis is to integrate Answer Set Programming (ASP) into a Golog system in order to obtain an agent framework that is capable of efficient non-monotonic reasoning with introspection.
Submitted by Jens Claßen on 16. December 2014 - 18:00 categories [ ]
In this seminar we will study several modeling and reasoning techniques for knowledge and belief in dynamic systems. Knowledge is an important aspect of intelligent programs: while most of today's systems assume a closed world, i.e., everything they don't know to be true is assumed to be false, an intelligent system needs to consider possible that there are truths not known to the system. In a dynamic environment, i.e., an environment where one or multiple agents (inter)act, the system will usually have to acquire new knowledge through sensing. Potentially it may even revise its beliefs when it realizes some beliefs were wrong. In this seminar we will study various aspects of action, knowledge, and belief.
We plan to implement a peer review process for this seminar. That is, every student will read some other students' term paper and provide feedback in form of a written review. This shall not only deepen your understanding of the other topics, but it also introduces you to the academic review process.
Submitted by Christoph Schwering on 5. January 2014 - 23:08 categories [ ]
Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of non-terminating Golog programs, based on the first-order modal Situation Calculus variant ES, and regression-based reasoning. However, while Golog’s high expressiveness is a desirable feature, it also means that their verification procedures cannot be guaranteed to terminate in general. In this thesis, we address this problem by showing that, for a relevant subset, the verification of non-terminating Golog programs is indeed decidable, which is achieved by means of three restrictions. First, we use the ES variant of a decidable two-variable fragment of the Situation Calculus that was introduced by Gu and Soutchanski. Second, we have to restrict the Golog program to contain ground action only. Finally, we consider special classes of successor state axioms, namely the context-free ones and those that only admit local effects.
Submitted by Martin Liebenberg on 13. April 2013 - 18:45 categories [ ]
Submitted by Jens Claßen on 1. February 2013 - 15:05 categories [ ]
Submitted by Daniel Beck on 3. April 2012 - 10:29 categories [ ]
In this seminar we will study several aspects of robust and reliable robotics. Robots are machines created to fulfill particular tasks instead of or in cooperation with humans. In virtually all scenarios a failure is annoying or even catastrophic. Planetary rovers cannot be repaired easily or at all, broken factory robots can become vastly expensive not only due to the cost to repair the robot itself, but the problems they cause for the overall supply chain; and domestic service robots operate in close proximity to humans in their habitats and must take special precautions as not to harm a human or damage the interior. These considerations make it necessary to develop techniques and systems that enable a robot system to detect failures or unexpected behavior and at least stop, better even work around the problem.
The topics include recent papers on execution monitoring, robot system debugging, and fault detection.
Submitted by tim on 9. January 2012 - 12:10 categories [ ]
Only students that do not need to enroll at the ZPA for the exam need to register here. For instance, these are diploma students or students who are currently pursuing their Bachelor degree but intend to use the exam for their Master's studies.
The registratration will be open until September 21.
Fields marked with an asterisk are mandatory.
Submitted by Daniel Beck on 13. September 2011 - 9:10 categories [ ]