Distributed automated synthesis of correct-by-construction controllers

Abstract

A method includes: receiving a mathematical model of a control system, with state variables and control parameters; discretizing at least a part of a space to obtain a set of tuples; determining for each tuple at least one successor state; obtaining an initial winning set of tuples; determining an updated winning set of tuples, including comparing the at least one successor state with the initial winning set of tuples, where the comparison is distributed over available processing elements by choosing one processing element from the available processing elements for each tuple to perform the comparison and where the available processing elements are used simultaneously at least in part; repeating the 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 criterion, and constructing a controller for the control system from the new updated winning set.

Claims

1. 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 {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/or 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)}.sub.i, {right arrow over (u)}.sub.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)}.sub.i, {right arrow over (u)}.sub.j) in the set of tuples at least one successor state {right arrow over (x)}.sub.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)}.sub.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.

2. The method according to claim 1, wherein the determination of the successor states is distributed over the available processing elements by choosing one processing element from the available processing elements for each tuple to determine {right arrow over (x)}.sub.f and the available processing elements are used simultaneously at least in part for the determination of the successor states.

3. The method according to claim 1, wherein identifying the available processing elements comprises determining a type of processing element for each available processing element, and wherein the comparison of the successor states with the initial winning set is adapted to the type of processing element for each available processing element.

4. The method according to claim 3, wherein the distribution over the available processing elements for the comparison of the successor states with the initial winning set is determined based on the types of the available processing elements, an available computing power of the available processing elements, available memory resources of the available processing elements, or a combination thereof.

5. The method according to claim 1, wherein the distribution over the available processing elements for the comparison of the successor states with the initial winning set is determined taking into account a communication overhead for exchanging data with the available processing elements.

6. The method according to claim 1, wherein the determination of the updated winning set of tuples to obtain a new updated winning set of tuples is repeated until the convergence measure obtained by comparing the new updated winning set with the previous updated winning set meets the predefined convergence criterion.

7. The method according to claim 1, wherein constructing the controller comprises: constructing a symbolic controller from the new updated winning set of tuples, and refining the symbolic controller to obtain the controller.

8. The method according to claim 1, wherein determining the at least one successor state {right arrow over (x)}.sub.f comprises determining an upper and lower bound for a set of successor states.

9. The method according to claim 1, wherein the discretization of at least a part of the space spanned by ({right arrow over (x)}, {right arrow over (u)}) comprises mapping the part of the space spanned by ({right arrow over (x)}, {right arrow over (u)}) to a lower-dimensional space.

10. The method according to claim 1, wherein the discretization of at least a part of the space spanned by ({right arrow over (x)}, {right arrow over (u)}) is determined based on one or more of the mathematical model, the at least one specification, and information pertaining the available processing elements.

11. The method according to claim 1, wherein the mathematical model comprises a system of differential equations and determining the successor states {right arrow over (x)}.sub.f comprises numerically solving the system of differential equations at least in part.

12. The method according to claim 1, wherein comparing the at least one successor state {right arrow over (x)}.sub.f of each tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) with the initial winning set of tuples comprises determining for at least one of the at least one successor state of the tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) whether the initial winning set contains at least one tuple ({right arrow over (x)}.sub.k, {right arrow over (u)}.sub.i) with {right arrow over (x)}.sub.k={right arrow over (x)}.sub.f, where k and l are indices labelling the state vectors and control vectors, respectively, and wherein the updated winning set contains all tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) with successor states {right arrow over (x)}.sub.f for which the initial winning set contains the tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) and contains at least one tuple ({right arrow over (x)}.sub.k, {right arrow over (u)}.sub.i) with {right arrow over (x)}.sub.k={right arrow over (x)}.sub.f for each of the at least one successor state of the tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j).

13. The method according to claim 1, wherein the convergence measure quantifies the overlap of the updated winning set with the initial winning set and the predefined convergence criterion specifies a minimum absolute or relative overlap.

14. The method according to claim 1, wherein the control system is a computer-controlled physical system, and wherein at least one of the state variables characterizes a position or velocity of a mechanical element of the control system.

15. The method according to claim 1, wherein the method is performed in real time during operation of the control system, and wherein the method is performed repeatedly with a fixed frequency or whenever updated specifications are provided or whenever the state of the control system has changed.

16. 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)}.sub.i, {right arrow over (u)}.sub.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)}.sub.i, {right arrow over (u)}.sub.j) in the set of tuples at least one successor state {right arrow over (x)}.sub.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)}.sub.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.

17. 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)}.sub.i, {right arrow over (u)}.sub.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)}.sub.i, {right arrow over (u)}.sub.j) in the set of tuples at least one successor state {right arrow over (x)}.sub.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)}.sub.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.

18. The device according to claim 17, wherein the management engine is further configured to determine a distribution over the available processing elements for the determination of the successor states and to determine corresponding queues of tasks for execution on the available processing elements.

19. The device according to claim 17, wherein the resource identification unit is configured to determine a computing power of the available processing elements by executing tasks associated with one or both of the determination of the successor states and the comparison of the successor states with the initial winning set on the available processing elements.

20. The device according to claim 17, wherein the interface unit is configured to receive the mathematical model of the control system and the at least one specification and to provide the synthesized controller via a computer network.

Description

BRIEF DESCRIPTION OF THE SEVERAL VIEWS OF THE DRAWINGS

(1) In the following, a detailed description of the invention and exemplary embodiments thereof is given with reference to the figures. The figures show schematic illustrations of

(2) FIG. 1: a symbolic controller synthesis method according to prior art

(3) FIG. 2a: a device for synthesizing a correct-by-construction controller according to an exemplary embodiment of the invention

(4) FIG. 2b: a flow chart of a method to synthesize a correct-by-construction controller in accordance with an embodiment of the invention

(5) FIG. 3: a flow chart of a method to identify available processing elements according to an embodiment of the invention

(6) FIG. 4a: a flow chart of a method for a parallel determination of a symbolic model in accordance with an embodiment of the invention

(7) FIG. 4b: a parallel determination of a symbolic model according to an embodiment of the invention

(8) FIG. 5a: a flow chart of a method for a parallel determination of an updated winning set in accordance with an embodiment of the invention

(9) FIG. 5b: a parallel determination of an updated winning set according to an embodiment of the invention

DETAILED DESCRIPTION

(10) FIG. 1 schematically illustrates the concept of symbolic controller synthesis as known from prior art. The aim is to design a controller 10 for a control system 12, wherein the controller 10 comprises a set of rules to be executed by a control unit. The current state of the control system 12 is characterized by a plurality of state variables x.sup.(1), x.sup.(2), . . . , x.sup.(n) and can be described by a state vector {right arrow over (x)} containing all of the state variables. The control system 12 has a number of control parameters u.sup.(1), u.sup.(2), . . . , u.sup.(m), which can be used to control the state of the control system 12 and are described by a control vector {right arrow over (u)} containing the control parameters. The set of rules of the controller 10 relate a state vector {right arrow over (x)} a control vector {right arrow over (u)}.

(11) The control system 12 can for example be an automated physical system like an autonomous car. In this case, the state variables could be the position and velocity of the car and the control parameters could be the position of the throttle and the angle of the steering wheel. In the following, an autonomous car is often used as an example for illustration. However, this should not in any sense be understood as a limitation for the subject-matter of the invention, which relates to the synthesis of controllers for technical control systems of any kind. Such control systems could for example be other automated physical systems like robots or cyber-physical systems like smart homes, smart grids or industrial process control systems.

(12) The control unit receives the current state {right arrow over (x)} of the control system 12 as well as a set of specifications for the control system 12 describing a target state of the control system 12 and possibly a set of boundary conditions. In the case of an autonomous car, the target state could for example by a target position and the boundary conditions could be the speed limit and the boundaries of the road. Based on the specifications, the controller 10 should determine a set of control parameters {right arrow over (u)} to meet the specifications, i.e., to reach the target state under the imposed boundary conditions. A car could for example be accelerated to reach a certain target velocity by changing the position of the throttle or the car's steering wheel could be controlled to autonomously reach a pre-defined target position, e.g., some coordinates specified by a passenger using a navigator device.

(13) The response of the control system 12 in a given state {right arrow over (x)} to the control input {right arrow over (u)} can be described by a mathematical model, which relates the change in the state {right arrow over (x)} to the current state {right arrow over (x)} and the control input {right arrow over (u)}. This mathematical model can for example be a set of differential equations
{dot over ({right arrow over (x)})}=f({right arrow over (x)},{right arrow over (u)})
The mathematical model forms the basis for designing the controller 10. To obtain a suitable controller 10, the mathematical model has to capture the essential dynamics of the control system 12 at least approximately. Depending on the complexity of the control system 12, obtaining a suitable model may be a difficult task on its own.

(14) In symbolic controller synthesis, a controller 10 is constructed in three steps, which are illustrated in FIG. 1 and detailed in the following: (1) finite abstraction of the mathematical model to obtain a symbolic model 14, (2) synthesis of a symbolic controller 18 based on the symbolic model 14 and the set of specifications 16, and (3) refinement of the symbolic controller 18 to obtain a refined controller 20 for the actual control system 12.

(15) In the first step, the continuous space spanned by the state variables {right arrow over (x)} and the control parameters {right arrow over (u)} is discretized to obtain a discrete space comprising a set of tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j), where i and j are indices labelling the state vectors and control vectors, respectively. Subsequently, a successor state {right arrow over (x)}.sub.f is determined for each tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) using the mathematical model, wherein {right arrow over (x)}.sub.f corresponds to the state that the control system 12 is expected to end up in if it is initially in state {right arrow over (x)}.sub.i and the control input {right arrow over (u)}.sub.j is applied for a predefined amount of time. Obtaining the successor state may involve solving the mathematical model exactly or numerically. The resulting symbolic model 14 thus consists of a plurality of transition rules associating each tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) to a successor state {right arrow over (x)}.sub.f. In FIG. 1, the higher-dimensional discrete space is illustrated by mapping it to a flat 2D space using the indices i and j as coordinates such that a tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) corresponds to the square at position (i,j). Accordingly, the transition rules are depicted as horizontal arrows linking a tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) with the tuple ({right arrow over (x)}.sub.f, {right arrow over (u)}.sub.j) corresponding to the successor state {right arrow over (x)}.sub.f at the same control vector {right arrow over (u)}.sub.j. For clarity, the transition rules are shown only for a select subset of tuples.

(16) In the following step, a symbolic controller 18 is synthesized based on the symbolic model 14 and the specifications 16 for the control system 12. This synthesis is conducted in such a way that the symbolic controller 18 automatically meets the specifications 16 when applied to the symbolic model 14. The resulting symbolic controller 18 is hence “correct-by-construction”. As detailed below, this can for example be achieved by an iterative determination of a final winning set of tuples that forms a fixed-point set with respect to one or more target states, i.e., when applying a feedback based on the final winning set to the control system 12, the control system 12 will remain within the final winning set and will eventually converge towards the target states.

(17) At first, an initial winning set is defined, which can, e.g., be the target states. This winning set is then updated iteratively, wherein each iteration comprises the following steps: The successor states for all tuples in the discrete space are obtained from the symbolic model 14. For each tuple, the successor state is compared to the initial winning set and based on this comparison an updated winning set is defined. For example, each tuple with a successor state {right arrow over (x)}.sub.f, for which the initial winning set contains a tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) with {right arrow over (x)}.sub.i={right arrow over (x)}.sub.f, can be added to the updated winning set, whereas tuples for which the aforementioned condition is not met are not contained in the updated winning set. Alternatively, the updated winning set could only contain tuples that meet the aforementioned condition and are from the initial winning set. Afterwards, the initial winning set and the updated winning set are compared to obtain a convergence measure, e.g., an overlap between the sets, and by comparing this convergence measure with a convergence criterion a decision is made whether to perform another iteration or to terminate the iterative determination. Before beginning with the next iteration, the initial winning set is redefined by replacing it with the updated winning set. In this way, the initial winning set can change from iteration to iteration, wherein new tuples may enter the set and/or other tuples previously contained in the set may leave the set.

(18) The convergence criterion can be chosen such that it ensures that the final updated winning set, also referred to as final winning set, forms a fixed-point set as defined above. The convergence criterion can be the equivalence between the initial and the updated winning sets, i.e., the iteration can be continued until the initial winning set and the updated winning set are identical. For example, when using the aforementioned condition to determine the updated winning set, this would be the case when for each tuple in the initial winning set a tuple exists in the initial winning set for which the state vector is identical to the successor state of the former.

(19) This facilitates the generation of the symbolic controller 18, which comprises a set of rules that identify a control vector for a given state vector, {right arrow over (x)}.sub.i.fwdarw.{right arrow over (u)}.sub.j. These rules can be obtained from the final updated winning set, e.g., by averaging u over all tuples in the final updated winning set with a given {right arrow over (x)}.sub.i or randomly selecting a tuple from the tuples in the final updated winning set with a given {right arrow over (x)}.sub.i. By construction, this symbolic controller 18 will enforce the specifications 16 provided initially in a discrete control system whose dynamics are governed by the symbolic model 14.

(20) Finally, the symbolic controller 18 is refined to obtain a refined controller 20 for the actual control system 12, i.e., a controller capable of handling state vectors from the continuous state space. This refinement can involve an interpolation and/or extrapolation process to extract rules that can be applied to a continuous state vector from the discrete set of rules of the symbolic controller 18. These rules can for example comprise a mathematical function mapping a state vector {right arrow over (x)} to a control vector {right arrow over (u)}({right arrow over (x)}). The refined controller 20 is then designed such that it provides a control vector to the control system 12 according to these rules in response to a state vector as an input. Alternatively, the refined controller 20 could approximate a continuous state vector by a discrete state vector contained in the discrete state space and use the rules of the symbolic controller 18 as a look-up table.

(21) FIG. 2a shows an example for a device 100 according to an embodiment of the present invention, which can be used to implement a method as depicted in FIG. 2b. The device 100 comprises a central processing unit (CPU) 102 with a processing element 104, a graphics processing unit (GPU) 106 with a two processing elements 108, 110 as well as a hardware accelerator (HWA) 112 with a processing element 114. Each of the processing elements 104, 108, 110 and 114 can have a memory resource associated therewith. Alternatively or additionally, processing elements within the same computation device, e.g., processing elements 108 and 110, may share a common memory resource. With a variety of processing elements at hand, the device 100 is capable of matching the requirements of various applications by distributing tasks over the processing elements 104, 108, 110, and 114. CPUs, for example, are suitable for complex serial mathematical computations, which may arise when constructing the symbolic model, e.g., for solving differential equations numerically. GPUs, on the other hand, typically contain many, but less-powerful processing elements and are thus particularly well suited for a massive parallelization of tasks, e.g., for computing the updated winning set. HWAs, e.g., an FPGA, can operate in a low-power mode, which may be advantageous for embedded applications that require real-time execution of the provided method.

(22) The processing elements 104, 108, 110 and 114 are coupled to a computing platform interface 116, which handles the exchange of data between the processing elements 104, 108, 110 and 114 and components connected with the computing platform interface 116. Data may be exchanged between the processing elements 104, 108, 110 and 114 themselves as well as between each of the processing elements 104, 108, 110 and 114 and each of the components connected with the computing platform interface 116. Additionally, processing elements within the same computation device, e.g., processing elements 108 and 110, may be configured to exchange data with each other independent of the computing platform interface 116.

(23) In the example shown in FIG. 2a, a resource identification unit 118 and a task scheduling unit 120 are coupled to the computing platform interface 116. The resource identification unit 118 is configured to identify available processing elements that can be used at least in part for the execution of tasks associated with the method according to the invention. Additionally, the resource identification unit 118 is configured to determine the type of processing element for the available processing elements, i.e., which kind of computation device the respective processing element belongs to, e.g., CPU, GPU or a type of HWA. The resource identification unit 118 may further be configured to obtain information regarding the available computing power and/or memory resources of each of the available processing elements as detailed below.

(24) The device 100 further comprises an interface unit 122 for communication with other devices, in particular to receive the specifications 240 and the mathematical model of the control system 12 for which a controller is to be synthesized and to provide the synthesized controller. For this, the interface unit 122 may be configured to communicate via wired connections, e.g., CAN, LAN or USB, and/or via wireless connections like WLAN. The interface unit 122 may be directly connected to the control unit of the control system 12. Alternatively or additionally, the interface unit 122 may be connected to another device, e.g., a computer, and/or comprise means for direct access by a user.

(25) The core part of the device 100 is the management engine 124, which is coupled to the interface unit 122, the resource identification unit 118 and the task scheduling unit 120. The management engine 124 is configured to execute the method according to the invention, in particular to determine the distribution of tasks for the associated computations as described below in detail.

(26) To perform these tasks, the device 100 comprises a task scheduling unit 120, which receives queues of tasks for execution on the available processing elements, manages the execution of these queues and collects results from the available processing elements. The task scheduling unit 120 handles the exchange of data between processing elements 104, 108, 110, 114 via the computing platform interface 116 as required for the task execution.

(27) The device 100 can further contain a logging unit 126 for storing and providing data, e.g., information on the controller synthesis acquired during execution of the method according to the invention, which may be used for debugging. For this, the logging unit 126 is coupled to the management engine 124.

(28) The device 100 depicted in FIG. 2a only constitutes one example for an embodiment of the present invention and a variety of modifications are possible in other examples. The number of processing elements and computation devices can be different and in particular much larger than shown in FIG. 2a. A device according to the present invention may contain multiple computing devices of the same type. Furthermore, two or more of the components could be formed by a single unit providing the respective functionalities.

(29) FIG. 2b depicts a flow diagram representing a method according to an embodiment of the present invention for synthesizing a correct-by-construction controller 20 for a control system 12, which could for example be implemented with device 100.

(30) In a first step 130, a mathematical model of the control system 12 is received, which characterizes the response of the control system 12 to a given control vector {right arrow over (u)}, i.e., the change of the current state {right arrow over (x)} as a result of the control input. The mathematical model can characterize the response exactly or approximately. As described above, the mathematical model can for example be a set of differential equations describing the dynamics of the control system 12. Alternatively, the mathematical model may comprise information based on which a response of the control system 12 can be determined, e.g., a Hamiltonian or Lagrangian or a set of intrinsic parameters of the control system 12.

(31) The first step 130 further comprises receiving at least one specification for the state variables and/or the control vector. This specification can for example be one or more target states or a range of target states, which the control system 12 should reach or remain in, e.g., a certain position or velocity for an autonomous car. The specification may be given as formulae in a certain specification modeling language, e.g., linear temporal logic (LTL) formulae or automata on infinite strings. The formulae can then be translated to a corresponding set of states or tuples. The specifications may contain conditions to be imposed on the control parameters, e.g., boundaries like a maximum angle for the steering wheel or a maximum position of the throttle to limit the acceleration. Additionally, a priority may be assigned to the specifications. For example, a speed limit may be required to be strictly enforced, whereas comfort settings like the maximum throttle position can have a lower priority.

(32) Subsequently, the method proceeds with step 132, in which available processing elements are identified that can be used for executing computations. The step 132 is described in more detail below with reference to FIG. 3.

(33) Afterwards, the continuous state space containing all possible state vectors and the continuous input space spanned by the input vectors u are discretized at least in part to obtain a set of tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j), for which a symbolic model 190 and a symbolic controller is to be determined. For this, a subspace of the continuous state space and a subspace of the continuous input space are selected, wherein each subspace may contain an arbitrary part of the respective space or the entire respective space. The tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) are chosen from the combination of the subspaces, e.g., using a periodic pattern with a fixed spacing. The subspaces to be discretized as well as the spacings used for the discretization may be chosen based on the provided specifications, the available processing elements, the mathematical model and/or additional information on the control system 12. For example the chosen state subspace may be required to contain the target state as well as the current state. The size of the subspaces to be discretized may be limited based on properties of the control system 12, e.g., the range for the velocity of a car may be bounded by the maximum velocity of the car or the range for the position of a car may depend on the area covered by the sensors observing the surroundings of the car. The size of the subspaces and the spacings can be chosen depending on the available computing power and/or memory resources. Furthermore, the spacing can be non-uniform and can account for properties of the mathematical model, e.g., the spacing for a control parameter may be closer in regions where the state of the control system 12 depends strongly on this parameter or the spacing for a state variable may be closer in a region where the mathematical model exhibits particular features. In the case of an autonomous car, this can for example be a region in which a pedestrian or a parked car was detected.

(34) Following the discretization, a symbolic model 190 is determined for the set 180 of tuples by a parallel computation assigning at least one successor state to each tuple based on the mathematical model as detailed below with reference to FIG. 4.

(35) In step 138, an initial winning set 230 of tuples is determined based on the at least one specification for the state variables and/or the control vector. This initial winning set 230 can for example contain some or all of the tuples from the set 180 of tuples that meet one or more of the specifications, e.g., all tuples corresponding to a target position for a car or to a velocity range specified for a car.

(36) Subsequently, an updated winning set 242 of tuples is obtained through a parallelized comparison of the successor states determined in step 140 with the initial winning set 230 of tuples. The step 140 is illustrated in FIG. 5 and described in more detail below.

(37) After determining the updated winning set 242, the updated winning set 242 and the initial winning set 230 are compared with each other in step 142. From this comparison, a convergence measure is obtained, which quantifies the overlap between the two sets. This convergence measure can for example be the number or fraction of tuples that are only contained in one of the sets. This convergence measure is then compared to a predefined convergence criterion, which specifies a desired degree of similarity between the initial winning set 230 and the updated winning set 242. The convergence criterion may for example require that the two sets are identical or that the fraction of tuples which only appear in one of the sets is smaller than a certain threshold.

(38) If the convergence measure does not meet the convergence criterion, the method returns to step 138 to determine a new updated winning set. To this end, the initial winning set 230 is replaced by the updated winning set 242 before proceeding to step 140 for the determination of the new updated winning set as described below, i.e., the previously determined updated winning set 242 is used as the initial winning set 230 when repeating step 140. Step 140 then results in a new updated winning set that replaces the updated winning set 242. In this way, the updated winning set 242 is modified iteratively until the convergence criterion is fulfilled, yielding a final winning set 244, namely the latest new updated winning set.

(39) The same convergence criterion may be used for all iterations. Alternatively, the convergence criterion may be adapted between iterations, e.g., to ensure a completion of the method within a specified amount of time. For this, the convergence criterion can be modified depending on the number of performed iterations or a maximum number of iterations can be set.

(40) Once the convergence measure satisfies the convergence criterion in step 142, the method proceeds to step 144, where a controller for the control system 12 is constructed using the final winning set 244, which is collected from all processing elements participating in step (140). This controller is designed such that it determines a control vector {right arrow over (u)} as an output to be provided as a control input to the control system 12 in response to a state vector {right arrow over (x)} received from the control system 12. The rules associating a state vector to a control vector {right arrow over (u)} are determined based on the final winning set 244.

(41) The construction of the controller can comprise determining a symbolic controller from the final winning set 244 and refining the symbolic controller to obtain the controller for the control system 12. The construction of the symbolic controller involves extracting a set of rules which uniquely identify a control vector for a given state vector, {right arrow over (x)}.sub.i.fwdarw.{right arrow over (u)}.sub.j. This defines the output {right arrow over (u)}.sub.i that the controller will provide to the control system 12 when receiving the state vector {right arrow over (x)}.sub.ti as an input. The symbolic controller is restricted to the discretized space, i.e., the tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) has to be contained in the discretized space. Since the final winning set 244 may contain multiple tuples with the same state vector constructing the symbolic controller may require a determination step, wherein a unique control vector is associated with the state vector {right arrow over (x)}.sub.i. This can be achieved, e.g., by randomly selecting one of the multiple tuples with the state vector {right arrow over (x)}.sub.i or by averaging {right arrow over (u)}.sub.j over two or more of the multiple tuples. Alternatively, a tuple can be chosen based on the provided specifications. For this, the specifications may contain one or more secondary specifications which can, e.g., be additional criteria that are not to be enforced strictly, but that can be optimized for if possible. Such a secondary specification could for example be that the acceleration should be as small as possible to maximize comfort for a passenger in an autonomous vehicle. In this case, the tuple resulting in the smallest acceleration would be selected. If multiple secondary specifications are provided, priorities may be assigned to the secondary specifications for the determination step.

(42) The refinement of the symbolic controller comprises the determination of one or more rules associating a continuous state vector {right arrow over (x)} to a control vector {right arrow over (u)} to obtain a controller that is capable to process an input from the continuous state space. In one example, the rule could be to determine the discrete state vector {right arrow over (x)}.sub.i that is closest to the continuous state vector {right arrow over (x)} and to use the symbolic controller as a look-up table to obtain the corresponding discrete control vector {right arrow over (u)}.sub.i as the output control vector it. Alternatively, an average or weighted average of the {right arrow over (u)}.sub.i associated with a plurality of discrete state vectors that are close to {right arrow over (x)} may be used. In another example, an interpolation and/or extrapolation could be performed with the discrete set of rules of the symbolic controller to obtain a mathematical function mapping a state vector {right arrow over (x)} to a control vector {right arrow over (u)}({right arrow over (x)}).

(43) In addition to the determination of the rules associating a state vector {right arrow over (x)} to a control vector {right arrow over (u)}, the construction of the controller for the control system 12 can comprise generating source code that can be used to implement the controller in a control unit, in step 146. The control unit can be configured to execute the source code in order to determine a control vector for a state vector received, e.g., as a plurality of digital signals and/or analog signals and to send the control vector, e.g., as a plurality of digital signals and/or analog signals to a control system 12. The source code can be provided automatically to the control unit for implementation or can be provided to a software/hardware developer, e.g., as a source code building block.

(44) The sequence of the steps illustrated in FIG. 2b and described above is only one particular example. As far as technically feasible, the steps can be permuted and the method and any embodiment thereof can be performed in an arbitrary order. This also applies to the order of the substeps that the steps shown in FIG. 2b are comprised of as illustrated in FIG. 3 to FIG. 5 and described below.

(45) In FIG. 3, an exemplary method for the determination of available processing elements in step 132 is illustrated as a flowchart. The purpose of the step 132 is to identify the processing elements which can be used at least in part for the parallel computations in step 136 and/or step 140. Furthermore, additional information on the available processing elements may be obtained, which can be useful for determining the distribution of computation tasks over the available processing elements. In step 150, the processing elements in the system that the method according to the invention is executed on are analyzed to obtain a list of processing elements which are suitable for the executing the computation tasks and are currently available, e.g., have sufficient spare computation capacities to speed up the parallel computations given their current workload. For device 100, this list might for example contain the processing elements 104, 108, 110, and 114.

(46) Step 132 may comprise determining the type of processing elements for the available processing elements in step 152, i.e., what type of computation device they belong to. Processing element 104 would for example be identified as a CPU processing element, whereas processing element 110 would be identified as a GPU processing element. The step 152 may include obtaining further information on the processing elements, e.g., the type of CPU 102, GPU 106 or HWA 112 or specifications like the clock speed or the available memory resources.

(47) Subsequently, in step 154, based on the information about the available processing elements, customized kernels may be compiled for executing the computations on the available processing elements. These kernels can be fine-tuned to the respective type of processing element in order to optimize the computation performance, e.g., by adapting the computations to the parallel architecture of GPUs or exploiting the large cache memory of CPUs.

(48) In addition to the specifications of the available processing elements obtained in step 152, the actual computing power of the available processing elements may be determined in step 156, e.g., by executing some of the computations tasks for the determination of the symbolic model 190 in step 136 and/or for the determination of the updated winning set 242 in step 140 and measuring the elapsed time. This allows for more reliable estimates of the number of computation tasks a given processing element can execute in a certain amount of time and thus facilitates the efficient distribution of tasks for the parallel computations as described below.

(49) FIG. 4a depicts a flow chart of an example for the parallel determination of the symbolic model 190 in step 136, the basic concept of which is illustrated in FIG. 4b. In FIGS. 4a and 4b, it is assumed that four processing elements are used, e.g., the processing elements 104, 108, 110, and 114 in the device 100. This only constitutes one specific example and the method and concept described in the following can easily be extended to any finite number of processing elements.

(50) In a first step 160, a distribution of the computing tasks for the determination of the successor states over the available processing elements is determined. For this, the set 180 of tuples is divided into subsets 182, 184, 186, and 188, which when taken together contain all tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) of the set 180 of tuples. Each subset is assigned to a different processing element of the available processing elements, e.g., subset 182 to processing element 104, subset 184 to processing element 108, subset 186 to processing element 110, and subset 188 to processing element 114. While in general it is desirable to use as many processing elements as possible to speed up the computation, the communication overhead arising from data exchange with and between the processing elements increases with the number of processing elements involved, which may limit the computation speed at some point. In some situations it may therefore be advantageous to only use some of the available processing elements, i.e., the number of subsets may be smaller than the number of available processing elements.

(51) The subsets 182-188 can have the same size, i.e., contain the same number of tuples. Preferably, however, the size of the subsets 182-188 is chosen individually based on information about the processing elements 104, 108, 110, and 114, in particular the types of processing elements, the available computing power of the processing elements, the memory resources of the processing elements or a combination thereof. For example, CPUs are suitable for complex serial mathematical computations and may be assigned a larger number of tasks when constructing the symbolic model, which may involve solving differential equations numerically. The computation time for the determination of the successor states can be minimized by choosing the subsets 182-188 such that the available processing elements 104, 108, 110, and 114 need the same time for executing the tasks assigned to them, i.e., the size of the subspace associated with a processing element scales with the number of successor state determinations the processing element can perform in a given amount of time. In FIG. 4b, the subsets 182-188 are chosen such that they form simply-connected areas in the flat 2D space. The tuples in each subset can, however, be chosen arbitrarily from the set 180 of tuples. Preferably, the tuples in each subset are chosen to minimize communication overhead due to data exchange with the processing elements, in particular taking into account the subsequent determination of the updated winning set 242 in step 140 as well as the potentially different data exchange rates with the processing elements and between different processing elements.

(52) In step 162, the data required for the determination of the successor states is provided to the respective processing elements, e.g., the tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) for which the successor states are to be determined as well as information pertaining the mathematical model. Depending on the memory resources of the processing elements, the entire respective subset is provided at once or the subset is divided further into subsets of the subset, which are provided sequentially whenever the tasks associated with the preceding subset of the subset have been executed.

(53) For each processing unit, a queue of tasks is established to perform the successor state determination for each tuple within the respective subset, e.g., a queue 166 for processing element 104, a queue 168 for processing element 108, a queue 170 for processing element 110, and a queue 172 for processing element 114. Each queue 166, 168, 170, 172 contains multiple sequences of tasks, wherein each sequence of tasks comprises the tasks for determining the at least one successor state {right arrow over (x)}.sub.f for one tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j). This is illustrated in FIG. 4a for a situation, in which the set 180 of tuples contains twelve tuples with i ∈ [1,4] and j ∈ [1,3]. In the sequence 173 of tasks, the at least one successor state for the tuple ({right arrow over (x)}.sub.4, {right arrow over (u)}.sub.2) is determined. The queues 166, 168, 170, 172 of tasks are sent to the respective processing elements and executed in step 164. The execution is performed in parallel at least in part as indicated by the vertical alignment of the queues 166, 168, 170, 172 of tasks. Preferably, the subsets 182-188 are chosen such that each processing element finishes the execution of the respective queue of tasks at the same time.

(54) For each tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j), the at least one successor state {right arrow over (x)}.sub.f is determined based on the mathematical model. The at least one successor state can for example be a state that the control system 12 is expected to be in according to the mathematical model, if the control system 12 is initially in the state {right arrow over (x)}.sub.i and the control input {right arrow over (u)}.sub.j is applied for a predetermined amount of time. This predetermined amount of time can be chosen depending on the control system 12, the mathematical model and/or the method used for determining the at least one successor state. If the mathematical model is a set of differential equations governing the dynamics of the control system 12 or if a set of such differential equations can be derived from the mathematical model, the at least one successor state may be determined by numerically solving the set of differential equations at least in part, e.g., via a Runge-Kutta method or a linear multistep method. Preferably, the at least one successor state is contained in the discretized state space. If the at least one successor state is not contained in the discretized state space, e.g., if it lies between two states from the discretized state space, it may be approximated by the closest state from the discretized state space. Furthermore, if a successor state lies outside of the range of the discretized state space, it may be marked in some way to indicate an out-of-bound state.

(55) The at least one successor state can be more than one successor state, e.g., to account for uncertainties in the determination of the state vector, the application of the control vector, the mathematical model and/or the numerical methods. For example, a successor state center may be calculated in step 174, i.e., the state that the control system 12 is expected to be in according to the mathematical model, if the control system 12 is initially in the state {right arrow over (x)}.sub.i and the control input {right arrow over (u)}.sub.j is applied for the predetermined amount of time. Subsequently, in step 175 a lower bound and an upper bound for the successor state center can be determined, which define a hyper-rectangle in the state space, e.g., as an estimate for the uncertainties. For this, a set of successor states may be determined, for example by calculating successor states for a plurality of state vectors and/or a plurality of control vectors, e.g., within predetermined uncertainty ranges around {right arrow over (x)}.sub.i and {right arrow over (u)}.sub.j respectively, and/or by determining additional successor states for each calculated successor state, e.g., by adding or subtracting a predetermined uncertainty. The set of successor states can be approximated by the lower and upper bound, e.g., by choosing a hyper-rectangle in the state space that contains the entire set or a certain fraction of states from the set. The at least one successor state can then be defined as the set comprising the lower bound and the upper bound. The at least one successor state may additionally contain the successor state center as well. Alternatively, the at least one successor state may comprise the entire set of successor states or a subset of the set of successor states. To reduce the memory requirements, the at least one successor state preferably is a small number of successor states characterizing the set of successor states, e.g., one or more lower bounds and one or more upper bounds defining a hyper-volume in state space.

(56) In step 176, the results of the computations in step 164 are collected by obtaining the at least one successor state for each tuple from the respective processing element. This collection may be performed once the entire queue of tasks for a given processing element has been executed or the data may be collected sequentially whenever a sequence of tasks has been executed. Subsequently, the data for all tuples is combined in step 178 to form the symbolic model 190. The symbolic model 190 contains transition rules for each tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) in the set 180 of tuples, with each rule associating one of the at least one successor state to the tuple ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j). Thus, if the at least one successor state consist of a lower bound and upper bound, there are two rules per tuple, one defining the transition to the state corresponding to the lower bound and a second one defining the transition to the state corresponding to the upper bound.

(57) In other examples of embodiments of the method according to the present invention, the steps 176 and 178 may be modified or omitted altogether, e.g., to reduce the communication overhead associated with the exchange of data with processing elements. For example, a symbolic model covering only the respective subspace may be determined directly on a processing element. Alternatively, the at least one successor state may be collected and/or exchanged between the processing elements only for some of the tuples in the subsets 182-188, e.g., to determine a symbolic model covering the subset used for the determination of the updated targets set in step 140 for each processing element.

(58) FIG. 5a shows an exemplary flowchart for the parallel determination of an updated winning set 242 in step 140 using four processing elements, e.g., the processing elements 104, 108, 110, and 114 in the device 100. An illustration of this process is depicted in FIG. 5b. As for FIGS. 4a and 4b, this number of processing elements is only a specific example and the method and concept described in the following can easily be extended to any finite number of processing elements.

(59) In step 200, a distribution over the available processing elements is determined for the computing tasks for the comparison between the initial winning set 230 and the at least one successor state for each tuple in the set 180 of tuples. The procedure for this is similar to step 160. The set 180 of tuples is divided into subsets 232, 234, 236, and 238, which when taken together contain all tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) of the set 180 of tuples. Each subset is assigned to a different processing element of the available processing elements, e.g., subset 232 to processing element 104, subset 234 to processing element 108, subset 236 to processing element 110, and subset 238 to processing element 114. The size and tuples for each of the subsets 232-238 are chosen in a similar way as described above for the subsets 182-188. For the iterative determination of the final winning set 244 as described above the communication overhead is of particular importance as data has to be exchanged between processing elements multiple times. The number of processing elements and thus the number of subspaces used in step 140 may be different from the one used in step 132. For example, GPUs contain many processing elements, which allow for a massive parallelization of computing tasks, and can thus be particularly suitable for the comparison with the initial winning set 230 as well as for computing the updated winning set.

(60) Subsequently, the data required for the computing tasks assigned to a processing element is provided to the respective processing element in step 202, in particular data relating to the corresponding subset, the initial winning set 230, the symbolic model 190 and the specifications 240. To reduce the amount of data that has to be exchanged, only the data which is relevant for the corresponding subset may be provided. Depending on the memory resources of each processing element, the data may be provided at once or sequentially during the execution of the tasks. As mentioned above, the symbolic model 190 may at least in part already be stored by the processing elements.

(61) For each processing unit, a queue of tasks is established to perform the comparison for each tuple within the respective subset, e.g., a queue 208 for processing element 104, a queue 210 for processing element 108, a queue 212 for processing element 110, and a queue 214 for processing element 114. Each queue contains multiple sequences of tasks, wherein each sequence of tasks comprises the tasks for comparing the at least one successor state of a tuple with the initial winning set 230. This is illustrated in FIG. 5a for a situation, in which the set 180 of tuples ({right arrow over (x)}.sub.i, {right arrow over (u)}.sub.j) contains twelve tuples with i ∈ [1,4] and j ∈ [1,3]. In the sequence 216 of tasks, this comparison is performed for the tuple ({right arrow over (x)}.sub.4, {right arrow over (u)}.sub.2). The queues 208, 210, 212, 214 of tasks are sent to respective the processing elements and executed in step 206. The execution is performed in parallel at least in part as indicated by the vertical alignment of the queues 208, 210, 212, 214 of tasks. Preferably, the subsets 232-238 are chosen such that each processing element finishes the execution of the respective queue of tasks at the same time.

(62) In a sequence of tasks like the sequence 216, the at least one successor state {right arrow over (x)}.sub.f for the respective tuple is obtained, e.g., from a memory associated with the processing element, and subsequently compared with the initial winning set 230. Based on this comparison, the tuple is marked as good or bad to indicate whether it should be included in the updated winning set 242. The tuple can for example be marked as good if the initial winning set 230 contains at least one tuple ({right arrow over (x)}.sub.k, {right arrow over (u)}.sub.l) with {right arrow over (x)}.sub.k={right arrow over (x)}.sub.f for each of the at least one successor state, or for a certain number or fraction of states of the at least one successor state. Alternatively, if the at least one successor state contains a lower bound and an upper bound, the tuple may be marked as good if all of the tuples in the set 180 of tuples that are enclosed by a hyper-rectangle defined by the lower and upper bound, or a certain number or fraction of these tuples are part of the initial winning set 230. Tuples to be marked as good may additionally be required to already be contained in the initial winning set 230. The specifications 240 may contain further conditions which have to be fulfilled as well by tuples to be marked as good.

(63) The tuples marked as good in step 206 are collected from the available processing elements in step 224 and then combined to obtain the updated winning set 242 in step 226. The updated winning set 242 is compared with the initial winning set 230 in step 142 obtain a convergence measure as described above. Alternatively, the available processing elements may perform a comparison of the tuples marked as good in their subset with the corresponding subset of the initial winning set 230 and only provide information pertaining this comparison for the convergence check.

(64) If an additional iteration is to be performed following the convergence check in step 142, data relating to the updated winning set 242 is provided to the processing elements as in step 202 to replace the data relating to the initial winning set 230. To reduce the amount of data that has to be exchanged, information may be provided only about tuples which have been added and/or removed in the updated winning set 242 as compared to the initial winning set 230 and are relevant for the corresponding subset. Subsequently, steps 206, 224, and 226 may be repeated to obtain a new updated winning set. For this, the same task distribution as in the previous iteration may be used or alternatively step 200 may be repeated to obtain a new distribution of tasks prior to repeating step 206.

(65) This procedure is repeated until the convergence criterion is met for the new updated winning set 244, at which point the method proceeds to the controller construction in step 144 as detailed above.

(66) The embodiments of the present invention disclosed herein only constitute specific examples for illustration purposes. The present invention can be implemented in various ways and with many modifications without altering the underlying basic properties. Therefore, the present invention is only defined by the claims as stated below.

LIST OF REFERENCE SIGNS

(67) 10—Controller 12—Control system 14—Symbolic model 16—Specifications 18—Symbolic controller 20—Refined controller 100—Device for synthesizing a correct-by-construction controller 102—Central processing unit (CPU) 104—Processing element 106—Graphics processing unit (GPU) 108—Processing element 110—Processing element 112—Hardware accelerator (HWA) 114—Processing element 116—Computing platform interface 118—Resource identification unit 120—Task scheduling unit 122—Interface unit 124—Management engine 126—Logging unit 130—Step of receiving the mathematical model and specifications 132—Step of identifying available processing elements 134—Step of discretizing the space 136—Step of determining the symbolic model 138—Step of obtaining the initial winning set 140—Step of determining the updated winning set 142—Step of checking the convergence 144—Step of constructing the correct-by-construction controller 146—Step of generating source code for implementing the correct-by construction controller 150—Step of determining available processing elements 152—Step of determining the type of the available processing elements 154—Step of compiling kernels for executing computations on available processing elements 156—Step of determining the computing power of the available processing elements 160—Step of determining the task distribution for determining the symbolic model 162—Step of providing data to processing elements for successor state determination 164—Step of the parallel determination of successor states 166—Queue of tasks 168—Queue of tasks 170—Queue of tasks 172—Queue of tasks 173—Sequence of tasks 174—Step of calculating a successor state center 175—Step of determining the lower bound and the upper bound for a set of successor states 176—Step of collecting results from the parallel determination of successor states 178—Step of determining the symbolic model from the collected data 180—Set of tuples 182—Subset of the set of tuples 184—Subset of the set of tuples 186—Subset of the set of tuples 188—Subset of the set of tuples 190—Symbolic model 200—Step of determining the task distribution for determining the updated winning set 202—Step of providing data to processing elements for updated winning set determination 206—Step of comparing successor states with initial winning set in parallel 208—Queue of tasks 210—Queue of tasks 212—Queue of tasks 214—Queue of tasks 216—Sequence of tasks 218—Step of obtaining successor state from memory 220—Step of comparing successor state with initial winning set 222—Step of determining marking tuples to be included in updated winning set 224—Step of collecting results of successor state comparison 226—Step of determining the updated winning set based on successor state comparison 230—Initial winning set 232—Subset of the set of tuples 234—Subset of the set of tuples 236—Subset of the set of tuples 238—Subset of the set of tuples 240—Specifications 242—Updated winning set 244—Final updated winning set

(68) The various embodiments described above can be combined to provide further embodiments. All of the U.S. patents, U.S. patent application publications, U.S. patent applications, foreign patents, foreign patent applications and non-patent publications referred to in this specification and/or listed in the Application Data Sheet are incorporated herein by reference, in their entirety. Aspects of the embodiments can be modified, if necessary to employ concepts of the various patents, applications and publications to provide yet further embodiments.

(69) These and other changes can be made to the embodiments in light of the above-detailed description. In general, in the following claims, the terms used should not be construed to limit the claims to the specific embodiments disclosed in the specification and the claims, but should be construed to include all possible embodiments along with the full scope of equivalents to which such claims are entitled. Accordingly, the claims are not limited by the disclosure.