DISTRIBUTED AUTOMATED SYNTHESIS OF CORRECT-BY-CONSTRUCTION CONTROLLERS

摘要

Disclosed herein is a method for synthesizing a correct-by-construction controller for a control system, the method comprising the following steps: receiving a mathematical model of the control system, with a plurality of state variables x and a plurality of control parameters u, discretizing at least a part of a space spanned by (x, u) to obtain a set of tuples (x_i, u_j), determining, based on the mathematical model, for each tuple (x_i,u_j) in the set of tuples at least one successor state x_f; obtaining an initial winning set of tuples based on said at least one specification; determining an updated winning set of tuples, including comparing the at least one successor state x_f of each tuple with the initial winning set of tuples, wherein said comparison is distributed over the available processing elements by choosing one processing element from the available processing elements for each tuple to perform the comparison and wherein the available processing elements are used simultaneously at least in part; repeating said determination of the updated winning set of tuples to obtain a new updated winning set of tuples if a convergence measure does not meet a predefined convergence criterion, and constructing a controller for the control system from said new updated winning set.