Learning Models of Sequential Decision-Making with Partial Specification of Agent Behavior

Artificial agents that interact with other (human or artificial) agents require models in order to reason about those other agents’ behavior. In addition to the predictive utility of these models, maintaining a model that is aligned with an agent’s true generative model of behavior is critical for effective human-agent interaction. In applications wherein observations and partial specification of the agent’s behavior are available, achieving model alignment is challenging for a variety of reasons. For one, the agent’s decision factors are often not completely known; further, prior approaches that rely upon observations of agents’ behavior alone can fail to recover the true model, since multiple models can explain observed behavior equally well. To achieve better model alignment, we provide a novel approach capable of learning aligned models that conform to partial knowledge of the agent’s behavior. Central to our approach are a factored model of behavior (AMM), along with Bayesian nonparametric priors, and an inference approach capable of incorporating partial specifications as constraints for model learning. We evaluate our approach in experiments and demonstrate improvements in metrics of model alignment.

Discovering Specifications for Unknown Procedures - Work in Progress

We study automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls or code pointers. Given the specification of a procedure whose body contains calls to an unknown procedure, we try to infer the possible specifications for the unknown procedure from its calling contexts. We employ a forward shape analysis with separation logic and an abductive inference mechanism to synthesize both pre- and postconditions for the unknown procedure. The inferred specification is a partial specification of the unknown procedure. Therefore it is subject to a later verification when the code or the complete specification for the unknown procedure are available. Our inferred specifications can also be used for program understanding.

Finite Position Synthesis of 5-SS Platform Linkages Including Partially Specified Joint Locations

A 5-SS platform linkage generates a one-degree-of-freedom motion of a moving platform such that each of five moving points on the platform is constrained on a sphere, or in its degenerated case, on a plane. It has been well established a 5-SS platform linkage can be made to guide though seven positions exactly. This paper investigates the cases when the number of given positions are less than seven that allows for partial specification of locations of the moving points. A recently developed novel algorithm with linear structure in the design equations has been extended for the solution of the problem. The formulation of this expanded motion generation problem unifies the treatment of the input positions and constraints on the moving and fixed joints associated with the 5-SS platform linkage. Numerical examples are provided to show the effectiveness of the unified algorithm.

Probabilistic Analysis of the Impact of Vessel Speed Restrictions on Navigational Safety: Accounting for the Right Whale Rule

The Right Whale Sighting Advisory System (RWSAS) is a National Oceanic and Atmospheric Administration (NOAA) Fisheries program designed to reduce collisions between vessels and critically endangered North Atlantic right whales. The vessel speed restriction that is part of the RWSAS presents navigation stakeholders with numerous challenges, owing to concerns about increased risks of ship grounding and collisions within ports. In this paper, we present a multi-methodology framework for assessing the impact of the vessel speed restriction on navigational safety. Empirically, we base our discussion in a first-order analysis of ship grounding risk for the Charleston Entrance Channel. Our analysis proceeds in three parts. We begin by using fault and event tree analyses to assess a relevant set of grounding-related event progression and failure probabilities. The influence of alternative vessel speed restrictions on ship grounding risk are then explored via a Bayesian network model that utilises the previously specified fault and event tree models for its partial specification and enumeration. Our analysis suggests that the speed restriction can, under certain reasonable assumptions, be seen to adversely impact the risk of ship grounding accidents in the Charleston Entrance Channel. We conclude with a summary of our findings and recommendations for future research.

Behavioural reasoning for conditional equations

Object-oriented (OO) programming techniques can be applied to equational specification logics by distinguishing visible data from hidden data (that is, by distinguishing the output of methods from the objects to which the methods apply), and then focusing on the behavioural equivalence of hidden data in the sense introduced by H. Reichel in 1984. Equational specification logics structured in this way are called hidden equational logics, HELs. The central problem is how to extend the specification of a given HEL to a specification of behavioural equivalence in a computationally effective way. S. Buss and G. Roşu showed in 2000 that this is not possible in general, but much work has been done on the partial specification of behavioural equivalence for a wide class of HELs. The OO connection suggests the use of coalgebraic methods, and J. Goguen and his collaborators have developed coinductive processes that depend on an appropriate choice of a cobasis, which is a special set of contexts that generates a subset of the behavioural equivalence relation. In this paper the theoretical aspects of coinduction are investigated, specifically its role as a supplement to standard equational logic for determining behavioural equivalence. Various forms of coinduction are explored. A simple characterisation is given of those HELs that are behaviourally specifiable. Those sets of conditional equations that constitute a complete, finite cobasis for a HEL are characterised in terms of the HEL's specification. Behavioural equivalence, in the form of logical equivalence, is also an important concept for single-sorted logics, for example, sentential logics such as the classical propositional logic. The paper is an application of the methods developed through the extensive work that has been done in this area on HELs, and to a broader class of logics that encompasses both sentential logics and HELs.

Improving the Quality of Requirements with Refactoring

Requirements specification can often exhibit some shortcomings, regarding contents and organization of its partial specification elements. Sometimes, modularization is deficient, with modules dealing with too much information, or the same functionality being specified in different modules. Left unchecked, these inadequacies will propagate themselves to the subsequent phases of the software development and cause problems during maintenance. We have been able to identify a collection of typical deficiencies in the specification of structured documents and we propose a collection of refactorings that minimize or remove them. Doing this early in the development process increases requirements modularity and understandability. A case study is conducted to illustrate the use of these refactoring practices on two existing requirement documents.