Robot challenges: Toward development of verification and synthesis techniques [from the Guest Editors]

This special issue describes the work being done toward creating formal methods for robotics and automation. Inherent to the approaches presented in this special issue is the idea that a robot, or team of robots, can be modeled as a hybrid system - a system that is defined by both discrete (states/modes) and continuous variables. Each mode can be viewed as a node in a state machine that has a dynamics associated with it, typically a set of differential equations. The continuous variables evolve based on the dynamics of the mode in which the system is in. The first three articles of the special issue rely on the notion of reachability analysis. Given a set of initial conditions, there are several approaches for calculating, exactly or approximately, the set of states that the system might reach. The remaining four articles focus on the problem of generating correct-by-construction control for a robot or team of robots such that the robot is guaranteed to achieve a high-level, abstract behavior. These articles focus on the use of linear temporal logic (LTL) as the specification formalism although other formalisms are used in the field as well.