Imagine a robot waiter having to surve customers with plates. Can we formalize its specification and automatically synthesize his behavior? How can he cope with the different data on the menu? If another waiter robot broke a glass, can he avoid trumpling over it on his way to the kitchen? How can we design it in a composite way, leveraging working provable subcomponents?
Design of robotic systems, being complete autonomous machines, involves many facets that are absent in the design of other computerized systems. The robotics theme thus present new challenges for automatic synthesis as envisioned by ExCAPE. Motion planning is a prominent example. ExCAPE researchers have developed an open source motion planning library implementing motions solvers that allow the satisfaction of a high level specification while at the same time ensuring a feasible robot motion plan is produced. Other researched areas include synthesis in partially unknown environments, syntheis with costs, synthesis with complex dynamics, and synthesis for multi-robot motion planning.
We address the problem of synthesizing optimal robot controllers for adversarial environments. Our main observation is that the quality of a path to a goal has two dimensions: (1) the number of phases in which the robot waits for the environment to perform some actions and (2) the cost of the robot’s actions to reach the goal. Our synthesis algorithm can take any prioritization over the possible cost combinations into account, and computes the optimal strategy in a symbolic manner, despite the fact that the action costs can be non-integer [JK13,JEK13].
In one approach to synthesizing a reactive control software for robots with complex dynamics, we developed an automatic construction of low-level controllers that ensure the correct continuous execution of a highlevel mission plan. Controllers are generated using trajectory-based verification to produce a set of robust reach tubes which strictly guarantee that the required motions achieve the desired task specification. Reach tubes, computed here by solving a series of sum-of-squares optimization problems, are composed in such a way that all trajectories ensure correct high-level behaviors [HK13]. In a second approach to the problem, we incorporated into the synthesis process an automatically generated abstraction of the robot dynamics. Thus if the controller can be synthesized, the behavior will be correct. We then examined how to provide revisions to the specifications when the dynamics of the robot cause the specification to be unrealizable.
We reason about how to synthesize and execute robot controllers for robots with different actions that are not instantaneous, so that the continuous execution is correct with respect to the specification no matter which action completes first. We have shown how this methods generalizes to multi robot tasks [RPK13,RK14].
We consider the synthesis of reactive systems from specifications with identifiers. Identifiers are useful to parametrize the input and output of a reactive system, for example, to state which client requests a grant from an arbiter, or the type of object that a robot is expected to fetch. Traditional reactive synthesis algorithms only handle a constant bounded range of such identifiers. However, in practice, we might not want to restrict the number of clients of an arbiter or the set of object types handled by a robot a priori. We first present a concise automata-based formalism for specifications with identifiers. The synthesis problem for such specifications is undecidable. We therefore give an algorithm that is always sound, and complete for unrealizable safety specifications. Our algorithm is based on computing a pattern-based abstraction of a synthesis game that captures the realizability problem for the specification. The abstraction does not restrict the possible solutions to finite-state ones and captures the obligations for the system in the synthesis game [ESK14].
We address the problem of robot plan synthesis in partially-unknown environments by combining a multi-layered synergistic framework with an iterative planning strategy [MLKKV13]. The approach employs the synergistic planning framework, which can handle complex dynamical systems, to generate continuous robotic trajectories that satisfy a given temporal logic specification. Once an unknown environment feature is encountered during the execution of the trajectory, the synergistic framework is called again to generate a new plan from the current state of the robot. The replanning step is fast because the expensive computations related to the temporal logic specification do not need to be repeated. In this approach, the planner deals with the unknown features only when they are discovered. In the case that the discovered feature renders the specification unsatisfiable, the planner uses a satisfaction metric to generate a trajectory that satisfies the specification as closely as possible. Case studies on a second-order car-like robot in an office environment with unknown obstacles illustrate the efficacy of the framework. In all the case studies, the planner successfully synthesized optimal robot trajectories with respect to the satisfaction metric of the specification.
Platform-based design means that the design proceeds in a double direction: (A) bottom-up: this is the direction that allows the designer to build the platform library, choosing the abstractions of functionalities and performance from a given architectural space; (B) top-down: in this direction, the design composes the library elements in order to define a specific function. This is a mapping process. Usually, in the top-down approach, the designer tries to compose a specific solution in an iterative way. Once he has arranged a possible implementation, he evaluates the performance information that the platform components of the library provide at that level and, eventually, he/she proceeds with additional iterations until the implementation meets the desired performance. Always in the top-level direction, if there is the need of specifuc platform elements that are not available at that time, the designer is allowed to instantiate new platform blocks through the definition of placeholders, that are added to the library and implemented in the lower level of abstraction in a second time. In order to avoid large-loop iterations, it is possible to define more platforms at different layers of abstraction. This process, that bring at the definition of a platform stack, is the key of the PBD. In the restaurant waiter scenario, some steps have been taken to meet the PBD principles. The first step is to define the basic functionalities that the robot is equipped with. This requires extrapolation of some information from the physical level in order to build the library of components. These elements from the lowest level include some physical quantities that could be useful in the design process (for example, energy, precision, time). We are also working to find a "common language" for guaranteeing that all the synthesis groups can interface correctly with the motion planner.
The problem of planning for robots with action uncertainty from high-level task descriptions is considered in this project. The main objective is to develop a framework that efficiently synthesizes optimal policies for uncertain systems to satisfy a temporal logic specification with maximum probability. To achieve this objective, the evolution of the stochastic system is first abstracted to a discrete, bounded-parameter Markov decision process (BMDP). The procedure is automated by algorithmic discretization of the system's states space and computation of optimal local policies enabling the system to transit between neighboring discrete regions [LLMK14a, LLMK14b]. Then, a global control policy over the product of the BMDP abstraction and the DFA representing the specification is generated. Analysis of the framework reveals that as the resolution of the abstraction becomes finer, the global policy converges to optimal [LLMK14c]. Simulated experiments confirm the theoretical results and illustrate that high-quality policies can be obtained in seconds, orders of magnitude faster than existing methods.
We consider the problem of compositional motion planning for multi-robot systems [SRKPS14]. Given the runtime behavior of a group of robots, specified using a set of safe LTL properties, the goal is to synthesize the robots motion plan. Our method relies on a library of motion primitives that provides a set of controllers to be used to control the behavior of the robots in different configurations. Using the closed loop behavior of the robots under the action of different controllers, we formulate the motion planning problem as a constraint solving problem and use an off-the-shelf satisfiability modulo theories (SMT) solver to solve the constraints and generate trajectories for the individual robot. Our approach can also be extended to synthesize optimal cost trajectories where optimality is defined with respect to the available motion primitives. Experimental results show that this framework has potential to solve complex motion planning problems in the context of multi-robot systems. See here the tool, ComPlan, devloped for this task, and a short video.
We are investigating the problem of supervisory control of vehicular networks for collision avoidance at intersections. Our efforts in the past year have been focused on the case of imperfect measurement in the position of the vehicles. Our approach to this problem is to use abstraction techniques for modeling a set of vehicles as a discrete event system, using controllable and uncontrollable events to model control actions, uncontrolled vehicles, and a disturbance. We have shown that this modeling formalism can also be used to incorporate measurement uncertainty by adding another class of observable but uncontrollable events to model measurement. To deal with the fact that the set of measurements are a subset of a continuous rather than a discrete space, we partitioned the set of continuous measurements into a set of equivalence classes (determined with respect to the spatial discretization of the abstraction), and defined an observable but uncontrollable event corresponding to each equivalence class. The same techniques can be extended to other robotic systems, which typically have to deal with the same complicating factors, namely disturbances, uncontrollable environments, and measurement uncertainty [DCDL13,DL14].
The reactive synthesis problem is to find a finite-state controller that satisfies a given temporal-logic specification regardless of how its environment behaves. Developing a formal specification is a challenging and tedious task and initial specifications are often unrealizable. In many cases, the source of unrealizability is the lack of adequate assumptions on the environment of the system. In this paper, we consider the problem of automatically correcting an unrealizable specification given in the generalized reactivity (1) fragment of linear temporal logic, by adding assumptions on the environment. When a temporal-logic specification is unrealizable, the synthesis algorithm computes a counter-strategy as a witness. Our algorithm then analyzes this counter-strategy and synthesizes a set of candidate environment assumptions that can be used to remove the counter-strategy from environment's possible behaviors. We demonstrate the applicability of our approach with several examples and case studies from the robotics domain [AMT13].
- R. Alur, S. Moarref, and U. Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2013.
- E. Dallal, A. Colombo, D. Del Vecchio, and S. Lafortune. Supervisory control for collision avoidance in vehicular networks with imperfect measurements. In Proceedings of the 52nd IEEE Conference on Decision and Control (CDC). December 2013, pp. 6298-6303.
- E. Dallal and S. Lafortune. On Most Permissive Observers in Dynamic Sensor Activation Problems. IEEE Trans. Automat. Contr. 59(4): 966-981 (2014).
- J. A. DeCastro, H. Kress-Gazit. Guaranteeing reactive high-level behaviors for robots with complex dynamics. IROS 2013: 749-756
- J. A. DeCastro, H. Kress-Gazit. Synthesis of Nonlinear Continuous Controllers for Verifiably-Correct High-Level, Reactive Behaviors. International Journal of Robotic Research, accepted.
- R. Ehlers, S. A. Seshia, and H. Kress-Gazit. Synthesis with Identifiers. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 415–433, January 2014.
- G. Jing, R. Ehlers, H. Kress-Gazit: Shortcut through an evil door: Optimality of correct-by-construction controllers in adversarial environments. IROS 2013: 4796-4802
- G. Jing, H. Kress-Gazit. Improving the continuous execution of reactive LTL-based controllers. ICRA 2013: 5439-5445
- R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki. Fast Stochastic Motion Planning with Optimality Guarantees using Local Policy Reconfiguration. IEEE International Conference on Robotics and Automation, Hong Kong, China, 2014.
- R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki. Optimal and Efficient Stochastic Motion Planning in Partially-Known Environments. The Twenty-Eighth AAAI Conference on Artificial Intelligence, Quebec City, Canada, 2014.
- R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki. Asymptotically Optimal Stochastic Motion Planning with Temporal Goals. Workshop on the Algorithmic Foundations of Robotics (WAFR), Istanbul, Turkey, 2014.
- M. R. Maly, M. Lahijanian, L. E. Kavraki, H, Kress-Gazit, M. Y. Vardi. Iterative temporal motion planning for hybrid systems in partially unknown environments. HSCC 2013: 353-362
- S. Maniatopoulos, M. Blair, C. Finucane and H. Kress-Gazit. Open-World Mission Specification for Reactive Robots. IEEE International Conference on Robotics and Automation 2014, Shanghai, China, May 2014.
- V. Raman, C. Finucane and H. Kress-Gazit. Temporal Logic-Based Mission Planning for Robots with Slow and Fast Actions. In the Proceedings of the 2012 IEEE/RSJ International Conference on Intelligent Robots and Systems, Vilamoura, Algarve, Portugal, October 2012.
- V. Raman and H. Kress-Gazit. Synthesis for multi-robot controllers with interleaved motion. In IEEE International Conference on Robotics and Automation 2014
- V. Raman and H. Kress-Gazit. Minimal Explanations of Unsynthesizability for High-Level Robot Behaviors. In the Proceedings of the 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems, Tokyo, Japan, November 2013.
- V. Raman, C. Lignos, C. Finucane, K. Lee, M. Marcus and H. Kress-Gazit. Sorry Dave, I’m Afraid I Can’t Do That: Explaining Unachievable Robot Tasks Using Natural Language. In the Proceedings of Robotics: Science and Systems 2013, Berlin, Germany, June 2013.
- V. Raman, N. Piterman, and H. Kress-Gazit. Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. In IEEE/RSJ International Conference on Intelligent Robots and Systems, ICRA 2013, pages 4075–4081
- V. Raman, B. Xu and H. Kress-Gazit. Avoiding Forgetfulness: Structured English Specifications for High-Level Robot Control with Implicit Memory. In the Proceedings of the 2012 IEEE/RSJ International Conference on Intelligent Robots and Systems, Vilamoura, Algarve, Portugal, October 2012.
- I. Saha, R. Ramaitithima, V. Kumar, G. J. Pappas and S. A. Seshia. Automated Composition of Motion Primitives for Multi-Robot Systems from Safe LTL Specifications. IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2014.
- K.W. Wong, R. Ehlers and H. Kress-Gazit. Correct High-level Robot Behavior in Environments with Unexpected Events. In the Proceedings of Robotics: Science and Systems 2014, Berkeley, CA, July 2014.
- K. W. Wong, C. Finucane, H. Kress-Gazit. Provably-correct robot control with LTLMoP, OMPL and ROS. IROS 2013: 2073