Source-linked AI summary
Formal Synthesis of Stochastic Systems via Control Barrier Certificates
Pushpak Jagtap, Sadegh Soudjani, Majid Zamani
TL;DR
The paper tackles formal policy synthesis for discrete-time stochastic systems with continuous state spaces and finite-trace temporal specifications. It decomposes negated specifications into reachability tasks solved with control barrier certificates, then combines the resulting controllers and bounds into a hybrid policy. The paper reports a finite-input temperature-control result with a satisfaction-probability lower bound of 0.9766 and develops systematic certificate-search procedures, subject to LTLF, polynomial-dynamics, and stationary-policy restrictions.
Problem
Formal synthesis for uncertain continuous-state systems with complex temporal specifications lacks generally available exact solutions and faces scalability problems under discretization.
Method
The paper negates each LTLF specification, decomposes its violation into automaton-guided reachability tasks, solves them with control barrier certificates, and combines the controllers and probability bounds.
Results
0.9766 is the reported lower bound on finite-trace specification satisfaction for the room-temperature example with a finite input set.
Takeaways & Limitations
The approach provides discretization-free synthesis of stationary policies with lower satisfaction-probability bounds for discrete-time stochastic systems under its stated assumptions.
Takeaways & Limitations
The approach is restricted to LTLF properties, polynomially transformable dynamics, and stationary policies, while finite-input CEGIS may run forever without an iteration cap.
Abstract
from arXiv · showhide
This paper focuses on synthesizing control policies for discrete-time stochastic control systems together with a lower bound on the probability that the systems satisfy the complex temporal properties. The desired properties of the system are expressed as linear temporal logic (LTL) specifications over finite traces. In particular, our approach decomposes the given specification into simpler reachability tasks based on its automata representation. We then propose the use of so-called \emph{control barrier certificate} to solve those simpler reachability tasks along with computing the corresponding controllers and probability bounds. Finally, we combine those controllers to obtain a hybrid control policy solving the considered problem. Under some assumptions, we also provide two systematic approaches for uncountable and finite input sets to search for control barrier certificates. We demonstrate the effectiveness of the proposed approach on a room temperature control and lane-keeping of a vehicle modeled as a four-dimensional single-track kinematic model. We compare our results with the discretization-based methods in the literature.
1. Introduction
The paper addresses formal policy synthesis for uncertain continuous-state systems, where exact solutions are generally unavailable and discretization-based methods face severe scalability challenges. It combines automata for finite-trace temporal logic with control barrier certificates to synthesize policies and probability bounds, while providing systematic certificate-search approaches.
- Exact synthesis is difficult for uncertain systems with continuous state spaces because closed-form solutions are generally unavailable.
- Discretization-based methods abstract stochastic systems using finite models and formal approximation-error bounds, but suffer from the curse of dimensionality.
- The paper combines automata for LTLF specifications with control barrier certificates to synthesize offline policies and lower bounds on finite-horizon satisfaction probabilities.
- The synthesis procedure negates the specification, decomposes its violation into sequential reachability tasks, solves them with barrier certificates, and combines the resulting controllers and bounds.
- Two systematic certificate-search approaches are provided under suitable assumptions because control barrier certificates may not exist and lack a complete computation algorithm.
2. Preliminaries
The preliminaries define discrete-time stochastic control systems, finite-trace temporal specifications, automata representations, and the probability-based synthesis problem. Policies may depend on histories or only on the current state under stationary control.
- 2.2. Discrete-time stochastic control systems.: A discrete-time stochastic control system consists of state, uncertainty, and input sets, an i.i.d. uncertainty sequence, and measurable dynamics governing state evolution.
- 2.2. Discrete-time stochastic control systems.: A history-dependent policy maps each finite state-action history to an input, whereas a stationary policy depends only on the current state and remains unchanged over time.
- 2.3. Linear temporal logic over finite traces.: LTLF extends LTL syntax to finite traces, whose semantics evaluate temporal operators over a finite sequence of proposition interpretations.
- 2.4. Deterministic finite automata.: Every LTLF formula can be translated into a deterministic finite automaton accepting the same language, enabling automata-based specification processing.
- 2.5. Problem formulation.: A system state sequence is mapped to a proposition trace through a measurable labeling function, and satisfaction probability is evaluated over a finite horizon under a policy.
- 2.5. Problem formulation.: The synthesis problem seeks a policy ensuring that the finite-trace specification is satisfied with probability at least a prescribed threshold for specified labeled initial states.
3. Control Barrier Certificates
Control barrier certificates provide the core reachability bounds used in the synthesis procedure. Their relaxed supermartingale conditions support stationary policy construction and finite-horizon probability bounds for continuous or finite input sets.
- Control barrier certificates are relaxed supermartingale-like functions whose expected value decreases along controlled system trajectories up to a constant.
- For finite input sets, the certificate condition becomes a minimum over inputs of the conditional expected next certificate value.
- A certificate induces a stationary policy by selecting an input satisfying the certificate inequality, or by minimizing its expected next value for discrete inputs.
- The reachability theorem upper-bounds the probability of reaching a target set within horizon Td by γ + cTd under the stated certificate conditions.
- The resulting optimization minimizes γ and c to obtain a finite-horizon reachability upper bound that is as tight as possible.
- When c = 0, the theorem applies to an unbounded time horizon, while allowing c > 0 makes certificates easier to find and broadens applicability.
4. Decomposition into Sequential Reachability
The paper converts an LTLF synthesis problem into sequential reachability tasks by analyzing accepting runs of a DFA for the negated specification. Self-loops are removed from bounded accepting runs, then length-three state segments with horizons are constructed for barrier-certificate analysis.
- Automata representation: The DFA A¬ϕ accepts finite words satisfying ¬ϕ, and its accepting state runs provide the paths used for decomposition.Runs begin in Q0, end in F, and correspond to finite proposition words labeling DFA transitions.
- Automata representation: Self-loop-free accepting runs of length at most N + 1 are collected in RN for the bounded decomposition.RN excludes consecutive repeated states and can be computed by viewing the DFA as a directed graph and applying depth-first search.
- Run grouping: For each initial edge proposition p, the construction groups accepting runs into Rp according to the proposition labeling the first transition.This grouping supports the subsequent sequential reachability construction for each possible initial region.
- Sequential reachability construction: Each run q in Rp is decomposed into length-three state segments, each paired with a horizon T(q, qi+1).The horizon is N + 2 − |q| when qi+1 is a self-loop state and 1 otherwise.
- Sequential reachability construction: The two transitions represented by each length-three segment later define regions Xa and Xb and the associated reachability horizon Td.Runs of length two are omitted because they yield a trivial zero probability for satisfying the specification.
5. Controller Synthesis using Control Barrier Certificates
The paper synthesizes a hybrid control policy by decomposing temporal-logic satisfaction into sequential reachability tasks and assigning barrier-certificate controllers to automaton-dependent partitions. It combines reachability bounds into a probability guarantee, while addressing certificate search, conservatism, and computational scaling.
- Policy construction: A policy with a potentially tight lower bound on satisfying ϕ is computed by performing reachability analysis over elements of P(A¬ϕ).Each element represents a state run augmented with a horizon.
- Switching mechanism: Different automaton locations induce different controllers, combined through DFA Am into a switching control policy on the augmented space X × Qm.The resulting policy is Markov on X × Qm and equivalent to a history-dependent policy on X.
- Policy construction: Control barrier certificates upper-bound each sequential reachability probability, with suitable control inputs producing the corresponding local controllers.For ν = (q, q′, q′′, T), the bound γν + cνT applies to transitions between proposition-labeled regions.
- Probability computation: Theorem 5.2 decomposes computation into sequential reachability, computes bounds using Theorem 3.6, and combines them in a sum-product expression.The resulting upper bound may be clipped by min(·,1) and is useful only when below one.
- Example result: 1.453e-6 is the computed upper bound on violating ϕ for all x0 ∈ L−1(p0) in Example 1.The bound is obtained as 4.883e-4 × 0.002 + 4.883e-4 × 9.766e-4.
- Computation and limitations: The number of required control barrier certificates is bounded by |Q|3, while fixed-degree sum-of-squares computations grow polynomially with system dimension.The CEGIS approach lacks a general termination guarantee, and common certificates can produce conservative probability bounds.
6. Case Studies
The case studies apply control-barrier-certificate synthesis to room-temperature regulation and vehicle lane keeping, reporting probability lower bounds and empirical or abstraction-based validation.
- Room temperature control: The room-temperature system uses stochastic thermal dynamics with a finite heater-valve input set U = {0, 0.5, 1}.The state is bounded to X = [0, 45], and environmental uncertainty is modeled by a standard normal disturbance.
- Room temperature control: 0.9766 is the synthesized lower bound for the finite-input room-temperature policy over the specified initial states.The policy is obtained with Z3 and sequential quadratic programming; finding the certificate and bound took around 4 minutes.
- Room temperature control: The continuous-input room-temperature policy has lower bound 0.9281, which is more conservative than the finite-input case.The paper attributes this conservatism mainly to fixed-degree polynomial optimization; increasing degrees can improve the bound at higher computational cost.
- Room temperature control: FAUST2 verifies the synthesized room-temperature lower bound a posteriori and also produces a comparison using a time-dependent policy.The discretization-based approach is used for validation because direct comparison with the synthesized policy is not possible when policies are generally time-dependent.
7. Conclusion
The paper presents a discretization-free synthesis approach for discrete-time stochastic control systems that computes policies and probability lower bounds for finite-trace LTL specifications. It identifies continuous-time extension and scalability as remaining boundaries for the approach.
- The approach synthesizes control policies alongside lower bounds on the probability of satisfying finite-trace LTL specifications.
- It uses control barrier certificates with sum-of-squares optimization or counter-example guided inductive synthesis to obtain policies.
- Continuous-time stochastic extensions can exclude the next operator but may become more conservative because the temporal horizon must use worst-case T = N.
- The authors identify compositional barrier-certificate construction and parallel-computation tooling as directions for improving scalability.