SHF: Medium: Collaborative Research: Formal Analysis and Synthesis of Multiagent Systems with Incentives

该项目开发了工具辅助设计和分析具有激励作用的多代理系统的自动化方法。这些系统是真实世界情况下的自然模型，在现实世界中，参与者集合以自主和自利的方式相互作用。例如，这样的系统可以对参与诸如广告拍卖或加密货币之类的基于互联网的协议的一组软件代理、共享物理或数字基础设施的一组机器人、或参与进化过程的一组细胞进行建模。该项目将博弈论和逻辑方法结合起来，开发用于此类系统的形式化建模、分析、验证和综合的技术。该项目的最终目标包括管理自治代理之间相互作用的可靠协议的设计，以及对自然发生的博弈论相互作用的计算机辅助理解。该项目的技术方法有三个维度。首先是发展新的形式模型，正确性要求，抽象和推理原则，激励多主体系统。研究方向包括多智能体系统中更丰富的均衡概念，以及相互作用和随机化对均衡的影响。其次，该项目研究算法工具，用于分析和验证具有激励的多智能体系统，以满足关于系统行为和均衡的期望要求。第三个方向是自动综合机构，以保证所需的性能。来自金融协议、机器人和生物学等一系列领域的应用程序被用来指导和评估这项研究。

The project develops automated methods for the tool-aided design and analysis of multi-agent systems with incentives. These systems are natural models for real-world situations in which collections of actors interact with one another in an autonomous and self-interested manner. For example, such a system can model a set of software agents that participate in an internet-based protocol, such as an advertisement auction or crypto currency; a collection of robots that share physical or digital infrastructure; or a set of cells that participate in an evolutionary process. The project combines game-theoretic and logical methods to develop techniques for formal modeling, analysis, verification, and synthesis of such systems. The end objectives of the project include reliable engineering of protocols that govern interactions among autonomous agents, and computer-aided understanding of naturally occurring game-theoretic interactions.The technical approach of the project has three dimensions. The first is the development of new formal models, correctness requirements, and abstraction and reasoning principles for multi-agent systems with incentives. Research directions include richer notions of equilibria in multi-agent systems, and effects of interaction and randomization on equilibria. Second, the project studies algorithmic tools for analysis and verification of multi-agent systems with incentives with respect to desired requirements regarding system behaviors and equilibria. The third direction is to automatically synthesize mechanisms so as to guarantee desired properties. Applications from a range of areas, including financial protocols, robotics, and biology, are used to guide and evaluate the research.