Case Studies

Here we present results on using SCOTS to synthesize symbolic controllers for various case studies. Some case studies include implementation of the synthesized controller.

Synthesizing and Implementing a Symbolic Controller for the Khepera-IV mobile robot

In this case study, we present details about using SCOTS to synthesize a symbolic controller for the Khepera-IV mobile robot. A mathematical model of the robot is presented as differential equations and they are used by SCOTS to derive an abstract model. The abstract model is used for controller synthesis while aiming at enforcing specifications like reachability and recurrence. The generated symbolic controller is then implemented within the mobile robot.