BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//WASP-HS - ECPv6.15.17//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:WASP-HS
X-ORIGINAL-URL:https://wasp-hs.org
X-WR-CALDESC:Events for WASP-HS
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Stockholm
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20240331T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20241027T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20250330T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20251026T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20260329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20261025T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Stockholm:20250505T130000
DTEND;TZID=Europe/Stockholm:20250505T170000
DTSTAMP:20260605T103059
CREATED:20250423T183327Z
LAST-MODIFIED:20250423T183327Z
UID:19268-1746450000-1746464400@wasp-hs.org
SUMMARY:PhD Defense – Formal methods for verification in human-agent interaction
DESCRIPTION:Andreas Brännström\, defends his doctoral thesis “Formal methods for verification in human-agent interaction“\, at Umeå University. \nAbstract\nFormal 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. \nRead full thesis. \nSupervisor\nJuan Carlos Nieves Sanchez\, Docent in theoretical foundations for artificial intelligence \nRead more about the defence. \nOpponent\nStefania Costantini\, Professor at University of L’Aquila\, Italy.
URL:https://wasp-hs.org/event3/phd-defense-formal-methods-for-verification-in-human-agent-interaction/
ATTACH;FMTTYPE=image/jpeg:https://wasp-hs.org/wp-content/uploads/2025/04/Andreas-Brannstrom-PhD-Defence-webb.jpg
END:VEVENT
END:VCALENDAR