Temporal Logic Guided Safe Model-Based Reinforcement Learning

M. Cohen,Călin Belta

Synthesis Lectures on Computer Science(2023)

Cited 0|Views3
No score
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.
Translated text
Key words
AI Read Science
Must-Reading Tree
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined