Abstract:This paper develops a state-based regression method for planning domains with sensing operators and a representation of the knowledge of the planning agent. The language includes primitive actions, sensing actions, and conditional plans. The regression operator is direct in that it does not depend on a progression operator for its formulation. We prove the soundness and completeness of the regression formulation with respect to the definition of progression and the semantics of a propositional modal logic of knowledge. The approach is illustrated with a running example that can not be handled by related methods that utilize an approximation of knowledge instead of the full semantics of knowledge as is used here. It is our expectation that this work will serve as the foundation for the extension of work on state-based regression planning to include sensing and knowledge as well.

Abstract:Intelligent tutoring systems (ITSs) acquire rich data about students' behavior during learning; data mining techniques can help to describe, interpret and predict student behavior, and to evaluate progress in relation to learning outcomes. This paper surveys a variety of data mining techniques for analyzing how students interact with ITSs, including methods for handling hidden state variables, and for testing hypotheses. To illustrate these methods we draw on data from two ITSs for math instruction. Educational datasets provide new challenges to the data mining community, including inducing action patterns, designing distance metrics, and inferring unobservable states associated with learning.

Abstract:Predicting and explaining the behavior of others in terms of mental states is indispensable for everyday life. It will be equally important for artificial agents. We present an inference system for representing and reasoning about mental states, and use it to provide a formal analysis of the false-belief task. The system allows for the representation of information about events, causation, and perceptual, doxastic, and epistemic states (vision,belief, and knowledge), incorporating ideas from the event calculus and multi-agent epistemic logic. Unlike previous AI formalisms, our focus here is on mechanized proofs and proof programmability, not on metamathematical results. Reasoning is performed via relatively cognitively plausible inference rules, and a degree of automation is achieved by generalpurpose inference methods and by a syntactic embedding of the system in first-order logic.

Abstract:Many of the current software systems rely on garbage collectors for automatic memory management. This is also the case for various software systems in real-time appli-cations. However, a real-time application often requires an incremental working style of the underlying garbage collection, which renders the garbage collector more complex and less trustworthy. We present a formal veriˉcation of the Yuasa incremental garbage collector in Hoare-style logic. The speciˉcation and proof of the collector are built on a concrete machine model and cover detailed behaviors of the collector which may lead to safety prob- lems but are often ignored in high-level veriˉcations. The work is fully implemented with the Coq proof assistant and can be packed as foundational proof-carrying-code packages.Our work makes an important step toward providing high-assurance garbage collection for mission-critical real-time systems.

Abstract:Engineering secure software systems requires a thorough understanding of the social setting within which the system-to-be will eventually operate. To obtain such an understanding, one needs to identify the players involved in the system's operation, and to recognize their personal preferences, agendas and powers in relation to other players. The analysis also needs to identify assets that need to be protected, as well as vulnerabilities leads to system failures when attacked. Equally important, the analyst needs to take rational steps to predict most likely attackers, knowing their possible motivations, and capabilities enabled by latest technologies and available resources. Only an integrated social analysis of both sides (attackers/protectors) can reveal the full space of tradeoffs among which the analyst must choose. Unfortunately, current system development practices treat design decisions on security in an ad-hoc way, often as an afterthought. This paper introduces a methodological framework based on i^*, for dealing with security and privacy requirements, namely, Secure-i^*. The framework supports a set of analysis techniques. In particular, attacker analysis helps identify potential system abusers and their malicious intents. Dependency vulnerability analysis helps detect vulnerabilities in terms of organizational relationships among stakeholders. Countermeasure analysis supports the dynamic decision-making process of defensive system players in addressing vulnerabilities and threats. Finally, access control analysis bridges the gap between security requirement models and security implementation models. The framework is illustrated with an example involving security and privacy concerns in the design of electronic health information systems.In addition, we discuss model evaluation techniques, including qualitative goal model analysis and property verification techniques based on model checking.