具有数据类型的关系多智能体系统的验证（扩展版）
Verification of Relational Multiagent Systems with Data Types (Extended Version)
摘要：
我们研究的关系多智能体系统（RMASs），其中代理人操纵成熟的关系数据库，数据类型和方面配备了特定领域的，刚性的关系（如总订单）的扩展。具体来说，我们专注于设计时验证的RMASs对丰富的一阶时间属性表示的一阶μ演算的一个变种，量化跨状态。我们建立在以前的可判定性结果下的“状态有界”的假设，即，在每个单个状态中，只有有限数量的数据对象被存储在代理数据库中，而随着时间的推移，可以遇到无限多的数据对象。我们重铸这种情况下，在存在密集的，线性的订单，并在他们上面定义的方面显示可判定性。我们的方法是基于建设的有限状态，健全和完整的抽象的原始系统，其中密集的线性订单被重新制定为非刚性的关系，仅在系统的活动域上工作。我们还显示不可判定性时，包括一个数据类型配备了后继关系。
英文摘要：
We study the extension of relational multiagent systems (RMASs), where agents manipulate full-fledged relational databases, with data types and facets equipped with domain-specific, rigid relations (such as total orders). Specifically, we focus on design-time verification of RMASs against rich first-order temporal properties expressed in a variant of first-order mu-calculus with quantification across states. We build on previous decidability results under the "state-bounded" assumption, i.e., in each single state only a bounded number of data objects is stored in the agent databases, while unboundedly many can be encountered over time. We recast this condition, showing decidability in presence of dense, linear orders, and facets defined on top of them. Our approach is based on the construction of a finite-state, sound and complete abstraction of the original system, in which dense linear orders are reformulated as non-rigid relations working on the active domain of the system only. We also show undecidability when including a data type equipped with the successor relation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
