Computational Reasoning for Socially Adaptive Electronic Partners (CoreSAEP)

POST 1 - formal semantics, temporal logic & normative agents

Motivation

The research in this Vidi project lies in the intersection of theoretical computer science (formal semantics, temporal logic) and multi-agent systems (agent programming, normative systems). The overall aim of the project is to develop a reasoning framework that combines logic and quantitative techniques for Socially Adaptive Electronic Partners (SAEPs) that adapt their behavior to norms and values of people. This becomes more and more important with the increasing pervasiveness of mobile devices and sensor technology, which stimulates the development of applications such as GPS technologies for tracking children 24/7, and remote monitoring of elderly to encourage independent living. Such pervasive applications make our lives more connected, efficient and safe, but research in value-sensitive design and ethics of technology has shown that their use carries the risk of violating values such as freedom, responsibility, and privacy. For example, existing systems for locating wandering dementia patients grant a caregiver real-time access to a patient’s location and send alerts if the patient leaves a preset location. This trades the patient’s privacy for safety, and comes with the risk for the caregiver to discover more about the patient’s activities than desired.

It is current practice in software development to address this by making a design time compromise to address value tensions, which does not account for the fact that people’s values play out differently in different situations. The computational reasoning techniques that we will develop in this project address this problem, enabling the creation of SAEPs that can adapt their behavior to people’s norms at run time. The resulting flexibility will allow SAEPs to support people in their daily lives in a way that truly respects their values.

Research challenge

The computational reasoning techniques to be developed in this part of the project are aimed at determining when and to what extent norm-compliance can be guaranteed. The challenge is to develop generic knowledge structures and reasoning techniques that make it easy to create the class of systems represented by the concept of a SAEP. The central question to be answered is the following: which knowledge structures and reasoning techniques are required for SAEPs to decide what to do in order to comply with adopted norms and user goals?

Developing these techniques is challenging because the reasoning needs to be tightly integrated with the SAEP’s execution mechanism for pursuing goals. The aim is to develop an execution semantics that integrates requirements from adopted norms and user goals to decide which action to execute to achieve norm-compliance and avoidance of conflicts between norms and/or goals. Avoidance of conflict is reasoned about during execution as well as during norm adoption. A possible starting point are Van Riemsdijk et al.'s AAMAS'13 and AAMAS'15 paper on reasoning about norm compliance, in which norms are represented as LTL formulas, and techniques from executable temporal logic are used for specifying the integrated execution semantics. An advantage of the use of temporal logic is its expressivity and amenability to formal analysis.

We will combine formal methods for providing rigorous mathematical definitions of knowledge structures and reasoning techniques with implementation of the reasoning framework. This will allow evaluation of the framework through 1) formal analysis of the properties of reasoning techniques, and 2) evaluation of run time behavior of the framework in a variety of prototypical scenarios.

Inquiries

If you are interested in this position, please get in touch with Birna van Riemsdijk via email (m dot b dot vanriemsdijk at tudelft dot nl) and see the CoreSAEP project page and the TU Delft website for details on how to apply.