用心理博弈建模人类情绪对行为的影响，验证多智能体系统可靠性。
Expectation vs. Reality: Towards Verification of Psychological Games
- 基于信念依赖效用构建心理博弈模型，刻画期望与现实的差距
- 在PRISM-games中实现求解算法，支持随机博弈的形式化验证
- 应用于交通场景中人类行为分析，验证情绪对决策的影响
博弈论为理性代理间的策略交互提供了有效建模方式。在形式化验证背景下，可用于保证多智能体系统的正确性，应用范围涵盖计算机安全到自动驾驶。心理博弈（Psychological Games, PGs）旨在建模具有信念依赖动机的代理，拓展了人类情绪影响行为的分析可能。在PG中，玩家的效用不仅取决于实际发生的结果（所选策略），还取决于其预期结果（对他人策略的信念）。尽管在经济学和心理学领域受到广泛关注，但其在计算机科学中的适用性及实用算法与工具支持仍鲜有研究。本文首次尝试填补这一空白，提出求解心理博弈的方法，并将其集成至PRISM-games——一个用于随机博弈的形式化验证工具。我们讨论了此类博弈的建模方法，指出分析中的特定挑战，并通过多个案例研究展示该方法的实用性，包括人类在交通场景中的行为建模。
原文摘要 · Abstract (English)
Game theory provides an effective way to model strategic interactions among rational agents. In the context of formal verification, these ideas can be used to produce guarantees on the correctness of multi-agent systems, with a diverse range of applications from computer security to autonomous driving. Psychological games (PGs) were developed as a way to model and analyse agents with belief-dependent motivations, opening up the possibility to model how human emotions can influence behaviour. In PGs, players' utilities depend not only on what actually happens (which strategies players choose to adopt), but also on what the players had expected to happen (their belief as to the strategies that would be played). Despite receiving much attention in fields such as economics and psychology, very little consideration has been given to their applicability to problems in computer science, nor to practical algorithms and tool support. In this paper, we start to bridge that gap, proposing methods to solve PGs and implementing them within PRISM-games, a formal verification tool for stochastic games. We discuss how to model these games, highlight specific challenges for their analysis and illustrate the usefulness of our approach on several case studies, including human behaviour in traffic scenarios.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。