Title:  A Framework to Verify the Coverage Property in the Single Agent and Multi-agent Persistent Turning Walker under a Range of Parameter Values

Committee: 

Dr. F. Zhang, Advisor    

Dr. Coogan, Chair

Dr. Hu

Abstract: The objective of the proposed research is to verify coverage properties of a continuous fish motion model, termed as the Persistent Turning Walker (PTW) model. Dependence on constant availability on an external localization service is often unreliable and infeasible in mobile robots.  We propose that the PTW model is a strategy which can achieve 2D and 3D coverage in an unknown environment in the absence of a localization service, such as a Global Positioning System (GPS). This is achieved by converting the continuous-time dynamical system into a Discrete-Time Markov Chain (DTMC) which is then shown to exhibit strongly connected properties. The formulated DTMC is also verified against certain mathematical hypotheses formulated in the Linear Temporal Logic (LTL) language. The framework can also be used to study the continuous-time dynamics of other biological systems and evaluate their properties. In our preliminary work we have verified the coverage property for the single agent PTW model and in our proposed work, we aim to extend the framework to verify the coverage property for the multi-agent PTW model.  Our work aims to show that the PTW model may be effectively used as a coverage strategy by mobile robots in underwater or underground environments where the availability of a GPS cannot be guaranteed at all times.