Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications

Sota Sato, Jie An, Zhenya Zhang +1

We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encod…