Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
<|reference_start|>Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications: 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 encoding of the STL semantics; it follows the idea of stable partitioning from the recent work on SMT-based STL model checking. Assuming that our (continuous-time) system models can be encoded to MILP -- typical examples are rectangular hybrid automata (precisely) and hybrid dynamics with closed-form solutions (approximately) -- our MILP encoding yields an optimization-based model checking algorithm that is scalable, is anytime/interruptible, and accommodates parameter mining. Experimental evaluation shows our algorithm's performance advantages especially for complex STL formulas, demonstrating its practical relevance e.g. in the automotive domain.<|reference_end|>
@article{sato2024optimization-based,
    title={Optimization-Based Model Checking and Trace Synthesis for Complex STL
  Specifications},
    author={Sota Sato, Jie An, Zhenya Zhang, Ichiro Hasuo},
    journal={arXiv preprint arXiv:2408.06983},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.06983},
    primaryClass={eess.SY cs.SY}
}