Trajectory-based formal controller synthesis for multi-link robots with elastic joints

Multi-link robots with elastic joints are receiving a lot of interest because neglecting joint flexibility introduced in industrial robots due to presence of transmission elements results in poor control performances. Robots with elastic joints also play a pivotal role in making human-robot interaction more safe. In this paper, we discuss the problem of synthesizing provably correct controller for motion control of such robot in the presence of obstacles in the work space. For robots with multiple links, such task is difficult because the configuration space is high-dimensional. For example, for a robot with N links, the dimension of the configuration space is 2N, and the dimension of the state-space is 4N. To solve this problem, we built upon our previous results on trajectory-based formal controller synthesis for nonlinear systems. In this paper, we exploit the fact that the dynamics of the robot is feedback linearizable. We can then demonstrate that a provably correct controller for the robot can be obtained by using finitely many samples of valid execution trajectories. We demonstrate the validity of our results by simulating it on a multi-link robot.