How to
Receding-horizon control
Plan a short horizon online from the live state within a deadline.
Where open-loop synthesis plans one input sequence offline, a receding-horizon controller plans online. At each step, it looks a short horizon ahead from the measured state, finds the best plan it can within a deadline, and applies only the first input. The plant advances, the next call sees the new state, and the loop closes.
Planning within a deadline
The search is anytime. It runs gradient chunks until a wall-clock budget expires and returns the best plan found so far, warm-started from the previous step. A budget smaller than a single chunk still returns a plan scored against the live state.
from sentil import Formula, SystemModel, Bounds, Controller
# x_{t+1} = x_t + u_t; reach a position past 2 within five steps
model = SystemModel.linear([[1.0]], [[1.0]], [0.0], ["pos"], 1.0, 5)
spec = Formula.parse("F[0, 5](pos > 2)")
bounds = Bounds([-1.0] * 5, [1.0] * 5)
# apply one input per step, spend at most 5 ms planning each
controller = Controller(model, spec, 1, 5_000_000, bounds=bounds)
state = [0.0]
for _ in range(6):
u = controller.control(state) # the input to apply now
state[0] += u[0]
print(state[0]) # 6.0, well past the target of 2use std::time::Duration;
use sentil::{Bounds, Controller, Formula, LinearModel};
// x_{t+1} = x_t + u_t; reach a position past 2 within five steps
let model = LinearModel::new(vec![vec![1.0]], vec![vec![1.0]], [0.0], ["pos"], 1.0, 5)?;
let spec = Formula::parse("F[0, 5](pos > 2)")?;
// apply one input per step, spend at most 5 ms planning each
let mut controller = Controller::new(&model, &spec, 1, Duration::from_millis(5))
.with_bounds(Bounds::new(vec![-1.0; 5], vec![1.0; 5])?);
let mut state = vec![0.0];
for _ in 0..6 {
let u = controller.control(&state)?; // the input to apply now
state[0] += u[0];
}Controller::new(model, spec, input_width, budget) plans spec over model, applies input_width values per step, and spends at most budget planning each. In Python the budget is nanoseconds, so 5 ms is 5_000_000; in Rust it is a Duration. Each control(state) call returns the first input to apply and warm-starts the next solve from where this one left off. Constrain the actuator with with_bounds, and set the smoothing temperature with with_smooth.
On a no_std target there is no wall clock, so build the controller with Controller::with_iterations, which bounds each plan by a gradient-step count instead of a duration. The step count is a fixed compute budget the board's timer translates back to time. Everything else about the loop is the same.
The convex fast path
When the dynamics are affine and the spec is a minimum of affine predicates, a step is a convex program so, a single solve is far faster than the gradient climb. The controller takes that path automatically and falls back to the gradient search on a spec outside the fragment; a disjunction for instance, or on any numerical failure. Both paths respect the actuator box. The choice is made per step and is internal.
Benchmarking
On the integrator benchmark, the controller planned by gradient and reached a robustness of 0.50.
| measurement | value |
|---|---|
| per-step plan time | 0.099 ms |
| steps | 200 |
| deadline | 5 ms |
| p99 plan time | 0.112 ms |
| missed deadlines | 0 |
NB: The absolute times are machine-dependent.
Closing the loop
Usually, the controller is paired with an online monitor that checks the same spec. So, the loop is (1) plan an input, (2) apply it, and (3) feed the measured state to a monitor. The next control call re-plans from wherever the plant actually is.
from sentil import Formula, SystemModel, Bounds, Controller, OnlineMonitor
model = SystemModel.linear([[1.0]], [[1.0]], [0.0], ["pos"], 1.0, 5)
spec = Formula.parse("F[0, 5](pos > 2) & G[0, 5](pos < 4)")
bounds = Bounds([-1.0] * 5, [1.0] * 5)
controller = Controller(model, spec, 1, 5_000_000, bounds=bounds)
# past-time, so every update resolves immediately
watchdog = OnlineMonitor(Formula.parse("H (pos < 4)"))
state = [0.0]
for t in range(6):
u = controller.control(state) # plan within the deadline
state[0] += u[0]
margin = watchdog.update(float(t), {"pos": state[0]})
print(f"t={t} pos={state[0]:.3f} margin={margin.value:.3f}")
# t=0 pos=0.936 margin=3.064
# ...
# t=5 pos=2.628 margin=1.372use std::time::Duration;
use sentil::{Bounds, Controller, Formula, LinearModel, Monitor, MonitorConfig};
let model = LinearModel::new(vec![vec![1.0]], vec![vec![1.0]], [0.0], ["pos"], 1.0, 5)?;
let spec = Formula::parse("F[0, 5](pos > 2) & G[0, 5](pos < 4)")?;
let mut controller = Controller::new(&model, &spec, 1, Duration::from_millis(5))
.with_bounds(Bounds::new(vec![-1.0; 5], vec![1.0; 5])?);
// past-time, so every update resolves immediately
let mut watchdog = Monitor::new("H (pos < 4)", MonitorConfig::new())?;
let mut state = vec![0.0];
for t in 0..6 {
let u = controller.control(&state)?; // plan within the deadline
state[0] += u[0];
let margin = watchdog.update(t as f64, &[("pos", state[0])])?;
println!("t={t} pos={:.3} margin={:.3}", state[0], margin.value());
}
// t=0 pos=0.936 margin=3.064
// ...
// t=5 pos=2.628 margin=1.372To validate the probabilistic side, check the closed loop with a chance constraint against the stochastic system rather than the nominal model.