Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2408.06983 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- 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.