Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis
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.
Cite
@article{arxiv.2012.00319,
title = {Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis},
author = {Sota Sato and Masaki Waga and Ichiro Hasuo},
journal= {arXiv preprint arXiv:2012.00319},
year = {2021}
}