Formal Synthesis of Stochastic Systems via Control Barrier Certificates

Abstract

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.

arXiv comment22 pages, 11 figures. arXiv admin note: text overlap with arXiv:1807.00064

References in corpus (6)

• Control Barrier Function Based Quadratic Programs for Safety Critical Systems
• FAUST${}^2$: Formal Abstractions of Uncountable-STate STochastic processes
• Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems
• A hybrid barrier certificate approach to satisfy linear temporal logic specifications
• First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
• A Class of Control Certificates to Ensure Reach-While-Stay for Switched Systems

Cited by in corpus (10)

• Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems
• Verification of Approximate Opacity via Barrier Certificates
• Context-triggered Abstraction-based Control Design
• Formal Policy Synthesis for Continuous-Space Systems via Reinforcement Learning
• Safe Control for Nonlinear Systems Under Faults and Attacks Via Control Barrier Functions
• Verification of Quantum Systems using Barrier Certificates
• Spatiotemporal Tubes for Temporal Reach-Avoid-Stay Tasks in Unknown Systems
• Reactive Temporal Logic Planning for Multiple Robots in Unknown Occupancy Grid Maps
• Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates
• Verification and Parameter Synthesis for Stochastic Systems using Optimistic Optimization