ETDs

This collection includes most of the ASU Theses and Dissertations from 2011 to present. ASU Theses and Dissertations are available in downloadable PDF format; however, a small percentage of items are under embargo. Information about the dissertations/theses includes degree information, committee members, an abstract, supporting data or media.

In addition to the electronic theses found in the ASU Digital Repository, ASU Theses and Dissertations can be found in the ASU Library Catalog.

Dissertations and Theses granted by Arizona State University are archived and made available through a joint effort of the ASU Graduate College and the ASU Libraries. For more information or questions about this collection contact or visit the Digital Repository ETD Library Guide or contact the ASU Graduate College at gradformat@asu.edu.

Displaying 1 - 1 of 1
Filtering by

Clear all filters

155536-Thumbnail Image.png

Representing Hybrid Transition Systems in an Action Language Modulo ODEs

Description
Several physical systems exist in the real world that involve continuous as well as discrete changes. These range from natural dynamic systems like the system of a bouncing ball to robotic dynamic systems such as planning the motion of a robot across obstacles. The key aspects of effectively describing such…

Several physical systems exist in the real world that involve continuous as well as discrete changes. These range from natural dynamic systems like the system of a bouncing ball to robotic dynamic systems such as planning the motion of a robot across obstacles. The key aspects of effectively describing such dynamic systems is to be able to plan and verify the evolution of the continuous components of the system while simultaneously maintaining critical constraints. Developing a framework that can effectively represent and find solutions to such physical systems prove to be highly advantageous. Both hybrid automata and action languages are formal models for describing the evolution of dynamic systems. The action language C+ is a rich and expressive language framework to formalize physical systems, but can be used only with physical systems in the discrete domain and is limited in its support of continuous domain components of such systems. Hybrid Automata is a well established formalism used to represent such complex physical systems at a theoretical level, however it is not expressive enough to capture the complex relations between the components of the system the way C+ does.

This thesis will focus on establishing a formal relationship between these two formalisms by showing how to succinctly represent Hybrid Automata in an action language which in turn is defined as a high-level notation for answer set programming modulo theories (ASPMT) --- an extension of answer set programs in the first-order level. Furthermore, this encoding framework is shown to be more effective and expressive than Hybrid Automata by highlighting its ability in allowing states of a hybrid transition system to be defined by complex relations among components that would otherwise be abstracted away in Hybrid Automata. The framework is further realized in the implementation of the system CPLUS2ASPMT, which takes advantage of state of the art ODE(Ordinary Differential Equations) based SMT solver dReal to provide support for ODE based evolution of continuous components of a dynamic system.
ContributorsLoney, Nikhil (Author) / Lee, Joohyung (Thesis advisor) / Fainekos, Georgios (Committee member) / Zhang, Yu (Committee member) / Arizona State University (Publisher)
Created2017