Umeå University's logo

Formal verification is essential for ensuring that systems behave according to their mathematical specifications. However, applying formal verification to human-agent interactions presents unique challenges due to the dynamic nature of human mental states and behaviors. Unlike traditional verification tasks, which focus on ensuring correctness in a well-defined action space, this work addresses reasoning over beliefs, intentions, and emotions that evolve through interaction. Two main contributions are introduced: (1) Belief Graphs for modeling mental state dynamics, and (2) the integration of these with formal dialogue games for verifying strategies and influence. To this end, the developed verification methods are rooted in two main pillars: psychological theories formalized to represent mental state dynamics as logical frameworks, and Non-Monotonic Reasoning (NMR) methods, including techniques such as Formal Argumentation and Answer Set Programming (ASP). By modeling  mental dynamics as states and transitions in a layer atop the action space—referred to as the Belief Graph methodology—we are provided a tool for modeling context and context dynamics that supports counterfactual, forward and backward reasoning about mental states and behaviors. By incorporating Belief Graphs into formal dialogue games we gain mathematical frameworks for analyzing and verifying agent beliefs, intentions and strategies, thereby enabling the verification of human-agent interactions.Whether it concerns potentially harmful human behaviors—such as malicious activities on social media—or intelligent systems that interact with humans, such as chatbots that are increasingly capable of influencing users’ emotions, thoughts, and decisions—there is an urgent need for formal verification methods to ensure safe and reliable human interactions in digital communication.The proposed methods have been evaluated through formal analysis, case studies, and published peer-reviewed research.

Interactive software agents, such as chatbots, are progressively being used in the area of health and well-being. In such applications, where agents engage with users in interpersonal conversations for, e.g., coaching, comfort or behavior-change interventions, there is an increased need for understanding agents’ empathic capabilities. In the current state-of-the-art, there are no tools to do that. In order to understand empathic capabilities in interactive software agents, we need a precise notion of empathy. The literature discusses a variety of definitions of empathy, but there is no consensus of a formal definition. Based on a systematic literature review and a qualitative analysis of recent approaches to empathy in interactive agents for health and well-being, a formal definition—an ontology—of empathy is developed. We present the potential of the formal definition in a controlled user-study by applying it as a tool for assessing empathy in two state-of-the-art health and well-being chatbots; Replika and Wysa. Our findings suggest that our definition captures necessary conditions for assessing empathy in interactive agents, and how it can uncover and explain trends in changing perceptions of empathy over time. The definition, implemented in Web Ontology Language (OWL), may serve as an automated tool, enabling systems to recognize empathy in interactions—be it an interactive agent evaluating its own empathic performance or an intelligent system assessing the empathic capability of its interlocutors.

In this paper, we propose a new computational model for affective knowledge representation that will be used for affective agents located in a multicultural environment. To this end, we present the results of two experiments, the first of which determines the most appropriate labels to define the pleasure-arousal dimensions in the culture and language of the agent's location. As an example, we use the Portuguese and Swedish languages. The second experiment identifies the most suitable values of pleasure-arousal dimensions for each emotion expressed in these example languages. The results obtained are compared with a previous model developed for agents interacting with European Spanish-speaking people. Results show significant differences in the values of pleasure and arousal associated with emotions across languages and cultures. The results also show no significant differences in gender or age when associating levels of pleasure-arousal to emotions. We propose two applications of these representation models, such as a model of an agent capable of adapting its affective behavior to different cultural environments and a human-aware planning scenario in which the agent uses this dimensional representation to recognize the user's affective state and select the best strategy to redirect that affective state to the target state.

Humans have evolved to seek social connections, extending beyond interactions with living beings. The digitization of society has led to interactions with non-living entities, such as digital companions, aimed at supporting mental well-being. This literature review surveys the latest developments in digital companions for mental health, employing a hybrid search strategy that identified 67 relevant articles from 2014 to 2022. We identified that by the nature of the digital companions’ purposes, it is important to consider person profiles for: a) to generate both person-oriented and empathetic responses from these virtual companions, b) to keep track of the person’s conversations, activities, therapy, and progress, and c) to allow portability and compatibility between digital companions. We established a taxonomy for digital companions in the scope of mental well-being. We also identified open challenges in the scope of digital companions related to ethical, technical, and socio-technical points of view. We provided documentation about what these issues mean, and discuss possible alternatives to approach them.

This work aims to utilize quantitative bipolar argumentation to detect deception in machine learning models. We explore the concept of deception in the context of interactions of a party developing a machine learning model with potentially malformed data sources. The objective is to identify deceptive or adversarial data and assess the effectiveness of comparative analysis during different stages of model training. By modeling disagreement and agreement between data points as arguments and utilizing quantitative measures, this work proposes techniques for detecting outliers in data. We discuss further applications in clustering and uncertainty modelling.

This paper presents a survey of software for computational argumentation, focusing on tools and libraries that can be re-used for building applications. The (so far preliminary) survey is intended as a continuously updated resource that researchers and potential practitioners can refer to when selecting tools for their argumentation use cases. The survey results indicate that while a plethora of argumentation tools exist, covering various formal argumentation approaches, the software engineering maturity of the tool ecosystem is low. For example, while many tools are openly available, few are properly documented and covered by automated tests. We argue that many of these shortcomings can be straightforwardly addressed by following simple engineering practices if community consensus regarding basic requirements for software artifacts can be established, as is the case in software engineering-oriented communities.

We consider a type of information-seeking dialogue between a seeker agent and a respondent agent, where the seeker estimates the respondent to not be willing to share a particular set of sought-after information. Hence, the seeker postpones (hides) its goal topic, related to the respondent's sensitive information, until the respondent is perceived as willing to talk about it. In the intermediate process, the seeker opens other topics to steer the dialogue tactfully towards the goal. Such dialogue strategies, which we refer to as goal-hiding strategies, are common in diverse contexts such as criminal interrogations and medical assessments, involving sensitive topics. Conversely, in malicious online interactions like social media extortion, similar strategies might aim to manipulate individuals into revealing information or agreeing to unfavorable terms. This paper proposes a formal dialogue framework for understanding goal-hiding strategies. The dialogue framework uses Quantitative Bipolar Argumentation Frameworks (QBAFs) to assign willingness scores to topics. An initial willingness for each topic is modified by considering how topics promote (support) or demote (attack) other topics. We introduce a method to identify relations among topics by considering a respondent's shared information. Finally, we introduce a gradual semantics to estimate changes in willingness as new topics are opened. Our formal analysis and empirical evaluation show the system's compliance with privacy-preserving safety properties. A formal understanding of goal-hiding strategies opens up a range of practical applications; For instance, a seeker agent may plan with goal-hiding to enhance privacy in human-agent interactions. Similarly, an observer agent (third-party) may be designed to enhance social media security by detecting goal-hiding strategies employed by users' interlocutors.

Indoor interventions are among the most dangerous situations police officers have to deal with, mostly due to a lack of situational awareness. This work describes a planner that determines when to provide information, implemented in DLV^K. It is based on the General Tactical Explanation Model, used by Swedish police during tactical interventions. The planner is envisioned to be integrated in an augmented reality tool to enhance officers’ situational awareness.

This paper introduces an automated decision-making framework for providing controlled agent behavior in systems dealing with human behavior-change. Controlled behavior in such settings is important in order to reduce unexpected side-effects of a system’s actions. The general structure of the framework is based on a psychological theory, the Theory of Planned Behavior (TPB), capturing causes to human motivational states, which enables reasoning about dynamics of human motivation. The framework consists of two main components: 1) an ontological knowledge-base that models an individual’s behavioral challenges to infer motivation states and 2) a transition system that, in a given motivation state, decides on motivational support, resulting in transitions between motivational states. The system generates plans (sequences of actions) for an agent to facilitate behavior change. A particular use-case is modeled regarding children with Autism Spectrum Conditions (ASC) who commonly experience difficulties in everyday social situations. An evaluation of a proof-of-concept prototype is performed that presents consistencies between ASC experts’ suggestions and plans generated by the system.

This paper introduces a formal framework for goal-hiding information-seeking dialogues to deal with interactions where a seeker agent estimates a human respondent to not be willing to share the sought-for information. Hence, the seeker postpones (hides) a sensitive goal topic until the respondent is perceived willing to talk about it. This regards a type of deceptive strategy to withhold information, e.g., a sensitive question, that, in a given dialogue state, may be harmful to a respondent, e.g., by violating privacy. The framework uses Quantitative Bipolar Argumentation Frameworks to assign willingness scores to topics, inferred from a respondent's asserted beliefs. A gradual semantics is introduced to handle changes in willingness scores based on relations among topics. The goal-hiding dialogue process is illustrated using an example inspired by primary healthcare nurses' strategies for collecting sensitive health information from patients.