Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis

TL;DR

This paper introduces a novel approach combining constrained optimization with falsification techniques to effectively handle conjunctive specifications in cyber-physical systems, demonstrated through experimental validation.

Contribution

It proposes a new method that integrates multiple constraint ranking with CMA-ES-based falsification to improve handling of conflicting requirements in CPS.

Findings

Enhanced performance in falsification tasks

Effective handling of conjunctive specifications

Validation through experimental results

Abstract

The synthesis problem of a cyber-physical system (CPS) is to find an input signal under which the system's behavior satisfies a given specification. Our setting is that the specification is a formula of signal temporal logic, and furthermore, that the specification is a conjunction of different and often conflicting requirements. Conjunctive specifications are often challenging for optimization-based falsification -- an established method for CPS analysis that can also be used for synthesis -- since the usual framework (especially how its robust semantics handles Boolean connectives) is not suited for finding delicate trade-offs between different requirements. Our proposed method consists of the combination of optimization-based falsification and constrained optimization. Specifically, we show that the state-of-the-art multiple constraint ranking method can be combined with falsification powered by CMA-ES optimization; its performance advantage is demonstrated in experiments.