Human Emotion Verification by Action Languages via Answer Set Programming

AI summary

Overview

Research area: Knowledge representation and reasoning — specifically action languages, Answer Set Programming (ASP), and computational models of human mental states (Theory of Mind, emotion).

Technical level: Advanced. The paper is a formal-methods contribution: it introduces a new action language with syntax and semantics, translations into ASP, and formal properties such as invariance. Readers need comfort with logic programming, transition systems, and non-monotonic reasoning.

One-sentence scope: The paper defines C_MT (Mind Transition Language), an ASP-based action language for representing, constraining, verifying, and comparing how human mental states evolve in response to sequences of observable actions.

What This Paper Is About

Interactive AI systems increasingly try to display human-like traits such as empathy and to influence how people feel, but there is little formal machinery for verifying that an interaction does not push a person into harmful mental states. The authors address this by treating mental states (such as emotions) as multi-dimensional configurations drawn from psychological theory, and by adding a new constraint construct — forbids to cause — that rules out certain mental-state transitions regardless of which action occurred. The goal is a framework in which an agent's available action sequences are filtered by principles of valid mental change, so unwanted mental side effects can be detected and avoided.

Key Contributions

1. A new action language, C_MT (Mind Transition Language). It refines the fluent and action alphabet of the existing action language C_TAID into observable environmental fluents (F^E) and actions (A^E) versus non-observable mental fluents (F^H) and human actions (A^H), providing a foundational platform for mental-state reasoning.

2. Syntax, semantics, and an ASP implementation. The paper presents the domain description language D^MT(A, F), specializations of C_TAID constructs (influences, facilitates, contravenes, mirroring causes, allows, inhibits), and the novel forbids to cause rule, together with a characterization under answer set semantics. The framework is evaluated formally and empirically.

3. The Belief Graph (BG) abstraction and its use for specifying psychological principles. A BG is a directed graph BG = (S, E) whose nodes are mental states (combinations of mental fluents f(c, v)) and whose edges are valid transitions. Sets of forbids-to-cause rules, layered on dynamic causal laws, define the BG, which filters trajectories produced by the action language. Characterizations are given for Roseman's Appraisal Theory of Emotion, Hedonic Emotion Regulation (HER), and Utilitarian Emotion Regulation (UER).

4. A method for representing, verifying, and comparing psychological theories. Because different theories encode different principles of change, the framework lets trajectories that adhere to different principles be compared, supporting principle-based assessment of agent behavior.

Main Findings

• Mental states can be modeled as multi-dimensional configurations. A mental fluent is a ground atom f(c, v) with c a psychological class and v a value from a totally ordered set V_c; the mental state space S is the union over all value combinations. In Roseman's appraisal theory the relevant variables include need-consistency, goal-consistency, accountability, and control potential.

• A new constraint type is needed beyond existing action languages. The forbids to cause rule (g_1^h, …, g_m^h forbids to cause f_1^h, …, f_n^h) states that if certain mental fluents hold at time t, then certain other mental fluents are forbidden at time t+1. The paper argues that this is not expressible in C_TAID, and that it is essential because (1) actions may directly induce undesirable changes in mental fluents and (2) such changes may indirectly trigger unwanted ramifications on other mental fluents.

• Principles of mental change become transition constraints and invariants. Psychological principles are translated into transition constraints and properties of invariance — in transition-system terms, a property that must hold in all states along every possible trajectory. Trajectories are the object of analysis rather than isolated transitions.

• Contrasting emotion-regulation theories produce different valid dynamics. Hedonic Emotion Regulation aims to increase positive emotions and decrease negative emotions, whereas Utilitarian Emotion Regulation aims to increase emotions that provide utility, such as control. A BG is agnostic to which theory is chosen, which is what enables comparison.

• The framework rests on a deliberate contrast with statistical user modeling. Statistical user modeling approximates a user from snapshots (interaction history, demographics), which can become stale as the user's state changes during an interaction. ASP is non-deterministic, yielding multiple answer sets that are filtered by constraints; the paper frames ASP as suited to emotional reasoning because it can express NP-search problems solved by a nondeterministic Turing machine in polynomial time, with solutions encoded as answer sets.

• The paper is an extended version of two prior works, augmented with a generalized formalism and methods for representing, analyzing, and comparing psychological theories in terms of action languages.

• Experimental specifics are not present in the provided content. The paper's structure assigns the experimental evaluation to Section 7 and a human-emotion-verification example to Section 8, but the truncated content does not report any experimental setups, datasets, benchmarks, timings, or quantitative results. Section 5 (case study) and Section 6 (formal analysis) results are likewise not available here.

Methodology in Plain English

The researchers take an existing action language designed for biological systems, C_TAID, and adapt it to the human mind. They split the vocabulary in two: things a system can observe about the environment and do there, and things going on inside a person that cannot be observed directly, like emotions. Actions in the environment can influence the unobservable mental variables, and human actions can be made easier (facilitates) or discouraged (contravenes) by the person's mental state.

On top of that, they add a rule that says: if the mind looks a certain way now, then it is simply not allowed to look a certain other way next. Collections of these rules define a Belief Graph — a map of which mental states may follow which others. Because the whole thing is written so it can be compiled into Answer Set Programming, a solver enumerates possible trajectories (sequences of actions and resulting states) and discards any trajectory that violates the rules. Psychological theories supply the contents of the rules: the appraisal theory supplies the dimensions of the mental state, and emotion-regulation theories such as hedonic and utilitarian regulation supply the transition prohibitions. Properties like invariance are then checked over all trajectories, and trajectories generated under one theory can be compared with those generated under another.

Why This Matters

Impact on research. The paper targets a gap it identifies explicitly: psychological theories such as emotion regulation describe patterns of mental-state change, but formal models rarely integrate those patterns as transition constraints or invariants that can be rigorously evaluated. It also argues that modal-logic approaches typically reduce emotions to atomic propositions (for example "Joy" or "Sadness") rather than multi-variable configurations with structured interdependencies, limiting expressivity about causes, constraints, and consequences of transitions. C_MT offers a constraint-based, trajectory-level alternative.

Real-world applications:

• Conversational agents for depression support, therapy, and behavior-change interventions, where modeling and constraining mental-state transitions is described as essential for coherent and safe interactions.
• Systems that deliver emotionally charged actions or aim to provoke empathic responses from users, which need to anticipate and reduce unwanted influence.
• Verifying and preventing unsafe forms of influence in human–AI interaction; the paper cites the documented case of an individual sentenced to nine years for attempting to assassinate Queen Elizabeth II after exchanging thousands of messages with a chatbot that appeared to encourage his violent intentions.
• User modeling and personalization in interactive systems, where snapshot-based statistical models can go stale mid-interaction and lead to uncontrolled agent behavior.

Industry relevance. Developers of mental-health and wellbeing software, conversational AI, and socially aware agents need assurance mechanisms for the emotional consequences of their systems. The framework's ASP encoding gives a concrete route to checking, before deployment, whether an agent's planned interactions can drive a user into forbidden mental states.

Future Directions

• Filling in and extending the empirical evaluation of the ASP implementation, which the paper assigns to Section 7 but which is not described in the available content.
• Broadening the case study beyond the three theories used here (Roseman's Appraisal Theory of Emotion, Hedonic Emotion Regulation, Utilitarian Emotion Regulation) to other psychological accounts, since the language is stated to be general and instantiable with alternative theories.
• Operationalizing theory comparison at scale: the framework supports comparing trajectories that adhere to different psychological principles, but how to adjudicate between competing theories on that basis remains open.
• The paper states that Section 10 concludes and outlines directions for future work, but the specific directions are not included in the truncated content.

Target Audience

Researchers and graduate students in knowledge representation, logic programming, and non-monotonic reasoning; formal-methods researchers working on verification of agent behavior; and interdisciplinary readers in affective computing and computational models of Theory of Mind who want psychological theories expressed as machine-checkable transition constraints. Practitioners building mental-health, conversational, or socially aware agents will find the modeling patterns useful, but the paper assumes prior familiarity with ASP and action languages.

Authors’ abstract

In this paper, we introduce the action language C-MT (Mind Transition Language). It is built on top of answer set programming (ASP) 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. With the objective to address the need for controlled agent behaviors and to restrict unwanted mental side-effects of actions, we extend the language with a novel causal rule, forbids to cause, along with expressions specialized for mental state dynamics, which enables the modeling of principles for valid transitions between mental states. These principles of mental change are translated into transition constraints, and properties of invariance, which are rigorously evaluated using transition systems in terms of so-called trajectories. This enables controlled reasoning about the dynamic evolution of human mental states. Furthermore, the framework supports the comparison of different dynamics of change by analyzing trajectories that adhere to different psychological principles. We apply the action language to design models for emotion verification. Under consideration in Theory and Practice of Logic Programming (TPLP).