EXPERIMENTAL EVALUATION OF METHODS OF REACHABLE SET COMUTATION CONTEXT OF SYMBOLIC CONTROLLER SYNTHESIS

Abstract

The design of hardware and software for safety critical applications often involves use of formal veri cation techniques to ensure correctness of implementation. If speci cation fails to satisfy then the cycle of design and veri cation needs to be repeated. Lengthy and costly design process can be avoided by the use of automated controller synthesis techniques which can provide correct-by-construction controller that enforces the desired formal speci cation on the given system. Use of synthesis techniques with continuous systems require construction of a symbolic model which in turn require computation of reachable sets. The set of states that can be attained by a system for given values of initial state, input and time horizon is referred to as reachable state set. As reachable sets are in nite objects their exact computation is di cult, thus their overapproximations are usually computed whose accuracy a ects the computation time and size of the synthesized controller. The choice of set representation also plays an important role in accuracy of approximation and time requirement. We used zonotopes which are centrally symmetric convex polytopes and are closed under linear transformation and Minkowski sum. After a short introduction to the process of symbolic model construction we discuss three methods of reachable set computation for nonlinear control systems. These are then used together with SCOTS, which is a tool for symbolic controller synthesis, to synthesize controllers for reachability and invariance speci cations on four examples