# Program

 09:00 - 10:30 Session 1: Chair: Malte Helmert Jan-Georg Smaus Construction of Buchi Automata for LTL Model Checking Verified in Isabelle/HOL Abstract: We present the implementation in Isabelle/HOL of a translation of LTL formulae into Buchi automata. In automaton-based model checking, systems are modeled as transition systems, and correctness properties stated as formulae of temporal logic are translated into corresponding automata. An LTL formula is represented by a (generalized) Buchi automaton that accepts precisely those behaviors allowed by the formula. The model checking problem is then reduced to checking language inclusion between the two automata. The automaton construction is thus an essential component of an LTL model checking algorithm. We implemented a standard translation algorithm due to Gerth et al. The correctness and termination of our implementation are proven in Isabelle/HOL, and executable code is generated using the Isabelle/HOL code generator. Christian Dornhege Coordinated Exploration with Marsupial Teams of Robots using Temporal Symbolic Planning Abstract: The problem of autonomously exploring an environment with a team of robots received considerable attention in the past. However, there are relatively few approaches to coordinate teams of robots that are able to deploy and retrieve other robots. Efficiently coordinating the exploration with such marsupial robots requires advanced planning mechanisms that are able to consider symbolic deployment and retrieval actions. In this paper, we propose a novel approach for coordinating the exploration with marsupial robot teams. Our method integrates a temporal symbolic planner that explicitly considers deployment and retrieval actions with a traditional utility-based assignment procedure. Our approach has been implemented and evaluated in several simulated environments and with varying team sizes. The results demonstrate that our proposed method is able to coordinate marsupial teams of robots to efficiently explore unknown environments. Moritz Gobelbecker Coming up With Good Excuses: What to do When no Plan Can be Found Abstract: When using a planner-based agent architecture, many things can go wrong. First and foremost, an agent might fail to execute one of the planned actions for some reasons. Even more annoying, however, is a situation where the agent is incompetent, i.e., unable to come up with a plan. This might be due to the fact that there are principal reasons that prohibit a successful plan or simply because the task's description is incomplete or incorrect. In either case, an explanation for such a failure would be very helpful. We will address this problem and provide a formalization of coming up with excuses for not being able to find a plan. Based on that, we will present an algorithm that is able to find excuses and demonstrate that such excuses can be found in practical settings in reasonable time. 10:30 - 10:45 Coffee Break 10:45 - 12:15 Session 2: Chair: Daniele Nardi Luca Iocchi Multi-Robot Teams for Environmental Monitoring Abstract: In this talk I will present the achievements of a project aiming at building a mobile reconfigurable multi-robot multi-camera automatic surveillance and monitoring system, that integrates visual and robotic surveillance techniques. I will describe the integrated framework developed to make vision components and robots interact, as well as human behavior analysis based on stereo vision and multi-robot coverage techniques. Luca Marchetti Towards a probabilistic approach for Multi-Robot area coverage Abstract: Video surveillance is an effective application for testing Distributed Data Fusion System. A hybrid architecture, composed by a team of mobile robots and a set of fixed camera, can pursue the surveillance task in a very effective way. In fact, the Multi-Robot System is able to cover a portion of the environment not directly perceived by the cameras, but can also support the belief of fixed sensors. In this talk, we present a probability density function based approach for the problem of Multi-Robot area coverage. The mobile robots are able to autonomously patrol an area, driven by an a-priori knowledge of the environment. The fixed cameras can modify the prior by adding a distributed event handling to the system. The robots can, thus, improve the effectiveness of the surveillance task by supporting the event-driven area coverage. Despite it is still under development, we would like to share some of the preliminary results obtained both in simulated environment and real world applications. Vittorio Amos Ziparo Learn to Behave! Rapid Training of Behavior Automata Abstract: Programming robot or virtual agent behaviors can be a challenging task, and makes attractive the prospect of automatically learning the behaviors from the actions of a human demonstrator. However, learning complex behaviors rapidly from a demonstrator may be difficult if they demand a large number of training samples. We describe an architecture for rapid learning of recurrent behaviors from demonstration. The architecture is based on deterministic hierarchical finite-state automata (HFAs) with classication algorithms taking the place of the state transition function. This architecture allows for task decomposition, statefulness, parameterized features and behaviors, per-behavior feature set customization, and storage of learned behaviors in libraries to be used later on as elements in more complex behaviors. We describe the system, and then illustrate its application in a simple, but nontrivial, foraging task involving multiple behaviors. 12:15 - 13:45 Lunch 13:45 - 15:15 Session 3: Chair: Jan-Georg Smaus Malte Helmert Sound and Complete Landmarks for And/Or Graphs Abstract: Landmarks for a planning problem are sub goals that are necessarily made true at some point in the execution of any valid plan. Since verifying that a fact is a landmark is PSPACE-complete, earlier approaches have focused on finding landmarks for the delete relaxation $\Pi^+$. Furthermore, some of these approaches have \emph{approximated} this set of landmarks, although it has been shown that the complete set of \emph{causal delete-relaxation landmarks} can be identified in polynomial time by a simple procedure over the relaxed planning graph. Here, we give a declarative characterization of this set of landmarks and show that the procedure computes the landmarks described by our characterization. Building on this, we observe that the procedure can be applied to any delete-relaxation problem and take advantage of a recent compilation of the $m$-relaxation of a problem into a problem with no delete effects to extract landmarks that take into account \emph{delete effects} in the original problem. We demonstrate that this approach finds strictly more causal landmarks than previous approaches and discuss the relationship between increased computational effort and experimental performance, using these landmarks in a recently proposed admissible landmark-counting heuristic. Robert Mattmuller Pattern Database Heuristics for Fully Observable Nondeterministic Planning Abstract: When planning in an uncertain environment, one is often interested in finding a contingent plan that prescribes appropriate actions for all possible states that may be encountered during the execution of the plan. We consider the problem of finding strong and strong cyclic plans for fully observable nondeterministic (FOND) planning problems. The algorithm we choose is LAO*, an informed explicit state search algorithm. We investigate the use of pattern database (PDB) heuristics to guide LAO* towards goal states. To obtain a fully domain-independent planning system, we use an automatic pattern selection procedure that performs local search in the space of pattern collections. The evaluation of our system on the FOND benchmarks of the Uncertainty Part of the International Planning Competition 2008 shows that our approach is competitive with symbolic regression search in terms of problem coverage and speed. Gabriele Roeger Stronger Abstractions for the Pancake Problem Abstract: The pancake problem is a famous search problem where the objective is to sort a sequence of objects (pancakes) through a minimal number of prefix reversals (flips). The best approaches for the problem are based on heuristic search with abstraction (pattern database) heuristics. We present a new class of abstractions for the pancake problem which have three advantages over the approaches considered in previous work. First, our new abstractions are size-independent, ie., do not need to be tailored to a particular instance size of the pancake problem. Second, they are more compact in that they can represent a larger number of pancakes within abstractions of bounded size. Finally, they can exploit symmetries in the problem specification to allow multiple heuristic lookups, significantly improving search performance over a single lookup. Our experimental results show that compared to the pattern databases suggested by Zahavi et al., our new techniques lead to an improvement of one order of magnitude in runtime and up to three orders of magnitude in the number of generated states. 15:15 - 15:30 Coffee Break 15:30 - 17:15 Session 4: Chair: Reyhan Aydogan Ehsan Ullah Warriach - Eirini Kaldeli Composing Services in a Smart Home Abstract: Domotics is concerned with the automation of the home to increase the safety and comfort of people. We propose a Service-Oriented Computing approach to manage the sensors and actuators of a generic home with the goal of creating an adaptive and interactive middleware. The assumption is that any home device is described as a discoverable service that can be accessed via XML standard descriptions, and a standardized plug-in architecture allows the addition of new devices. The coordination of the home is based on planning techniques that enables the user of the home to command the house issuing high-level instructions, and also allows the home to react to relevant contextual changes. In this talk, we illustrate a platform for smart homes that interacts bidirectional with a visualization/simulation application and the planning techniques that support the dynamic adaptable home coordination. Elie El-Khoury Adaptive Middleware for Large-scale Wireless Sensor Networks Abstract: Wireless Sensor Networks have found more and more applications in a variety of pervasive computing environments. As sensors are becoming more accessible, new challenges arise when deploying in a large-scale environment. The challenges include scalability, network load, communication overhead, security and heterogeneity of the devices. In this presentation, I draw the line over the existing studies on large-scale WSN middleware and then describe the persisting current issues with emphasis on the security challenges. With this in mind, I propose architecture for managing large-scale wireless sensor network, and identify the main research challenges. Viktoriya Degeler Searching for strategies to deal with distributed data inconsistencies Abstract: Pervasive distributed systems must function and make decisions in a constantly changing environment. The information they rely on originates from different distributed sensors and is subject to unbounded delays and faulty and noisy readings. This frequently results in having inconsistent data (outdated, incomplete, or contradictory). The challenge we have is to create an approach for the detection of different kinds of inconsistencies; an approach for reasoning about inconsistencies that we are unable to detect; and a strategy for optimally resolving a task in the presence of contradictory data. In this presentation, we will describe open research questions for dealing with data inconsistencies.