pFaces: An Acceleration Ecosystem for Formal Methods in Control

The correctness of control software in many safety-critical applications such as autonomous vehicles is crucial. Formal methods in control provide approaches for automated synthesis of correct-by-construction controllers for such critical systems. Unfortunately, in most of the approaches, the complexity of synthesizing such controllers grows exponentially in the number of state variables. On the other hand, if distributed implementations are considered, high-performance computing platforms such as Cloud computing and super computers, can be leveraged to mitigate the effects of the state-explosion problem.

pFaces was proposed as an extensible software-ecosystem, to accelerate the techniques of formal methods in control. It facilitates designing parallel algorithms and supervises their executions to utilize available computing resources.

More details about pFaces can be found on its official page here.

Tools that use pFaces

The following tools use pFaces to accelerate their execution:

AMYTISS: A tool for parallel automated controller synthesis for large-scale stochastic systems.
PIRK: A tool for parallel computation of reachable sets for general nonlinear systems.

Download

pFaces is free to download and use with a demo license. You can download it from its GitHub repository. For researches, there exist academic license that extend the functionality of pFaces. Contact Mahmoud Khaled to request an academic license if you are interested.

Tool paper and related works

M. Khaled, and M. Zamani. pFaces: An Acceleration Ecosystem for Symbolic Control. 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2019), April 16-18, 2019, Montreal, Canada.
M. Khaled, E. S. Kim, M. Arcak, M. Zamani. Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). ETAPS 2019: 6-11 April, 2019, Prague, Czech Republic.
M. Khaled and M. Zamani. Distributed Automated Synthesis Of Correct-by-construction Controllers. European Patent Office. April 2020. EPO Publication.
A. Lavei, M. Khaled, S. Soudjani, M. Zamani. AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems. 32nd Conference on Computer Aided Verification (CAV), July 2020.
A. Devonport$, M. Khaled, M. Arcak, M. Zamani. PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems. 32nd Conference on Computer Aided Verification (CAV), July 2020.

Support

Please report any problems/bugs you face while installing and running pFaces to Mahmoud Khaled.