Vehicle with Time: Signal First-Order Logic for Closed-Loop Controller Synthesis
summary
Vehicle extends the Vehicle DSL with a Time type, discrete-time bounded operators (□,[a,b], ◇,[a,b], U_[a,b]), an @dynamics annotation and a rollout primitive that produces full trajectories and evaluates temporal formulas on GPU via an adapted STLCG++/PyTorch backend. A general Signal First-Order logic semantics compiles to differentiable losses (soundness reuse theorem), synthesises adaptive cruise controllers from a single spec without behaviour cloning, and verifies them with CROWN reachability — controllers outperform ARCH-COMP 2025 BC on every centre-evaluated property.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:49Neural networks and safety
- 5:20Closed-loop controller scenarios
- 7:50Limitations without time
- 9:14Extending Vehicle with SFO logic
- 9:34Temporal operators semantics
- 11:24State and dynamics in Vehicle
- 13:14Safety properties over trajectories
- 15:03Differentiable logics for controllers
- 17:33GPU acceleration with STLCG++
- 18:18Error bounds in smooth operators
- 21:12Adaptive cruise control case study
- 24:02Training with STL and SFO logic
- 25:27Benchmark results and performance
- 27:14Future work and verification
- 28:57Uncertainty bounds theorem
- 29:40Q&A
related talks
16mSyntra: Synthesizing Cross-Layer Controllers for Low-Latency Video Streaming
13mExtending SUMO for Lane-Free Microscopic Simulation of Connected and Automated Vehicles
13mWIP: Learning Adversarial Attacks on Adaptive Traffic Signal Control Systems...
10mRobots, rockets, and more! Control theory in 10 minutes!
22mSynthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
39mLinear Logic Programming
59mOn Human-robot Interactions via Multimodal Intent Modeling and Reachability-based Safety Assurance
42mEnforcing Constraints for Time Series Prediction in Supervised/Unsupervised/Reinforcement Learning