Matching Items (1,043)
Filtering by

Clear all filters

150359-Thumbnail Image.png
Description
S-Taliro is a fully functional Matlab toolbox that searches for trajectories of minimal robustness in hybrid systems that are implemented as either m-functions or Simulink/State flow models. Trajectories with minimal robustness are found using automatic testing of hybrid systems against user specifications. In this work we use Metric Temporal Logic

S-Taliro is a fully functional Matlab toolbox that searches for trajectories of minimal robustness in hybrid systems that are implemented as either m-functions or Simulink/State flow models. Trajectories with minimal robustness are found using automatic testing of hybrid systems against user specifications. In this work we use Metric Temporal Logic (MTL) to describe the user specifications for the hybrid systems. We then try to falsify the MTL specification using global minimization of robustness metric. Global minimization is carried out using stochastic optimization algorithms like Monte-Carlo (MC) and Extended Ant Colony Optimization (EACO) algorithms. Irrespective of the type of the model we provide as an input to S-Taliro, the user needs to specify the MTL specification, the initial conditions and the bounds on the inputs. S-Taliro then uses this information to generate test inputs which are used to simulate the system. The simulation trace is then provided as an input to Taliro which computes the robustness estimate of the MTL formula. Global minimization of this robustness metric is performed to generate new test inputs which again generate simulation traces which are closer to falsifying the MTL formula. Traces with negative robustness values indicate that the simulation trace falsified the MTL formula. Traces with positive robustness values are also of great importance because they indicate how robust the system is against the given specification. S-Taliro has been seamlessly integrated into the Matlab environment, which is extensively used for model-based development of control software. Moreover the toolbox has been developed in a modular fashion and therefore adding new optimization algorithms is easy and straightforward. In this work I present the architecture of S-Taliro and its working on a few benchmark problems.
ContributorsAnnapureddy, Yashwanth Singh Rahul (Author) / Fainekos, Georgios (Thesis advisor) / Lee, Yann-Hang (Committee member) / Gupta, Sandeep (Committee member) / Arizona State University (Publisher)
Created2011
148109-Thumbnail Image.png
Description

System and software verification is a vital component in the development and reliability of cyber-physical systems - especially in critical domains where the margin of error is minimal. In the case of autonomous driving systems (ADS), the vision perception subsystem is a necessity to ensure correct maneuvering of the environment

System and software verification is a vital component in the development and reliability of cyber-physical systems - especially in critical domains where the margin of error is minimal. In the case of autonomous driving systems (ADS), the vision perception subsystem is a necessity to ensure correct maneuvering of the environment and identification of objects. The challenge posed in perception systems involves verifying the accuracy and rigidity of detections. The use of Spatio-Temporal Perception Logic (STPL) enables the user to express requirements for the perception system to verify, validate, and ensure its behavior; however, a drawback to STPL involves its accessibility. It is limited to individuals with an expert or higher-level knowledge of temporal and spatial logics, and the formal-written requirements become quite verbose with more restrictions imposed. In this thesis, I propose a domain-specific language (DSL) catered to Spatio-Temporal Perception Logic to enable non-expert users the ability to capture requirements for perception subsystems while reducing the necessity to have an experienced background in said logic. The domain-specific language for the Spatio-Temporal Perception Logic is built upon the formal language with two abstractions. The main abstraction captures simple programming statements that are translated to a lower-level STPL expression accepted by the testing monitor. The STPL DSL provides a seamless interface to writing formal expressions while maintaining the power and expressiveness of STPL. These translated equivalent expressions are capable of directing a standard for perception systems to ensure the safety and reduce the risks involved in ill-formed detections.

ContributorsAnderson, Jacob (Author) / Fainekos, Georgios (Thesis director) / Yezhou, Yang (Committee member) / Computer Science and Engineering Program (Contributor) / Barrett, The Honors College (Contributor)
Created2021-05
137869-Thumbnail Image.png
Description
Meteorology is an uncommon term rarely resonating through elementary classrooms. However, it is a concept found in both fourth and sixth grade Arizona science standards. As issues involving the environment are becoming more pertinent, it is important to study and understand atmospheric processes along with fulfilling the standards for each

Meteorology is an uncommon term rarely resonating through elementary classrooms. However, it is a concept found in both fourth and sixth grade Arizona science standards. As issues involving the environment are becoming more pertinent, it is important to study and understand atmospheric processes along with fulfilling the standards for each grade level. This thesis project teaches the practical skills of weather map reading and weather forecasting through the creation and execution of an after school lesson with the aide of seven teen assistants.
ContributorsChoulet, Shayna (Author) / Walters, Debra (Thesis director) / Oliver, Jill (Committee member) / Balling, Robert (Committee member) / Barrett, The Honors College (Contributor) / College of Liberal Arts and Sciences (Contributor)
Created2012-12
137870-Thumbnail Image.png
Description
Plants are essential to human life. They release oxygen into the atmosphere for us to breathe. They also provide shelter, medicine, clothing, tools, and food. For many people, the food that is on their tables and in their supermarkets isn't given much thought. Where did it come from? What part

Plants are essential to human life. They release oxygen into the atmosphere for us to breathe. They also provide shelter, medicine, clothing, tools, and food. For many people, the food that is on their tables and in their supermarkets isn't given much thought. Where did it come from? What part of the plant is it? How does it relate to others in the plant kingdom? How do other cultures use this plant? The most many of us know about them is that they are at the supermarket when we need them for dinner (Nabhan, 2009) (Vileisis, 2008).
ContributorsBarron, Kara (Author) / Landrum, Leslie (Thesis director) / Swanson, Tod (Committee member) / Pigg, Kathleen (Committee member) / Barrett, The Honors College (Contributor) / College of Liberal Arts and Sciences (Contributor)
Created2012-12
137871-Thumbnail Image.png
DescriptionBased on previous research and findings it is proven that a non-profit class to create awareness will be beneficial in the prevention of eating disorders. This analysis will provide significant research to defend the proposed class.
ContributorsAllen, Brittany (Author) / Chung, Deborah (Author) / Fey, Richard (Thesis director) / Peck, Sidnee (Committee member) / Mazurkiewicz, Milena (Committee member) / Barrett, The Honors College (Contributor) / W. P. Carey School of Business (Contributor) / College of Liberal Arts and Sciences (Contributor)
Created2012-12
Description
Restraint stress is the most commonly used laboratory stressor. It is difficult to characterize as psychological or physical, because past studies show psychological features, but the nature of confinement adds a physical dimension. This was the first study to investigate how experience with restraint stress affects brain response to the

Restraint stress is the most commonly used laboratory stressor. It is difficult to characterize as psychological or physical, because past studies show psychological features, but the nature of confinement adds a physical dimension. This was the first study to investigate how experience with restraint stress affects brain response to the next stress without a physical burden. Pair-housed adult male rats were transported to a novel context and restrained or left undisturbed (6hr). The next day, rats were returned to the same context and were either restrained or left undisturbed in the context (n=8/group). After 90min, rats were euthanized to determine functional activation in limbic structures using Fos immunohistochemistry and to measure HPA axis reactivity through blood serum corticosterone levels. Regardless of day 1 experience, context exposure on day 2 enhanced Fos expression in CA1 and CA3 of the hippocampus, basolateral amygdala, and central amygdala. Conversely, other regions and corticosterone levels demonstrated modulation from the previous day's experience. Specifically, rats that were placed back into the restraint context but not restrained on day 2 showed enhanced Fos expression in the dentate gyrus suprapyramidal blade (DGSup), and infralimbic cortex (IL). Also Fos expression was attenuated in rats that received two restraint exposures in the IL and medial amygdala (MEA), suggesting habituation. Only the DG infrapyramidal blade (DGInf) showed enhanced Fos expression to restraint on day 2 without influence of the previous day. While context predominately directed Fos activation, prior experience with restraint influenced Fos expression in the DGSup, IL, MEA and corticosterone levels to support restraint having psychological components.
ContributorsAnouti, P. Danya (Author) / Conrad, D. Cheryl (Thesis director) / Hammer, Ronald (Committee member) / Hoffman, N. Ann (Committee member) / Barrett, The Honors College (Contributor) / College of Liberal Arts and Sciences (Contributor)
Created2012-12
152324-Thumbnail Image.png
Description
With robots being used extensively in various areas, a certain degree of robot autonomy has always been found desirable. In applications like planetary exploration, autonomous path planning and navigation are considered essential. But every now and then, a need to modify the robot's operation arises, a need for a human

With robots being used extensively in various areas, a certain degree of robot autonomy has always been found desirable. In applications like planetary exploration, autonomous path planning and navigation are considered essential. But every now and then, a need to modify the robot's operation arises, a need for a human to provide it some supervisory parameters that modify the degree of autonomy or allocate extra tasks to the robot. In this regard, this thesis presents an approach to include a provision to accept and incorporate such human inputs and modify the navigation functions of the robot accordingly. Concepts such as applying kinematical constraints while planning paths, traversing of unknown areas with an intent of maximizing field of view, performing complex tasks on command etc. have been examined and implemented. The approaches have been tested in Robot Operating System (ROS), using robots such as the iRobot Create, Personal Robotics (PR2) etc. Simulations and experimental demonstrations have proved that this approach is feasible for solving some of the existing problems and that it certainly can pave way to further research for enhancing functionality.
ContributorsVemprala, Sai Hemachandra (Author) / Saripalli, Srikanth (Thesis advisor) / Fainekos, Georgios (Committee member) / Turaga, Pavan (Committee member) / Arizona State University (Publisher)
Created2013
151467-Thumbnail Image.png
Description
A semiconductor supply chain modeling and simulation platform using Linear Program (LP) optimization and parallel Discrete Event System Specification (DEVS) process models has been developed in a joint effort by ASU and Intel Corporation. A Knowledge Interchange Broker (KIBDEVS/LP) was developed to broker information synchronously between the DEVS and LP

A semiconductor supply chain modeling and simulation platform using Linear Program (LP) optimization and parallel Discrete Event System Specification (DEVS) process models has been developed in a joint effort by ASU and Intel Corporation. A Knowledge Interchange Broker (KIBDEVS/LP) was developed to broker information synchronously between the DEVS and LP models. Recently a single-echelon heuristic Inventory Strategy Module (ISM) was added to correct for forecast bias in customer demand data using different smoothing techniques. The optimization model could then use information provided by the forecast model to make better decisions for the process model. The composition of ISM with LP and DEVS models resulted in the first realization of what is now called the Optimization Simulation Forecast (OSF) platform. It could handle a single echelon supply chain system consisting of single hubs and single products In this thesis, this single-echelon simulation platform is extended to handle multiple echelons with multiple inventory elements handling multiple products. The main aspect for the multi-echelon OSF platform was to extend the KIBDEVS/LP such that ISM interactions with the LP and DEVS models could also be supported. To achieve this, a new, scalable XML schema for the KIB has been developed. The XML schema has also resulted in strengthening the KIB execution engine design. A sequential scheme controls the executions of the DEVS-Suite simulator, CPLEX optimizer, and ISM engine. To use the ISM for multiple echelons, it is extended to compute forecast customer demands and safety stocks over multiple hubs and products. Basic examples for semiconductor manufacturing spanning single and two echelon supply chain systems have been developed and analyzed. Experiments using perfect data were conducted to show the correctness of the OSF platform design and implementation. Simple, but realistic experiments have also been conducted. They highlight the kinds of supply chain dynamics that can be evaluated using discrete event process simulation, linear programming optimization, and heuristics forecasting models.
ContributorsSmith, James Melkon (Author) / Sarjoughian, Hessam S. (Thesis advisor) / Davulcu, Hasan (Committee member) / Fainekos, Georgios (Committee member) / Arizona State University (Publisher)
Created2012
151793-Thumbnail Image.png
Description
Linear Temporal Logic is gaining increasing popularity as a high level specification language for robot motion planning due to its expressive power and scalability of LTL control synthesis algorithms. This formalism, however, requires expert knowledge and makes it inaccessible to non-expert users. This thesis introduces a graphical specification environment to

Linear Temporal Logic is gaining increasing popularity as a high level specification language for robot motion planning due to its expressive power and scalability of LTL control synthesis algorithms. This formalism, however, requires expert knowledge and makes it inaccessible to non-expert users. This thesis introduces a graphical specification environment to create high level motion plans to control robots in the field by converting a visual representation of the motion/task plan into a Linear Temporal Logic (LTL) specification. The visual interface is built on the Android tablet platform and provides functionality to create task plans through a set of well defined gestures and on screen controls. It uses the notion of waypoints to quickly and efficiently describe the motion plan and enables a variety of complex Linear Temporal Logic specifications to be described succinctly and intuitively by the user without the need for the knowledge and understanding of LTL specification. Thus, it opens avenues for its use by personnel in military, warehouse management, and search and rescue missions. This thesis describes the construction of LTL for various scenarios used for robot navigation using the visual interface developed and leverages the use of existing LTL based motion planners to carry out the task plan by a robot.
ContributorsSrinivas, Shashank (Author) / Fainekos, Georgios (Thesis advisor) / Baral, Chitta (Committee member) / Burleson, Winslow (Committee member) / Arizona State University (Publisher)
Created2013
151653-Thumbnail Image.png
Description
Answer Set Programming (ASP) is one of the most prominent and successful knowledge representation paradigms. The success of ASP is due to its expressive non-monotonic modeling language and its efficient computational methods originating from building propositional satisfiability solvers. The wide adoption of ASP has motivated several extensions to its modeling

Answer Set Programming (ASP) is one of the most prominent and successful knowledge representation paradigms. The success of ASP is due to its expressive non-monotonic modeling language and its efficient computational methods originating from building propositional satisfiability solvers. The wide adoption of ASP has motivated several extensions to its modeling language in order to enhance expressivity, such as incorporating aggregates and interfaces with ontologies. Also, in order to overcome the grounding bottleneck of computation in ASP, there are increasing interests in integrating ASP with other computing paradigms, such as Constraint Programming (CP) and Satisfiability Modulo Theories (SMT). Due to the non-monotonic nature of the ASP semantics, such enhancements turned out to be non-trivial and the existing extensions are not fully satisfactory. We observe that one main reason for the difficulties rooted in the propositional semantics of ASP, which is limited in handling first-order constructs (such as aggregates and ontologies) and functions (such as constraint variables in CP and SMT) in natural ways. This dissertation presents a unifying view on these extensions by viewing them as instances of formulas with generalized quantifiers and intensional functions. We extend the first-order stable model semantics by by Ferraris, Lee, and Lifschitz to allow generalized quantifiers, which cover aggregate, DL-atoms, constraints and SMT theory atoms as special cases. Using this unifying framework, we study and relate different extensions of ASP. We also present a tight integration of ASP with SMT, based on which we enhance action language C+ to handle reasoning about continuous changes. Our framework yields a systematic approach to study and extend non-monotonic languages.
ContributorsMeng, Yunsong (Author) / Lee, Joohyung (Thesis advisor) / Ahn, Gail-Joon (Committee member) / Baral, Chitta (Committee member) / Fainekos, Georgios (Committee member) / Lifschitz, Vladimir (Committee member) / Arizona State University (Publisher)
Created2013