期望与现实：向心理游戏验证迈进

博弈论提供了有效的方法来建模理性代理人之间的战略互动。在形式化验证的背景下，这些思想可以用于产生对多代理系统正确性的保证，广泛应用于计算机安全、自动驾驶等领域。心理博弈（PG）是一种用于建模和分析具有信念依赖动机的代理人的工具，开拓了建模人类情感如何影响行为的可能性。在PG中，玩家的效用不仅取决于实际发生的事情（即玩家选择采纳的策略），也取决于玩家过去预期发生的事情（即他们对将要采纳的策略的信念）。尽管该领域在经济学和心理学等领域受到广泛关注，但针对计算机科学问题的适用性，以及实际算法和工具支持方面的考虑仍寥寥无几。本文旨在弥合这一差距，提出解决PG的方法，并将其实现于PRISM-games中，该工具是用于随机博弈的形式化验证工具。我们讨论了如何建模这些博弈，突出其分析的特定挑战，并通过包括人类交通情景中的行为等多个案例研究说明我们方法的有用性。