Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study

We report our experience of applying hybrid system falsification-an optimization-based method of finding a counterexample to a temporal-logic specification-to the parameter synthesis problem of an industrial gas turbine system model. We identified two major challenges unique to the target problem, namely 1) multiple requirements that are at odds, and 2) their geometric nature. These challenges are dealt with by the following two extensions of falsification, respectively: 1) the use of the multiple constraint ranking (MCR) method by de Paula Garcia et al., in combination with CMA-ES, for multiple requirements; and 2) the introduction of the area modality, following the logic AvSTL by Akazaki & Hasuo, for geometric requirements.