Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Subject "Formal methods"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    A formal investigation of the organization of guidance behavior: implications for humans and autonomous implications for humans and autonomous
    (2012-10) Kong, Zhaodan
    Guidance behavior generated either by artificial agents or humans has been actively studied in the fields of both robotics and cognitive science. The goals of these two fields are different. The former is the automatic generation of appropriate or even optimal behavior, while the latter is the understanding of the underlying mechanism. Their challenges, though, are closely related, the most important one being the lack of a unified, formal and grounded framework where the guidance behavior can be modeled and studied. This dissertation presents such a framework. In this framework, guidance behavior is analyzed as the closed-loop dynamics of the whole agent-environment system. The resulting dynamics give rise to interaction patterns. The central points of this dissertation are that: first of all, these patterns, which can be explained in terms of symmetries that are inherent to the guidance behavior, provide building blocks for the organization of behavior; second, the existence of these patterns and humans' organization of their guidance behavior based on these patterns are the reasons that humans can generate successful behavior in spite of all the complexities involved in the planning and control. This dissertation first gives an overview of the challenges existing in both scientific endeavors, such as human and animal spatial behavior study, and engineering endeavors, such as autonomous guidance system design. It then lays out the foundation for our formal framework, which states that guidance behavior should be interpreted as the collection of the closed-loop dynamics resulting from the agent's interaction with the environment. The following, illustrated by examples of three different UAVs, shows that the study of the closed-loop dynamics should not be done without the consideration of vehicle dynamics, as is the common practice in some of the studies in both autonomous guidance and human behavior analysis. The framework, the core concepts of which are symmetries and interaction patterns, is then elaborated on with the example of Dubins' vehicle's guidance behavior. The dissertation then describes the details of the agile human guidance experiments using miniature helicopters, the technique that is developed for the analysis of the experimental data and the analysis results. The results confirm that human guidance behavior indeed exhibits invariance as defined by interaction patterns. Subsequently, the behavior in each interaction pattern is investigated using piecewise affine model identification. Combined, the results provide a natural and formal decomposition of the behavior that can be unified under a hierarchical hidden Markov model. By employing the languages of dynamical system and control and by adopting algorithms from system identification and machine learning, the framework presented in this dissertation provides a fertile ground where these different disciplines can meet. It also promises multiple potential directions where future research can be headed.
  • Thumbnail Image
    Item
    Oral history interview with Karl Levitt
    (Charles Babbage Institute, 2013-06-06) Levitt, Karl
    Computer security pioneer discusses his educational background and early career, with the bulk of the interview on his approximately four decades plus focus on computer security research. He discusses his work with fault-tolerant systems, the institutional setting and his research and management roles at SRI (including PSOS, IDES/NIDES, etc.). He also discusses joining the faculty at UC-Davis in Computer Science and launching its Computer Security Laboratory, which has been influential in educating and placing computer security specialists in academe, government, and industry. Also discussed is his post-IDES/NIDES work on intrusion detection, voting systems and security, federal funding for computer security, his program manager role for Trustworthy Computing at NSF, and other topics. This material is based upon work supported by the National Science Foundation under Grant No. 1116862, “Building an Infrastructure for Computer Security History.”
  • Thumbnail Image
    Item
    Safe Multi-Agent Planning Under Time-Window Temporal Logic Specifications
    (2020-05) Peterson, Ryan
    This thesis addresses a multi-agent planning problem, where each agent aims to achieve an individual task while avoiding collisions with other agents in the environment. It is assumed that each agent's task is expressed as a Time-Window Temporal Logic (TWTL) specification defined over a 3D environment. A distributed receding horizon algorithm is introduced for online planning of trajectories. Under mild assumptions on the environment topology, the resulting agent trajectories are always safe (collision-free) and lead to the satisfaction of the TWTL specifications or their finite temporal relaxations. Accordingly, each agent is guaranteed to safely achieve its task while avoiding deadlocks. Performance of the proposed algorithm is demonstrated via numerical simulations and through experiments with quadrotors.