Umeå University's logo

In this paper, we introduce the action language C-MT (Mind Transition Language), built on top of answer set programs and transition systems to represent how human mental states evolve in response to sequences of observable actions. Drawing on well-established psychological theories, such as the Appraisal Theory of Emotion, we formalize mental states, such as emotions, as multi-dimensional configurations. To enable controlled agent behavior and limit undesirable effects such as undue psychological influence, we introduce a novel causal rule, forbids to cause, together with constructs tailored to mental state dynamics. These allow the specification of valid transitions as constraints and invariance properties, which are rigorously evaluated over trajectories in transition systems. The framework supports reasoning about and comparing different dynamics of mental change under varying constraints. We apply the action language to design models for emotion verification.

With the arrival of Large Language Models (LLMs), there is an explosion of agents characterised in terms of LLM-prompts. But LLMs lack consistency with their answers, and they are prone to hallucinations. This means that LLM-based agents are erratic agents. Hence, there are no guarantees that LLM-based agents will be aligned with an expected behaviour. We argue that formal dialogue verification is the way to go for minimising the potential negative side effects of erratic LLM-based agents. Erratic LLM-based agents are far from complying with basic Trustworthy AI principles such as technical robustness and safety. Formal Dialogue Verification methods provide rigorous mathematical frameworks for verifying fundamental behavioral properties of LLM-based agents.

Medication management is a daily and time-consuming task for hospital nurses. It includes searching for generic substitutions in online databases when a prescribed drug is not available, and also searching for specific drugs in the actual medication room to find where it is physically located. In co-creation with stakeholders an Augmented Reality-based companion was created, which resides in a holographic device that can be worn during practice and assists nurses through a holographic, mixed reality environment, supporting the task of medication management in a comfortable way. Ethical assessment of the system, conducted using the AI4EU assessment tool, highlighted key strengths of the system and also identified areas for improvement, particularly in transparency legislative clarity. A challenge for user testing in clinical environments is that hospital medication rooms are strictly regulated. To enable future user studies a Medication Room Simulator was developed.

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.

The analysis of abrasive wear is central to sustainable material design and tool development, yet current practice relies on manual inspection of scanning electron microscopy (SEM) images, limiting scalability and reproducibility. We propose early work towards a neuro-symbolic approach that integrates convolutional neural networks for SEM image segmentation with an expert-elicited taxonomy of wear features encoded in Answer Set Programming. A curated dataset of 400 laboratory and field SEM images with expert-labeled annotations supports interpretable detection of wear mechanisms. This approach aims to reduce the dependency on large datasets, increase interpretability, in automated abrasive wear analysis. The contribution opens the way for scalable and transparent decision processes in tribology, with implications for efficient materials development and extended service life of industrial tools.

Designing Artificial Intelligence (AI)-based interactive systems for law enforcement poses unique socio-technical and ethical challenges, particularly when such systems must support real-time decision-making in dynamic, high-stakes environments. Despite their potential, AI-supported interactive systems in policing require carefully elicited domain-specific requirements to ensure effective use while being Ethical by Design. However, methods for such requirement elicitation remain limited. This paper presents a participatory approach for identifying the requirements of AI-driven Mixed Reality (MR) systems in law enforcement contexts. The introduced methodology builds on two of our previous EU projects: the Erasmus+ project "Trustworthy AI", which provided educational material to teach key principles of Trustworthy AI, and AI4EU, which developed an abbreviated assessment tool for evaluating AI systems. In collaboration with police education units and law enforcement agencies in Sweden and Catalonia, we conducted a multi-phase study involving two preparatory workshops—one focused on educating participants in Trustworthy AI, and another involving hands-on MR use in standard police training scenarios. This reflects the view that it is not enough to simply ask people about new technologies—they must also be educated to critically assess their implications. After the workshops, we collected structured feedback using quantitative and qualitative methods. To analyze risk levels of the elicited requirements, we applied the AI4EU-based assessment tool. Our findings highlight key challenges and opportunities for designing AI-based systems with MR interfaces that enhance decision-making in real-time police operations while ensuring transparency, safety, and human oversight.

The “right to contest” decisions that have consequences on individuals or the society is a well-established democratic right. Contesting a decision is not a matter of simply providing an explanation, but rather of assessing whether the decision and the explanation are permissible against an organization's governance framework. Yet, albeit the popularity of adjacent fields, little work has been explicitly done on contesting AI decisions. In this paper, we propose that formal argumentation can be used to formulate contestations of decisions made by artificial agents. We extend the discourse on socio-ethical values in AI by conceptualizing our argumentation framework as a formal dialogue, enabling the interaction between humans and agents as decisions are being contested.

In cooperative human decision-making, agreements are often not total; a partial degree of agreement is sufficient to commit to a decision and move on, as long as one is somewhat confident that the involved parties are likely to stand by their commitment in the future, given no drastic unexpected changes. In this paper, we introduce the notion of agreement scenarios that allow artificial autonomous agents to reach such agreements, using formal models of argumentation, in particular abstract argumentation and value-based argumentation. We introduce the notions of degrees of satisfaction and (minimum, mean, and median) agreement, as well as a measure of the impact a value in a value-based argumentation framework has on these notions. We then analyze how degrees of agreement are affected when agreement scenarios are expanded with new information, to shed light on the reliability of partial agreements in dynamic scenarios. An implementation of the introduced concepts is provided as part of an argumentation-based reasoning software library.

We introduce a formal framework for recognizing manipulation in human-agent interactions, where one agent gradually influences another's beliefs. To this end, we extend Quantitative Bipolar Argumentation Frameworks (QBAFs) by incorporating agents' beliefs about arguments, attacks, and supports, forming QBAF with Belief (QBAFB). By defining axioms of belief change and integrating QBAFB into dialogue games, we establish conditions for manipulation-belief change, concealment, and intent-where strategies are shaped by (dis)honesty. The framework generates belief state trajectories, serving as explanations for manipulation.

In this paper, we apply formal dialogue methods to recognize and analyze phishing in interactions. Phishing attacks exploit human vulnerabilities, typically through deceptive and manipulative messages, leading victims to disclose sensitive information. Existing machine learning-based detection methods often lack transparency, making it difficult to trace manipulation tactics. We utilize the so-called Goal-Hiding Dialogue (GHD) framework, originally designed for reasoning about non-collaborative agents in information-seeking dialogues. The framework employs Quantitative Bipolar Argumentation Frameworks (QBAFs) to model how a seeker agent strategically influences a target’s willingness to engage with certain topics. Our approach provides a mathematically grounded method for identifying key conversational shifts where manipulation occurs, contributing to phishing detection and evidence analysis.