Case Studies: Symbolic control goes real time
A well-known approach to synthesize controllers enforcing such complex specifications is based on so-called symbolic models (a.k.a. discrete abstractions). A given plant (i.e. a physical process described by a set of differential equations) is approximated by a symbolic model, i.e., a system with finite state and input sets. As the model is finite, algorithmic techniques from computer science are applicable to automatically synthesize discrete controllers enforcing complex logic specifications over symbolic models. Finally, those discrete controllers (a.k.a. symbolic controllers) can be refined to hybrid ones enforcing the same properties over original concrete systems.
The kernel pFaces-SymbolicControl runs on pFaces to synthesize, automatically, correct-by-construction embedded control software for dynamical systems. They implemented novel parallel algorithms to accelerate one common technique of symbolic control.
In the the next video, we present a demo where the tool pFaces-SymbolicControl is used to drive, autonomously, a car in the high way. In the first video, the car should keep the lane and provide and adaptive cruise control behaviour. pFaces-SymbolicControl is used here as an online synthesis engine. A simulator (namely Udacity self-driving vehicle simulator) is used to simulate and visualize the vehicle.
In this second video, we switch on the smart cruise control feature. This allows the vehicle to automatically move to a free lane if the current lane is blocked.
A glue code is developed to collect the car state and sensor data and send them to pFaces. pFaces then synthesizes a formally-verified controller that works within one second. The glue code keeps monitoring the real-time behavior snd synchronizing between pFaces and the simulator.
Used HW: Apple MacBook pro 2018 15" (Intel Core i9 CPU / AMD Vega 20 GPU).
In this case study, we deployed pFaces-SymbolicControl on the Amazon AWS as controller synthesis service.
Here we are showing a fleet of trucks that keep asking the online service for best control strategies. The service synthesizes controllers based on the truck situation and replies with a strategy in real-time.
Used HW: instances from Amazon AWS Cloud-computing
More case studies and complete benchmarks can be found in the following papers of the tool:
- Mahmoud Khaled and Majid Zamani. pFaces: An Acceleration Ecosystem for Symbolic Control. HSCC 2019
- Mahmoud Khaled, Eric S Kim, Murat Arcak, and Majid Zamani. Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach. TACAS 2019.