Verification and synthesis of cyber physical systems with machine learning and constraint-solver-driven learning

A computer program product comprising:

• a computer readable storage medium readable by one or more processors and storing instructions for execution by the one or more processors for performing a method comprising:
• generating, by the one or more processors, input-output pairs, to form a training set for machine learning based on obtaining data from sensing capabilities of a cyber physical system, via communication capabilities of the cyber physical system;
• generating, by the one or more processors, a machine learning model of the cyber physical system comprising objective functions, wherein the generating comprises utilizing a machine learning algorithm and the training set to train the machine learning model, and wherein the cyber physical system comprises one or more physical devices with integrated networking capabilities, the communication capabilities, the sensing capabilities, computation capabilities, and control capabilities;
• converting, by the one or more processors, the trained machine learning model into an equivalent constraint, wherein the trained machine learning model comprises a neural network and the converting comprises compressing the neural network into the equivalent constraint, wherein the equivalent constraint comprises a mixed integer linear program (MILP);
• optimizing, by the one or more processors, the objective functions subject to the constraint, wherein the optimizing comprises utilizing one or more constraint solvers to compute an input-output pair;
• determining, by the one or more processors, that the computed input-output pair is not within a pre-defined error tolerance of an input-output pair produced by a cyber physical system evaluator;
• based on the determining that the computed input-output pair is not within the pre-defined error tolerance, iteratively repeating a process until reaching an iteration when the computed input-output pair is within the pre-defined tolerance or reaching a pre-determined number of times for training the cyber physical system, the process comprising, for each iteration:
• adding the computed input-output pair to the training set to generate new training instances for each of the objective functions;
• updating, by the one or more processors, the machine learning model of the cyber physical system, wherein the updating comprises utilizing the machine learning algorithm and the updated training set to re-train the machine learning model;
• converting, by the one or more processors, the re-trained machine learning model into the equivalent constraint;
• optimizing, by the one or more processors, objective functions subject to the constraint, wherein the optimizing comprises utilizing the one or more constraint solvers to compute a new input-output pair;
• and
• determining, by the one or more processors, if the computed new input-output pair is within the pre-defined error tolerance of an input-output pair produced by the cyber physical system evaluator;
• and
• based on reaching the iteration when the computed input-output pair is within the pre-defined tolerance, the method further comprises:
• utilizing the computed new input-output pair as the solution, wherein the utilizing comprises automatically maneuvering, via the control capabilities of the cyber physical system, the cyber physical system, according to a value of each value in the new input-output pair, wherein each value is a navigational value and one navigational value is a position changing maneuver in three-dimensional space.

A system comprising:

• one or more memories;
• one or more processors in communication with the one or more memories;
• program instructions executable by the one or more processors via the one or more memories to perform a method, the method comprising:
• generating, by the one or more processors, input-output pairs, to form a training set for machine learning based on obtaining data from sensing capabilities of a cyber physical system, via communication capabilities of the cyber physical system;
• generating, by the one or more processors, a machine learning model of the cyber physical system comprising objective functions, wherein the generating comprises utilizing a machine learning algorithm and the training set to train the machine learning model, and wherein the cyber physical system comprises one or more physical devices with integrated networking capabilities, the communication capabilities, the sensing capabilities, computation capabilities, and control capabilities;
• converting, by the one or more processors, the trained machine learning model into an equivalent constraint, wherein the trained machine learning model comprises a neural network and the converting comprises compressing the neural network into the equivalent constraint, wherein the equivalent constraint comprises a mixed integer linear program (MILP);
• optimizing, by the one or more processors, the objective functions subject to the constraint, wherein the optimizing comprises utilizing one or more constraint solvers to compute an input-output pair;
• determining, by the one or more processors, that the computed input-output pair is not within a pre-defined error tolerance of an input-output pair produced by a cyber physical system evaluator;
• based on the determining that the computed input-output pair is not within the pre-defined error tolerance, iteratively repeating a process until reaching an iteration when the computed input-output pair is within the pre-defined tolerance or reaching a pre-determined number of times for training the cyber physical system, the process comprising, for each iteration:
• adding the computed input-output pair to the training set to generate new training instances for each of the objective functions;
• updating, by the one or more processors, the machine learning model of the cyber physical system, wherein the updating comprises utilizing the machine learning algorithm and the updated training set to re-train the machine learning model;
• converting, by the one or more processors, the re-trained machine learning model into the equivalent constraint;
• optimizing, by the one or more processors, objective functions subject to the constraint, wherein the optimizing comprises utilizing the one or more constraint solvers to compute a new input-output pair;
• and
• determining, by the one or more processors, if the computed new input-output pair is within the pre-defined error tolerance of an input-output pair produced by the cyber physical system evaluator;
• and
• based on reaching the iteration when the computed input-output pair is within the pre-defined tolerance, the method further comprises:
• utilizing the computed new input-output pair as the solution, wherein the utilizing comprises automatically maneuvering, via the control capabilities of the cyber physical system, the cyber physical system, according to a value of each value in the new input-output pair, wherein each value is a navigational value and one navigational value is a position changing maneuver in three-dimensional space.