Conjunctive Bayesian Optimization (conBO): An application to Cyber-Physical Systems Verification with Conjunctive Requirements

Bayesian optimization (BO) is a widely used technique for optimizing black-box functions, whose mathematical form is unknown and can only be evaluated through costly simulations. In this work, we focus on optimizing functions that are the \(\min/\max\) of several components, where each component is typically a non-linear, non-convex black-box function. Traditional BO approaches may suffer from the masking effect , where components with lower mean values are sampled more, even if they do not contain the global optimum. In our prior work, Minimum Bayesian Optimization ( minBO ) addressed this issue by proposing a sampling approach that uses a surrogate for each component and samples based on predicted improvement across all components. While effective, minBO treats each component independently and does not capture potential dependencies between components. Additionally, estimating surrogates for each component can limit the scalability of the approach. We introduce Conjunctive Bayesian Optimization ( conBO ), a novel approach that overcomes these limitations. We propose a paired sampling algorithm ( conBO-PS ) that considers dependencies between components by analysing all pairs of functions and estimating the distribution of the minimum of two functions. While conBO-PS accounts for dependencies, it is computationally expensive. To improve efficiency, we introduce conBO large-scale ( conBO-LS ), which adapts conBO-PS by considering a subset of components chosen based on their potential impact, allowing users to control computational effort. We evaluate the performance of these algorithms on non-linear synthetic functions and also compare them to state-of-the-art methods in the context of falsifying conjunctive safety requirements for Cyber Physical Systems (CPS). A conjunctive safety requirement refers to a set of safety conditions (requirements) tested together, where if at-least one condition is falsified, the entire conjunctive requirement is considered falsified. In fact, in such context the function to be minimized is the minimum of several sub-components. Results show that conBO-PS and conBO-LS outperform existing approaches, offering better solution quality and computational efficiency. In the CPS application, the proposed approaches achieve faster falsification and improved falsification rates across all benchmarks.