Distributed automated synthesis of correct-by-construction controllers

A computer program comprising computer-readable instructions, wherein the instructions, when executed by a computer device, cause the computer device to implement a method for synthesizing a correct-by-construction controller for a control system by:

• receiving a mathematical model of the control system with a plurality of state variables {right arrow over (x)} and a plurality of control parameters {right arrow over (u)} wherein the mathematical model characterizes at least in part the change of the state variables {right arrow over (x)} in response to the control parameters {right arrow over (u)} as a control input;
• receiving at least one specification for one or both of the state variables {right arrow over (x)} and the control parameters {right arrow over (u)};
• identifying available processing elements;
• discretizing at least a part of a space spanned by ({right arrow over (x)}, {right arrow over (u)}) to obtain a set of tuples ({right arrow over (x)}i, {right arrow over (u)}j), where i and j are indices labelling the state vectors and control vectors, respectively;
• determining, based on the mathematical model, for each tuple ({right arrow over (x)}i, {right arrow over (u)}j) in the set of tuples at least one successor state {right arrow over (x)}f;
• obtaining an initial winning set of tuples based on the at least one specification;
• determining an updated winning set of tuples, wherein the determination comprises:
• comparing the at least one successor state {right arrow over (x)}f of each tuple with the initial winning set of tuples, wherein the 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;
• receiving information pertaining the comparison from the available processing elements;
• and
• determining the updated winning set of tuples based on the information;
• comparing the updated winning set with the initial winning set to obtain a convergence measure;
• repeating the determination of the updated winning set of tuples to obtain a new updated winning set of tuples if the convergence measure does not meet a predefined convergence criterion, wherein the previous updated winning set of tuples is used as the initial winning set for the determination and is provided at least in part to the available processing elements;
• and
• constructing a controller for the control system from the new updated winning set.

A device for synthesizing a correct-by-construction controller for a control system, wherein the device comprises:

• at least two processing elements;
• a computing platform interface coupled to the at least two processing elements for exchanging data with the at least two processing elements;
• a resource identification unit coupled to the computing platform interface for identifying available processing elements of the at least two processing elements;
• an interface unit for:
• receiving a mathematical model of the control system with a plurality of state variables {right arrow over (x)} and a plurality of control parameters {right arrow over (u)}, wherein the mathematical model characterizes at least in part the change of the state variables {right arrow over (x)} in response to the control parameters {right arrow over (u)} as a control input,
• receiving at least one specification for one or both of the state variables {right arrow over (x)} and the control parameters {right arrow over (u)}, and
• providing the synthesized controller;
• a management engine coupled to the resource identification unit and the interface unit;
• and
• a task scheduling unit coupled to the computing platform interface and the management engine, wherein the device is configured to execute a method for synthesizing a correct-by-construction controller for a control system by:
• receiving the mathematical model of the control system and the at least one specification;
• identifying the available processing elements;
• discretizing at least a part of a space spanned by ({right arrow over (x)}, {right arrow over (u)}) to obtain a set of tuples ({right arrow over (x)}i, {right arrow over (u)}j), where i and j are indices labelling the state vectors and control vectors, respectively;
• determining, based on the mathematical model, for each tuple ({right arrow over (x)}i, {right arrow over (u)}j) in the set of tuples at least one successor state {right arrow over (x)}f;
• obtaining an initial winning set of tuples based on the at least one specification;
• determining an updated winning set of tuples, wherein the determination comprises:
• comparing the at least one successor state {right arrow over (x)}f of each tuple with the initial winning set of tuples, wherein the management engine is configured to determine a distribution over the available processing elements for the comparison by choosing one processing element from the available processing elements for each tuple to perform the comparison and wherein the management engine is further configured to determine corresponding queues of tasks for execution on the available processing elements, the task scheduling unit being configured to receive the queues of tasks from the management engine and to manage the execution of the queues of tasks on the available processing elements, wherein the available processing elements are used simultaneously at least in part;
• receiving information pertaining the comparison from the available processing elements;
• and
• determining the updated winning set of tuples based on the information;
• comparing the updated winning set with the initial winning set to obtain a convergence measure;
• repeating the determination of the updated winning set of tuples to obtain a new updated winning set of tuples if the convergence measure does not meet a predefined convergence criterion, wherein the previous updated winning set of tuples is used as the initial winning set for the determination and is provided at least in part to the available processing elements;
• and
• constructing the controller for the control system from the new updated winning set.