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

2024/08/13 by Sota Sato, Sato, Sota, Jie An +5 · 2 citations
Computer Science · #FOS: Electrical engineering #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · pdf · doi:10.48550/arxiv.2408.06983

openalex publication_date 2024/08/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Online Monitoring and Risk Assessment of Non-Cooperative UAVs via STL-Aware Adaptive Fusion Kalman Filtering
• Trace Repair for Temporal Behavior Trees

Related

• Improved Bounded Model Checking of Timed Automata
• Bounded Model Checking of an MITL Fragment for Timed Automata
• Diagnosis and Repair for Synthesis from Signal Temporal Logic\n Specifications
• Time-Robust Control for STL Specifications
• Formal Analysis and Verification of Max-Plus Linear Systems