Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

4-2023

Abstract

Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifer framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.

Keywords

Learning-based control, Stochastic systems, Martingales, Formal verification

Discipline

Databases and Information Systems | OS and Networks

Research Areas

Intelligent Systems and Optimization

Areas of Excellence

Digital transformation

Publication

Proceedings of the 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27

First Page

3

Last Page

25

ISBN

9783031308239

Identifier

10.1007/978-3-031-30823-9_1

Publisher

Springer

City or Country

Switzerland

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-031-30823-9_1

Download

Share

COinS