Skip to Main Content
Frequently Asked Questions
Submit an ETD
Global Search Box
Need Help?
Keyword Search
Participating Institutions
Advanced Search
School Logo
Files
File List
Masters, David Accepted Thesis 4-20-21 Sp 21.pdf (290.03 KB)
ETD Abstract Container
Abstract Header
Verifying Value Iteration and Policy Iteration in Coq
Author Info
Masters, David M
Permalink:
http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1618999718015199
Abstract Details
Year and Degree
2021, Master of Science (MS), Ohio University, Electrical Engineering & Computer Science (Engineering and Technology).
Abstract
Reinforcement learning is a growing field of research, but little work is being done to verify the correctness of reinforcement learning algorithms. Researchers are exploring the use of reinforcement learning in safety critical systems such as self-driving cars and autonomous aircraft, so mathematical proofs of correctness of the underlying reinforcement learning algorithms would greatly improve our confidence in the systems that utilize reinforcement learning. This project verifies convergence and optimality of two fundamental reinforcement learning algorithms: value iteration and policy iteration. These algorithms converge and are optimal if they eventually produce an optimal policy. It also is designed to be extensible to future research into verified reinforcement learning.
Committee
Gordon Stewart (Advisor)
Bunescu Razvan (Committee Member)
Juedes David (Committee Member)
Elster Charlotte (Committee Member)
Pages
63 p.
Subject Headings
Computer Science
Keywords
Reinforcement Learning
;
Software Verification
;
Coq
;
Value Iteration
;
Policy Iteration
Recommended Citations
Refworks
EndNote
RIS
Mendeley
Citations
Masters, D. M. (2021).
Verifying Value Iteration and Policy Iteration in Coq
[Master's thesis, Ohio University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1618999718015199
APA Style (7th edition)
Masters, David.
Verifying Value Iteration and Policy Iteration in Coq.
2021. Ohio University, Master's thesis.
OhioLINK Electronic Theses and Dissertations Center
, http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1618999718015199.
MLA Style (8th edition)
Masters, David. "Verifying Value Iteration and Policy Iteration in Coq." Master's thesis, Ohio University, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1618999718015199
Chicago Manual of Style (17th edition)
Abstract Footer
Document number:
ohiou1618999718015199
Download Count:
482
Copyright Info
© 2021, all rights reserved.
This open access ETD is published by Ohio University and OhioLINK.