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.
Temporal Logic Guided Safe Model-Based Reinforcement Learning
synth. Lectures on Computer sci.
Adaptive and Learning-Based Control of Safety-Critical Systems ; Kapitel : 9 ; 165-192
2023-05-16
28 pages
Aufsatz/Kapitel (Buch)
Elektronische Ressource
Englisch