Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


19843.pdf (5.41 MB)

ETD Abstract Container

Abstract Header

Verification of Genetic Fuzzy Systems

Arnett, Timothy J.
http://orcid.org/0000-0001-6759-4593
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1460731645

Abstract Details

2016, MS, University of Cincinnati, Engineering and Applied Science: Aerospace Engineering.
In recent years, there have been huge advances in controllers used in autonomous systems. One particular area of research is Fuzzy Logic Controllers (FLCs) that are trained by both expert knowledge-based optimization algorithms such as Genetic Algorithms (GAs). GAs represent a particularly powerful way to optimize a FLC as they often perform better than other search algorithms when the state space is rather complex. A downside to these systems however is that their functionality is difficult to verify due to highly non-linear behavior. Typical verification involves Monte Carlo type simulations that require time to perform and may miss critical test points. Therefore, there is a need for more formal ways of verifying the correctness of FLCs based on specifications set forth for their operation over the entire state space. In this work, a method of converting a 2-input 1-output FLC with specific constraints into a Piecewise Affine Hybrid System (PWAHS) is extended to a 3-input 1-output case for implementation of a cascaded FLC system. Verification of safety properties of the converted PWAHS using Formal Methods tools is then conducted. FLCs were then created for a case study involving both one and two degree-of-freedom inverted pendulum systems and trained with Genetic Algorithms. Specifications about their functionality were derived from expert knowledge of the system and simulation results. The specifications were translated into temporal logic specifications that could then be checked by Symbolic Model Checkers (SMCs) utilizing Satisfiability Modulo Theories (SMT) solvers. It is shown that the FLCs created are shown to meet the requirements set forth, and in cases where they do not, generated counterexamples give a point in the state space where they are violated. FLCs that violated the properties were then re-trained and checked again using specifications derived from simulation results. The final FLC was shown to meet all safety specifications under all conditions, leveraging a model checking verification approach for to show satisfaction.
Kelly Cohen, Ph.D. (Committee Chair)
Matthew A. Clark, M.S. (Committee Member)
Nicholas D. Ernest, Ph.D. (Committee Member)
Manish Kumar, Ph.D. (Committee Member)
119 p.
Aerospace Materials
fuzzy logic; verification; model checking; genetic algorithm

Recommended Citations

Citations

  • Arnett, T. J. (2016). Verification of Genetic Fuzzy Systems [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1460731645

    APA Style (7th edition)

  • Arnett, Timothy. Verification of Genetic Fuzzy Systems. 2016. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1460731645.

    MLA Style (8th edition)

  • Arnett, Timothy. "Verification of Genetic Fuzzy Systems." Master's thesis, University of Cincinnati, 2016. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1460731645

    Chicago Manual of Style (17th edition)

ucin1460731645
546
© 2016, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.