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

TL;DR

This paper introduces a scalable, optimization-based model checking method for complex signal temporal logic specifications using MILP encoding, enabling efficient verification and trace synthesis for hybrid systems, especially in automotive applications.

Contribution

The paper presents a novel MILP encoding of STL semantics and an optimization-based model checking algorithm that is scalable, interruptible, and supports parameter mining.

Findings

Effective for complex STL formulas

Demonstrates practical relevance in automotive systems

Offers scalable and anytime verification capabilities

Abstract

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.