# Temporal Logic Guided Safe Model-Based Reinforcement Learning

Synthesis Lectures on Computer Science（2023）

Abstract

Temporal logics are formal, expressive languages traditionally used in the computer science area of formal methods to specify the correctness of digital circuits and computer programs. Safety, as defined in previous chapters, is just a particular case of a temporal logic formula. In this chapter, we discuss adding general, temporal logic specifications to the control problem considered previously. In Sect. 9.1, we introduce Linear Temporal Logic (LTL) and automata accepting languages satisfying LTL formulas. Our approach to constructing controllers that enforce the satisfaction of an LTL formula is to break down an LTL formula into a sequence of reach-avoid subproblems. In Sect. 9.2, we formulate and solve these subproblems, and in Sect. 9.3 we present a hybrid system approach to combine the above controllers in such a way that the trajectories of the closed loop system satisfy the formula. We extend this procedure to systems for which CLFs are not known or for which the dynamics are uncertain in Sect. 9.4, where we leverage the MBRL framework from Chap. 8. We illustrate the method developed in this chapter with numerical examples in Sect. 9.5 and conclude with final remarks, references, and suggestions for further reading in Sect. 9.6.

MoreTranslated text

Key words

temporal,learning,model-based

AI Read Science

Must-Reading Tree

Example

Generate MRT to find the research sequence of this paper

Chat Paper

Summary is being generated by the instructions you defined