Modeling and analysis for robotics: theory and practice

Embedded software, cyber-physical systems, robotic applications have shown the challenges of thigh connection between a software architecture and a hardware system which has to interact with the physical world in the classical sense-plan-act loop.
Traditional modeling techniques have evolved to capture the peculiarities of these system. This talk will present first an overview of the problems faced when modeling and analyzing such systems and then present a toolchain to model a ROS-based robotic system. This model, based on AADL, can be used for analysis and automatic code generation. The talk will conclude by listing open challenges related with this approach and the field in general.

Probabilistic planning with formal guarantees for mobile robots

In this talk we present a method to compute cost-optimal policies for a robot planning problem where the environment does not allow the robot to successfully execute certain task. This method uses co-safe linear temporal logic for tasks specification and a Markov decision process model to encode the uncertainty of robot's actions. With this method it is possible to generate policies that are formally guaranteed to (in decreasing order of priority) maximize the probability of finishing the task, maximize progress towards completion (if this is not possible), and minimize the expected time cost required.