Formal Synthesis of Stochastic Systems via Control Barrier Certificates

Understand

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.