Control design of discrete-time unicycle model using satisfiability modulo theory

This paper discusses a formal control design of a discrete-time unicycle model using Satisfiability Modulo Theory (SMT). Given a set of possible initial positions, a set of possible target positions, a lane and a time horizon, we develop a method to formally synthesize a controller that drives the unicycle from a starting position to a target position within the given time horizon, while staying in the lane. The method encodes the set of possible initial positions, the set of possible target positions, the lane and the discrete-time unicycle model into linear real arithmetic expressions, and then checking the satisfaction via an SMT solver. If a solution exists, then the solution represents the controller. Finally, the proposed method is applied to a case study.