Formal Synthesis of Stochastic Systems via Control Barrier Certificates

We study formal synthesis of control policies for discrete-time stochastic control systems against complex temporal properties. Our goal is to synthesize a control policy for the system together with a lower bound on the probability that the system satisfies a complex temporal property. The desired properties of the system are expressed as a fragment of linear temporal logic (LTL), called safe-LTL over finite traces. We propose leveraging control barrier certificates which alleviate the issue of the curse of dimensionality associated with discretization-based approaches existing in the literature. We show how control barrier certificates can be used for synthesizing policies while guaranteeing lower bounds on the probability of satisfaction for the given property. Our approach decomposes negation of the specification into sequential reachabilities and then finds control barrier certificates for computing upper-bounds on the reachability probabilities. Control policies associated with these barrier certificates are then combined as a hybrid control policy for the concrete system that guarantees a lower bound on the probability of satisfaction of the property.