Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
summary
An algorithm synthesizes Metric Temporal Logic formulas that are provably bounded lookahead (future reach ≤ K) and globally separate given positive and negative piecewise‑constant signals, reducing synthesis to satisfiability in Linear Real Arithmetic and producing minimal formulas by iterating formula size. The construction encodes MTL semantics over dense time into SMT, yields a decision in NP for existence, and is implemented as TEAL with Z3, recovering many benchmark formulas quickly and timing out only for larger target formulas combined with large samples.
AI-written summary · about
chapters (7)
- 0:00Runtime verification intro
- 3:14Writing MTL formulas challenges
- 8:54MTL formula synthesis problem
- 12:11Decision problem NP characterization
- 14:38SMT encoding for MTL semantics
- 17:53Implementation and evaluation
- 19:17Future work and conclusion
related talks
14mA Unifying Approach to Product Constructions for Quantitative Temporal Inference
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
25mLearning Formulas in Finite Variable Logics
29mEfficient Discovery of Actual Causality in Stochastic Systems
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
31mVehicle with Time: Signal First-Order Logic for Closed-Loop Controller Synthesis
43mQuantitative Algebraic Reasoning
26mData-Driven Lemma Synthesis for Interactive Proofs