Physical systems that can operate reliably and autonomously are increasingly becoming available. A variety of such systems are used in safety-critical scenarios and errors in their design can lead to catastrophic failures. Hence, it is of utmost importance to ensure that the designed systems satisfy their specifications. In this talk, we discuss algorithmic techniques that can help us build systems with formal guarantees on their behavior. We use safety analysis of physical systems and robot motion planning with complex goals as motivating problems. Recent research has shown that solving these problems is computationally hard, and furthermore, even approximating their solutions is hard.
The first part of this talk describes a robotics-inspired approach for safety analysis of systems driven by exogenous inputs. Instead of trying to prove that a given system always behaves safely, the proposed approach explores the state-space incrementally to find a feasible and unsafe state. For the case when the system can never reach an unsafe state, the approach returns a safety certificate. The certificate guarantees safety of the system for a subset of inputs. The second part of the talk addresses the scalability challenge in solving a class of motion planning problems. The problem instances involve nonlinear (possibly hybrid) robot models, complex workspace environments, and temporal goals. We show how a combination of geometry and discrete and continuous search techniques can be used to solve these problems efficiently. Experimental results on benchmark problems indicate that using geometry yields an order of magnitude improvement in overall performance compared to alternate approaches.