(76a) Verifying Performance Specifications for Dynamic Processes Under Uncertainty Using Backward Reachability Analysis

A new algorithm is presented for efficiently characterizing the set of uncertain inputs to a dynamic process for which the process is guaranteed to satisfy a given set of performance specifications. These specifications are generally described as a combination of ‘goal sets’ that the system states must eventually reach or remain in indefinitely (e.g., attaining a desired level of conversion or purity), and ‘obstacles’ that must be avoided (e.g., operating regions that are unsafe or otherwise detrimental to the process or product). Characterizing the set of inputs for which these specifications are guaranteed to be satisfied provides a robust operating envelope for the process, and is important in a number of applications where one or more of the following properties hold: (i) large input variability is unavoidable, (ii) critical product specifications are difficult or impossible to measure online, and therefore must be ensured by operating within a precomputed envelope, and/or (iii) even temporary violations of a specification can contaminate or otherwise destroy the product, and are therefore intolerable. For example, all of these qualities occur in various pharmaceutical and biopharmaceutical processes, which has led to widespread interest in the concept of ‘Quality-by-Design’ (QbD). In the QbD paradigm, the set of process inputs for which all critical product quality attributes can be ensured is known as the ‘design space’, and algorithms for efficiently computing it are of critical importance. Other emerging applications where robust performance verification is critical include remote modular systems, such as wellhead gas purification systems, remote power systems, and advanced manufacturing systems using automated industrial robotics.

To address the formal verification of such processes, we will present an algorithm that provides guaranteed inner and outer approximations of the set of inputs that lead to satisfaction of all performance specifications with certainty. This problem is commonly referred to as ‘backward reachability analysis,’ and is solved in the most basic approach by embedding forward reachability calculations in a branch-and-bound framework (forward reachability analysis aims to bound the set of model outputs that are achievable with given set of inputs). In our algorithm, we apply this standard branch-and-bound approach with several novel advancements. First, we use advanced forward reachability algorithms recently developed in our group, which are able to achieve much tighter bounds than other algorithms of similar complexity in many important application areas by exploiting model redundancy and centered-form enclosures. Second, we use custom dynamic constraint propagation techniques based on the specified goal and obstacle sets to accelerate convergence of the algorithm. Our final algorithm will be demonstrated using case studies in design space construction, and will be compared against state-of-the-art algorithms from the literature in terms of both accuracy and efficiency.