Digitala Vetenskapliga Arkivet

RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal methods for verification in human-agent interaction
Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap. (Responsible Artificial Intelligence; Formal Methods for Trustworthy Hybrid Intelligence)ORCID-id: 0000-0001-9379-4281
2025 (Engelska)Doktorsavhandling, monografi (Övrigt vetenskapligt)Alternativ titel
Formella metoder för verifiering i interaktioner mellan människor och intelligenta agenter (Svenska)
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Umeå: Umeå University, 2025. , s. 262
Serie
Report / UMINF, ISSN 0348-0542
Nyckelord [en]
formal verification, human-agent interaction, non-monotonic reasoning, theory of mind
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
datalogi
Identifikatorer
URN: urn:nbn:se:umu:diva-237425ISBN: 978-91-8070-682-7 (tryckt)ISBN: 978-91-8070-683-4 (digital)OAI: oai:DiVA.org:umu-237425DiVA, id: diva2:1950795
Disputation
2025-05-05, HUM.D.220, Humanisthuset, Umeå University, Umeå, 13:15 (Engelska)
Opponent
Handledare
Tillgänglig från: 2025-04-14 Skapad: 2025-04-09 Senast uppdaterad: 2025-04-11Bibliografiskt granskad

Open Access i DiVA

fulltext(4564 kB)517 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 4564 kBChecksumma SHA-512
39e4f4109b66d0731284ffef4f7bd5ab32d51e5b411826893398341cbd6abe6d741ad8c80e6649773f3c4715821d1522ed8f44c1eb43244436c40ae6652bd5b3
Typ fulltextMimetyp application/pdf
spikblad(91 kB)39 nedladdningar
Filinformation
Filnamn SPIKBLAD01.pdfFilstorlek 91 kBChecksumma SHA-512
0099916b20dfa141139de00812be2a1edf632b59836155477967654f04f68cef3d3b6404d0441cbc192c7364fb4fec401c7ceffed13a8fa9ab6a7d866824b85f
Typ spikbladMimetyp application/pdf
About the cover image(203 kB)35 nedladdningar
Filinformation
Filnamn FULLTEXT02.pdfFilstorlek 203 kBChecksumma SHA-512
945cb120f5043227a3f2bd8674b2b6479e95a5edf36c0e6e70c24ee68bc6245f4c75bf9cd0d6f1f2ff1ae3669ed1ce062ab4e1a1276782a2237630c479a9a287
Typ attachmentMimetyp application/pdf

Sök vidare i DiVA

Av författaren/redaktören
Brännström, Andreas
Av organisationen
Institutionen för datavetenskap
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 557 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 984 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf