Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the control-D system

Abstract

This dissertation studies the semi-automated synthesis and verification of control systems for robotics and manufacturing devices using formal methods in a discrete framework, and bears some resemblance to the theory of controlled discrete event systems (CDES) of Ramadge and Wonham. The discrete controller components of a walking machine and of a manufacturing line in the Combat Ration Advanced Manufacturing Technology Demonstration (CRAMTD) of Rutgers University are constructed automatically using the algorithms developed here. The goal of this research has been to facilitate the integration of CDES theory with the the specification and verification formalisms for finite state systems. Many of our techniques rely on the application of some flavor of temporal logic. In particular, the model-checking techniques of Clarke and Emerson, for branching time temporal logic, proved to be valuable in the implementation of a controller synthesis tool for CDES, called Control-D. The main synthesis algorithm used by the Control-D tool compares favorably with the Ramadge-Wonham algorithm in time and space complexity, while achieving improved expressiveness in its underlying specification language.