Research Group on the Foundations of Artificial Intelligence

Complete list of publications

• sorted by year of publication
• sorted by author
• sorted by area

Recent publications (last 12 months):

(Show all abstracts) (Hide all abstracts)

• Marc Gissler, Christian Dornhege, Bernhard Nebel and Matthias Teschner.
  Deformable Proximity Queries and their Application in Mobile Manipulation Planning.
  In Symposium on Visual Computing (ISVC 2009). 2009.
  To appear.
  (Show abstract) (Hide abstract)
  

• Hans-Jörg Peter and Robert Mattmüller.
  Component-based Abstraction Refinement for Timed Controller Synthesis.
  In Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS 2009). 2009.
  To appear.
  (Show abstract) (Hide abstract)
  

  We present a novel technique for synthesizing controllers for distributed real-time environments with safety requirements. Our approach is an abstraction refinement extension to the on-the-fly algorithm by Cassez et al. from 2005. Based on partial compositions of some environment components, each refinement cycle constructs a sound abstraction that can be used to obtain under- and over-approximations of all valid controller implementations. This enables (1) early termination if an implementation does not exist in the over-approximation, or, if one does exist in the under-approximation, and (2) pruning of irrelevant moves in subsequent refinement cycles. In our refinement loop, the precision of the abstractions incrementally increases and converges to all specification-critical components.

  We implemented our approach in a prototype synthesis tool and evaluated it on an industrial benchmark. In comparison with the timed game solver UPPAAL-Tiga, our technique outperforms the nonincremental approach by an order of magnitude.

• Alexander Kleiner and Christian Dornhege.
  Operator-Assistive Mapping in Harsh Environments.
  In Proceedings of the IEEE International Workshop on Safety, Security and Rescue Robotics (SSRR 2009). 2009.
  To appear.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  Teleoperation is a difficult task, particularly when controlling robots from an isolated operator station. In general, the operator has to solve nearly blindly the problems of mission planning, target identification, robot navigation, and robot control at the same time. The goal of the proposed system is to support teleoperated navigation with real-time mapping. We present a novel scan matching technique that re-considers data associations during the search, enabling robust pose estimation even under varying roll and pitch angle of the robot enabling mapping on rough terrain. The approach has been implemented as an embedded system and extensively tested on robot platforms designed for teleoperation in critical situations, such as bomb disposal. Furthermore, the system has been evaluated in a test maze by first responders during the Disaster City event in Texas 2008. Finally, experiments conducted within different environments show that the system yields comparably accurate maps in real-time when compared to higher sophisticated offline methods, such as Rao-Blackwellized SLAM.

• Christian Dornhege, Marc Gissler, Matthias Teschner and Bernhard Nebel.
  Integrating Symbolic and Geometric Planning for Mobile Manipulation.
  In Proceedings of the IEEE International Workshop on Safety, Security and Rescue Robotics (SSRR 2009). 2009.
  To appear.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  Mobile manipulation requires to solve multiple subproblems. One is planning in high-dimensional configuration spaces, that we approach in this work. We decompose the manipulation problem into a symbolic and a geometric part. The symbolic part is implemented as a classical symbolic planner that tightly integrates a geometric planner enabling us to efficiently generate correct plans. A probabilistic roadmap planner constitutes the geometric part. During the computation of the roadmap we utilize proximity queries to determine non-colliding configurations and to verify collision-free paths between configurations accurately and efficiently. We demonstrate experiments in two scenarios, one of these being the manipulator dexterity test scenario that was used in NIST's response robot evaluation in Disaster City.

• Dapeng Zhang, Cai Zhongjie, Chen Kefei and Bernhard Nebel.
  A Game Controller Based on Multiple Sensors.
  In In Proceedings of the Fifth International Conference on Advances in Computer Entertainment Tochnology (ACE 2009). 2009.
  Video.
  (Show abstract) (Hide abstract) (PDF)
  

  A digital game is normally controlled by hand. Playing such a game requires only minimum hand movements. Rather than being easy and comfortable, this game controller is designed to be physically taxing for the players. It consists of several sensors, which makes a game more lively and forces the users to be more physically active. By using different mapping methods, one game can be played in several ways. The statistics gathered from the experiments show that even though the quality of control on the chosen fighting game is not as high as with a normal joystick, the developed controller is still preferred by most of the participants. It induces much more movement than a normal joystick.

• Christian Dornhege, Patrick Eyerich, Thomas Keller, Sebastian Trüg, Michael Brenner and Bernhard Nebel.
  Semantic Attachments for Domain-Independent Planning Systems.
  In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pp. 114-121. AAAI Press 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  Solving real-world problems using symbolic planning often requires a simplified formulation of the original problem, since certain subproblems cannot be represented at all or only in a way leading to inefficiency. For example, manipulation planning may appear as a subproblem in a robotic planning context or a packing problem can be part of a logistics task. In this paper we propose an extension of PDDL for specifying semantic attachments. This allows the evaluation of grounded predicates as well as the change of fluents by externally specified functions. Furthermore, we describe a general schema of integrating semantic attachments into a forward-chaining planner and report on our experience of adding this extension to the planners FF and Temporal Fast Downward. Finally, we present some preliminary experiments using semantic attachments.

• Patrick Eyerich, Robert Mattmüller and Gabriele Röger.
  Using the Context-enhanced Additive Heuristic for Temporal and Numeric Planning.
  In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009). 2009.
  To appear.
  (Show abstract) (Hide abstract) (PDF)
  

  Planning systems for real-world applications need the ability to handle concurrency and numeric fluents. Nevertheless, the predominant approach to cope with concurrency followed by the most successful participants in the latest International Planning Competitions (IPC) is still to find a sequential plan that is rescheduled in a post-processing step. We present Temporal Fast Downward (TFD), a planning system for temporal problems that is capable of finding low-makespan plans by performing a heuristic search in a temporal search space. We show how the context-enhanced additive heuristic can be successfully used for temporal planning and how it can be extended to numeric fluents. TFD often produces plans of high quality and, evaluated according to the rating scheme of the last IPC, outperforms all state-of-the-art temporal planning systems.

• Dunbo Cai, Jörg Hoffmann and Malte Helmert.
  Enhancing the Context-Enhanced Additive Heuristic with Precedence Constraints.
  In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pp. 50-57. AAAI Press 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Recently, Helmert and Geffner proposed the context-enhanced additive heuristic, where fact costs are evaluated relative to context states that arise from achieving first a pivot condition of each operator. As Helmert and Geffner pointed out, the method can be generalized to consider contexts arising from arbitrary precedence constraints over operator conditions instead. Herein, we provide such a generalization. We extend Helmert and Geffner's equations, and discuss a number of design choices that arise. Drawing on previous work on goal orderings, we design a family of methods for automatically generating precedence constraints. We run large-scale experiments, showing that the technique can help significantly, depending on the choice of precedence constraints. We shed some light on this by profiling the behavior of all possible precedence constraints, using a sampling technique.

• Malte Helmert and Carmel Domshlak.
  Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?
  In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pp. 162-169. AAAI Press 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Current heuristic estimators for classical domain-independent planning are usually based on one of four ideas: delete relaxations, critical paths, abstractions, and, most recently, landmarks. Previously, these different ideas for deriving heuristic functions were largely unconnected.

  We prove that admissible heuristics based on these ideas are in fact very closely related. Exploiting this relationship, we introduce a new admissible heuristic called the landmark cut heuristic, which compares favourably with the state of the art in terms of heuristic accuracy and overall performance.

• Silvia Richter and Malte Helmert.
  Preferred Operators and Deferred Evaluation in Satisficing Planning.
  In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pp. 273-280. AAAI Press 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Heuristic forward search is the dominant approach to satisficing planning to date. Most successful planning systems, however, go beyond plain heuristic search by employing various search-enhancement techniques. One example is the use of helpful actions or preferred operators, providing information which may complement heuristic values. A second example is deferred heuristic evaluation, a search variant which can reduce the number of costly node evaluations. Despite the wide-spread use of these search-enhancement techniques however, we note that few results have been published examining their usefulness. In particular, while various ways of using, and possibly combining, these techniques are conceivable, no work to date has studied the performance of such variations. In this paper, we address this gap by examining the use of preferred operators and deferred evaluation in a variety of settings within best-first search. In particular, our findings are consistent with and help explain the good performance of the winners of the satisficing tracks at IPC 2004 and 2008.

• Christoph Betz and Malte Helmert.
  Planning with h+ in Theory and Practice.
  In Bärbel Mertsching, Marcus Hund and Zaheer Aziz, Proceedings of the 32nd Annual German Conference on Artificial Intelligence (KI 2009), pp. 9-16. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Many heuristic estimators for classical planning are based on the so-called delete relaxation, which ignores negative effects of planning operators. Ideally, such heuristics would compute the actual goal distance in the delete relaxation, i.e., the cost of an optimal relaxed plan, denoted by h+. However, current delete relaxation heuristics only provide (often inadmissible) estimates to h+ because computing the correct value is an NP-hard problem.

  In this work, we consider the approach of planning with the actual h+ heuristic from a theoretical and computational perspective. In particular, we provide domain-dependent complexity results that classify some standard benchmark domains into ones where h+ can be computed efficiently and ones where computing h+ is NP-hard. Moreover, we study domain-dependent implementations of h+ which show that the h+ heuristic provides very informative heuristic estimates compared to other state-of-the-art heuristics.

• Pascal Bercher and Robert Mattmüller.
  Solving Non-deterministic Planning Problems with Pattern Database Heuristics.
  In B. Mertsching, M. Hund and Z. Aziz, Proceedings of the 32nd Annual Conference on Artificial Intelligence (KI 2009), pp. 57-64. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Non-determinism arises naturally in many real-world applications of action planning. Strong plans for this type of problems can be found using AO* search guided by an appropriate heuristic function. Most domain-independent heuristics considered in this context so far are based on the idea of ignoring delete lists and do not properly take the non-determinism into account. Therefore, we investigate the applicability of pattern database (PDB) heuristics to non-deterministic planning. PDB heuristics have emerged as rather informative in a deterministic context. Our empirical results suggest that PDB heuristics can also perform reasonably well in non-deterministic planning. Additionally, we present a generalization of the pattern additivity criterion known from classical planning to the non-deterministic setting.

• Florian Pommerening, Stefan Wölfl and Matthias Westphal.
  Right-of-Way Rules as Use Case for Integrating GOLOG and Qualitative Reasoning.
  In Bärbel Mertsching, Marcus Hund and Muhammad Zaheer Aziz, Proceedings of the 32nd Annual Conference on Artificial Intelligence (KI 2009), pp. 468-475. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (PDF) (DBLP)
  

  Agents interacting in a dynamically changing spatial environment often need to access the same spatial resources. A typical example is given by moving vehicles that meet at an intersection in a street network. In such situations right-of-way rules regulate the actions the vehicles involved may perform. For this application scenario we show how the Golog framework for reasoning about action and change can be enhanced by external reasoning services that implement techniques known from the domain of Qualitative Spatial Reasoning.

• Michael Brenner and Bernhard Nebel.
  Continual Planning and Acting in Dynamic Multiagent Environments.
  Journal of Autonomous Agents and Multiagent Systems 19 (3), pp. 297-331. 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  In order to behave intelligently, artificial agents must be able to deliberatively plan their future actions. Unfortunately, realistic agent environments are usually highly dynamic and only partially observable, which makes planning computationally hard. For most practical purposes this rules out planning techniques that account for all possible contingencies in the planning process. However, many agent environments permit an alternative approach, namely continual planning, i.e. the interleaving of planning with acting and sensing.

  This paper presents a new principled approach to continual planning that describes why and when an agent should switch between planning and acting. The resulting continual planning algorithm enables agents to deliberately postpone parts of their planning process and instead actively gather missing information that is relevant for the later refinement of the plan. To this end, the algorithm explictly reasons about the knowledge (or lack thereof) of an agent and its sensory capabilities. These concepts are modelled in the planning language MAPL. Since in many environments the major reason for dynamism is the behaviour of other agents, MAPL can also model multiagent environments, common knowledge among agents, and communicative actions between them. For Continual Planning, MAPL introduces the concept of of assertions, abstract actions that substitute yet unformed subplans.

  To evaluate our continual planning approach empirically we have developed MAPSIM, a simulation environment that automatically builds multiagent simulations from formal MAPL domains. Thus, agents can not only plan, but also execute their plans, perceive their environment, and interact with each other. Our experiments show that, using continual planning techniques, deliberate action planning can be used efficiently even in complex multiagent environments.

• Martin Wehrle and Malte Helmert.
  The Causal Graph Revisited for Directed Model Checking.
  In Jens Palsberg and Zhendong Su, Proceedings of the 16th International Static Analysis Symposium (SAS 2009), pp. 86-101. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Directed model checking is a well-established technique to tackle the state explosion problem when the aim is to find error states in large systems. In this approach, the state space traversal is guided through a function that estimates the distance to nearest error states. States with lower estimates are preferably expanded during the search. Obviously, the challenge is to develop distance functions that are efficiently computable on the one hand and as informative as possible on the other hand. In this paper, we introduce the causal graph structure to the context of directed model checking. Based on causal graph analysis, we first adapt a distance estimation function from AI planning to directed model checking. Furthermore, we investigate an abstraction that is guaranteed to preserve error states. The experimental evaluation shows the practical potential of these techniques.

• Jens Witkowski.
  Eliciting Honest Reputation Feedback in a Markov Setting.
  In Proceedings of the 21th International Joint Conference on Artificial Intelligence (IJCAI 2009). 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Recently, online reputation mechanisms have been proposed that reward agents for honest feedback about products and services with fixed quality. Many real-world settings, however, are inherently dynamic. As an example, consider a web service that wishes to publish the expected download speed of a file mirrored on different server sites. In contrast to the models of Miller, Resnick and Zeckhauser and of Jurca and Faltings, the quality of the service (e.g., a server's available bandwidth) changes over time and future agents are solely interested in the present quality levels. We show that hidden Markov models (HMM) provide natural generalizations of these static models and design a payment scheme that elicits honest reports from the agents after they have experienced the quality of the service.

• Moritz Göbelbecker and Christian Dornhege.
  Realistic Cities in Simulated Environments - An Open Street Map to Robocup Rescue Converter.
  In Online-Proceedings of the Fourth International Workshop on Synthetic Simulation and Robotics to Mitigate Earthquake Disaster (SRMED 2009). 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  A general problem when developing large scale disaster simulation environments is to acquire GIS data. In this work, we tackle the problem of map generation from public sources. Usually the major problem is not only the data conversion itself, but to get access to the data at all. We solve this problem by using the website OpenStreetMap.org, that provides mapping data for the whole world in a wiki-style concept, as our source of data, thus being able to generate maps for almost any city. The data is converted to the format required by the Robocup Rescue Simulation System, enabling simulations on various real-world scenarios.

• Jörg Hoffmann, Piergiorgio Bertoli, Malte Helmert and Marco Pistore.
  Message-Based Web Service Composition, Integrity Constraints, and Planning under Uncertainty: A New Connection.
  Journal of Artificial Intelligence Research 35, pp. 49-117. 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  Thanks to recent advances, AI Planning has become the underlying technique for several applications. Figuring prominently among these is automated Web Service Composition (WSC) at the "capability" level, where services are described in terms of preconditions and effects over ontological concepts. A key issue in addressing WSC as planning is that ontologies are not only formal vocabularies; they also axiomatize the possible relationships between concepts. Such axioms correspond to what has been termed "integrity constraints" in the actions and change literature, and applying a web service is essentially a belief update operation. The reasoning required for belief update is known to be harder than reasoning in the ontology itself. The support for belief update is severely limited in current planning tools.

  Our first contribution consists in identifying an interesting special case of WSC which is both significant and more tractable. The special case, which we term forward effects, is characterized by the fact that every ramification of a web service application involves at least one new constant generated as output by the web service. We show that, in this setting, the reasoning required for belief update simplifies to standard reasoning in the ontology itself. This relates to, and extends, current notions of "message-based" WSC, where the need for belief update is removed by a strong (often implicit or informal) assumption of "locality" of the individual messages. We clarify the computational properties of the forward effects case, and point out a strong relation to standard notions of planning under uncertainty, suggesting that effective tools for the latter can be successfully adapted to address the former.

  Furthermore, we identify a significant sub-case, named strictly forward effects, where an actual compilation into planning under uncertainty exists. This enables us to exploit off-the-shelf planning tools to solve message-based WSC in a general form that involves powerful ontologies, and requires reasoning about partial matches between concepts. We provide empirical evidence that this approach may be quite effective, using Conformant-FF as the underlying planner.

• Rainer Kümmere, Bastian Steder, Christian Dornhege, Michael Ruhnke, Giorgio Grisetti, Cyrill Stachniss and Alexander Kleiner.
  On measuring the accuracy of SLAM algorithms.
  Autonomous Robots 27 (4), pp. 387-407. 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  In this paper, we address the problem of creating an objective benchmark for evaluating SLAM approaches. We propose a framework for analyzing the results of a SLAM approach based on a metric for measuring the error of the corrected trajectory. This metric uses only relative relations between poses and does not rely on a global reference frame. This overcomes serious shortcomings of approaches using a global reference frame to compute the error. Our method furthermore allows us to compare SLAM approaches that use different estimation techniques or different sensor modalities since all computations are made based on the corrected trajectory of the robot.

  We provide sets of relative relations needed to compute our metric for an extensive set of datasets frequently used in the robotics community. The relations have been obtained by manually matching laser-range observations to avoid the errors caused by matching algorithms. Our benchmark framework allows the user to easily analyze and objectively compare different SLAM approaches.

• Alexander Schimpf, Stephan Merz and Jan-Georg Smaus.
  Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.
  In Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), pp. 424-439. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (BIB)
  

  We present the implementation of a translation of LTL formulae into automata in Isabelle/HOL, which is an essential component of LTL model checking algorithms. In automaton-based model checking, we have a system modelled as a transition system and a correctness property stated as a temporal (in our case: LTL) formula. Such a formula can be translated into a (generalised) Büchi automaton that accepts precisely those behaviours allowed by the formula. Checking correctness of the system thus amounts to a language inclusion property between the two automata. We implemented a standard translation algorithm due to Gerth et al. The correctness and termination of our implementation is shown in Isabelle/HOL, and executable code is generated using the Isabelle/HOL code generator.

• Stefan Ratschan and Jan-Georg Smaus.
  Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate.
  In Catherine Dubois, Proceedings of the 3rd International Conference on Tests And Proofs (TAP 2009), pp. 153-168. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a trajectory to an unsafe state. The approach is to approximate how close a point is to being an initial point of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for an optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verification algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts.

• Bahareh Badban, Stefan Leue and Jan-Georg Smaus.
  Automated Invariant Generation for the Verification of Real-Time Systems.
  In Andrew Ireland and Laura Kovács, Proceedings of the 2nd International Workshop on Invariant Generation (WING 2009). 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  We present an approach to automatically generating invariants for timed automata models. The CIPM algorithm that we propose first computes new invariants for timed automata control locations taking their originally defined invariants as well as the constrains on clock variables imposed by incoming state transitions into account. In doing so the CIPM algorithm also prunes idle transitions, which are transitions that can never be taken, from the automaton. We discsuss a prototype implementation of the CIPM algorithm as well as some initial experimental results.

• Stefan Ratschan and Jan-Georg Smaus.
  Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate.
  In Tarmo Uustalu and Jüri Vain, Proceedings of the 20th Nordic Workshop on Programming Theory (NWPT 2008), pp. 72-74. 2008.
  (PDF) (BIB)
  

• Matthias Westphal and Stefan Wölfl.
  Qualitative CSP, finite CSP, and SAT: Comparing methods for qualitative constraint-based reasoning.
  In Proceedings of the 21th International Joint Conference on Artificial Intelligence (IJCAI 2009). 2009.
  (Show abstract) (Hide abstract) (PDF) (DBLP)
  

  Qualitative Spatial and Temporal Reasoning (QSR) is concerned with constraint-based formalisms for representing, and reasoning with, spatial and temporal information over infinite domains. Within the community it has been a widely accepted assumption that genuine qualitative reasoning methods outperform other reasoning methods that are applicable to encodings of qualitative CSP instances. Recently this assumption has been tackled by several authors, who proposed to encode qualitative CSP instances as finite CSP or SAT instances. In this paper we report on the results of a broad empirical study in which we compared the performance of several reasoners on instances from different qualitative formalisms. Our results show that for small-sized qualitative calculi (e.g. Allen's interval algebra and RCC-8) a state-of-the-art implementation of QSR methods currently gives the most efficient performance. However, on recently suggested large-size calculi, e.g. OPRA_4, finite CSP encodings provide a considerable performance gain. These results confirm a conjecture by Bessière stating that support-based constraint propagation algorithms provide better performance for large-sized qualitative calculi.

• Stefan Wölfl and Matthias Westphal.
  On combinations of binary qualitative constraint calculi.
  In Proceedings of the 21th International Joint Conference on Artificial Intelligence (IJCAI 2009). 2009.
  (Show abstract) (Hide abstract) (PDF) (DBLP)
  

  Qualitative constraint calculi are representation formalisms that allow for efficient reasoning about spatial and temporal information. Many of the calculi discussed in the field of Qualitative Spatial and Temporal Reasoning can be defined as combinations of other, simpler and more compact formalisms. On the other hand, existing calculi can be combined to a new formalism in which one can represent, and reason about, different aspects of a domain at the same time. For example, Gerevini and Renz presented a loose combination of the region connection calculus RCC-8 and the point algebra: the resulting formalism integrates topological and qualitative size relations between spatially extended objects. In this paper we compare the approach by Gerevini and Renz to a method that generates a new qualitative calculus by exploiting the semantic interdependencies between the component calculi. We will compare these two methods and analyze some formal relationships between a combined calculus and its components. The paper is completed by an empirical case study in which the reasoning performance of the suggested methods is compared on random test instances.

• Bernhard Nebel and Stefan Wölfl.
  Benchmarking of Qualitative Spatial and Temporal Reasoning Systems.
  2009.
  AAAI Technical Report SS-09-02.
  (AAAI)
  

• Martin Wehrle, Sebastian Kupferschmid and Andreas Podelski.
  Transition-based Directed Model Checking.
  In Stefan Kowalewski and Anna Philippou, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), pp. 186-200. Springer-Verlag 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  Directed model checking is a well-established technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by an abstract distance function that estimates a state's distance to a nearest error state. In this paper, we propose a general enhancement to directed model checking based on the evaluation of state transitions. We present a schema, parametrized by an abstract distance function, to evaluate transitions and propose a new method for the state space traversal. Our framework can be applied automatically to a wide range of abstract distance functions. The empirical evaluation impressively shows its practical potential. Apparently, the new method identifies a sweet spot in the trade-off between scalability (memory consumption) and short error traces.

• Geert-Jan Kruijff and Michael Brenner.
  Phrasing Questions.
  In AAAI Spring Symposium on Agents that Learn from Human Teachers. 2009.
  

• Wolfram Burgard, Cyrill Stachniss, Giorgio Grisetti, Bastian Steder, Rainer Kümmerle, Christian Dornhege, Michael Ruhnke, Alexander Kleiner and Juan D. Tardos.
  A Comparison of SLAM Algorithms Based on a Graph of Relations.
  In Proceedings of the IEEE/RSJ Int. Conf. on Intelligent Robots and Systems (IROS). 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  In this paper, we address the problem of creating an objective benchmark for comparing SLAM approaches. We propose a framework for analyzing the results of SLAM approaches based on a metric for measuring the error of the corrected trajectory. The metric uses only relative relations between poses and does not rely on a global reference frame. The idea is related to graph-based SLAM approaches in the sense that it considers the energy needed to deform the trajectory estimated by a SLAM approach to the ground truth trajectory. Our method enables us to compare SLAM approaches that use different estimation techniques or different sensor modalities since all computations are made based on the corrected trajectory of the robot. We provide sets of relative relations needed to compute our metric for an extensive set of datasets frequently used in the SLAM community. The relations have been obtained by manually matching laser-range observations. We believe that our benchmarking framework allows the user an easy analysis and objective comparisons between different SLAM approaches.

• Malte Helmert.
  Concise finite-domain representations for PDDL planning tasks.
  Artificial Intelligence 173, pp. 503-535. 2009.
  (Show abstract) (Hide abstract) (PDF)
  

  We introduce an efficient method for translating planning tasks specified in the standard PDDL formalism into a concise grounded representation that uses finite-domain state variables instead of the straight-forward propositional encoding.

  Translation is performed in four stages. Firstly, we transform the input task into an equivalent normal form expressed in a restricted fragment of PDDL. Secondly, we synthesize invariants of the planning task that identify groups of mutually exclusive propositions which can be represented by a single finite-domain variable. Thirdly, we perform an efficient relaxed reachability analysis using logic programming techniques to obtain a grounded representation of the input. Finally, we combine the results of the third and fourth stage to generate the final grounded finite-domain representation.

  The presented approach has originally been implemented as part of the Fast Downward planning system for the 4th International Planning Competition (IPC4). Since then, it has been used in a number of other contexts with considerable success, and the use of concise finite-domain representations has become a common feature of state-of-the-art planners.

• Rainer Kümmerle, Bastian Steder, Christian Dornhege, Alexander Kleiner, Giorgio Grisetti and Wolfram Burgard.
  Large Scale Graph-based SLAM using Aerial Images as Prior Information.
  In Proceedings of Robotics: Science and Systems (RSS). 2009.
  (Show abstract) (Hide abstract) (PDF) (BIB)
  

  To effectively navigate in their environments and accurately reach their target locations, mobile robots require a globally consistent map of the environment. The problem of learning a map with a mobile robot has been intensively studied in the past and is usually referred to as the simultaneous localization and mapping (SLAM) problem. However, existing solutions to the SLAM problem typically rely on loop-closures to obtain global consistency and do not exploit prior information even if it is available. In this paper, we present a novel SLAM approach that achieves global consistency by utilizing publicly accessible aerial photographs as prior information. Our approach inserts correspondences found between three-dimensional laser range scans and the aerial image as constraints into a graph-based formulation of the SLAM problem. We evaluate our algorithm based on large real-world datasets acquired in a mixed in- and outdoor environment by comparing the global accuracy with state-of-the-art SLAM approaches and GPS. The experimental results demonstrate that the maps acquired with our method show increased global consistency.

• Michael Brenner.
  Continual Collaborative Planning for Mixed-Initiative Action and Interaction.
  In Proceedings of the 7th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2008). 2008.
  (Show abstract) (Hide abstract) (PDF)
  

  Multiagent environments are often highly dynamic and only partially observable which makes deliberative action planning computationally hard. In many such environments, however, agents can take a more proactive approach and suspend planning for partial plan execution, especially for active information gathering and interaction with others. This paper presents a new algorithm for Continual Collaborative Planning (CCP) that enables agents to deliberately interleave planning, acting, perception and communication. Our implementation of CCP has been evaluated with MAPSIM, a tool that automatically generates multiagent simulations from formal multiagent planning (MAP) domains. For different such simulations, we show how CCP leads to collaborative planning and acting and, despite minimal linguistic capabilities, to fairly natural dialogues between agents.

• Michael Brenner and Ivana Kruijff-Korbayova.
  A Continual Multiagent Planning Approach to Situated Dialogue.
  In Proceedings of the 12th Workshop on the Semantics and Pragmatics of Dialogue (LonDial 2008). 2008.
  (Show abstract) (Hide abstract) (PDF)
  

  Situated dialogue is usually tightly integrated with behavior planning, physical action and perception. This paper presents an algorithmic framework, Continual Collaborative Planning (CCP), for modeling this kind of integrated behavior and shows how CCP agents naturally blend physical and communicative actions. For experiments with conversational CCP agents we have developed MAPSIM, a software environment that can generate multiagent simulations from formal multiagent planning problems automatically. MAPSIM permits comparison of CCP-based dialogue strategies on a wide range of domains and problems without domain-specific programming. Despite their linguistic capabilities being limited MAPSIM agents can already engage in fairly realistic situated dialogues. Our ongoing work is taking this approach from simulation to real human-robot interaction.

• Geert-Jan Kruijff, Michael Brenner and Nick Hawes.
  Continual Planning for Cross-Modal Situated Clarification in Human-Robot Interaction.
  In Proceedings of the 17th IEEE International Symposium on Robots and Human Interactive Communication (RO-MAN 2008). 2008.
  (Show abstract) (Hide abstract) (PDF)
  

  Current robots do not fully understand the world they are situated in, including what humans talk to them about. A fundamental problem in robotics is thus how a robot can clarify such a lack of understanding. This paper addresses the question of how a robot can create a plan for resolving a need for clarification. This paper characterizes situated clarification as an information need which may arise in any sensory-motoric modality interpreting the situated context of the robot, or any deliberative modality referring to that context. The paper then focuses on how, once a clarification need has been identified, the robot can create a plan in which one or more modalities are involved in resolving it. Modalities are involved on the basis of the types of information they can provide. These information types are identified in the ontologies the modalities use to interconnect their content with content of other modalities ("information fusion"). We take a continual approach to planning and execution monitoring. This provides the abiltity to re-plan depending on modality availability and success in resolving (part of) a clarification need. We illustrate our implementation of this approach with several examples from our system.