Rational Verification for Probabilistic Systems
Rational Verification for Probabilistic Systems
复制标题
概率系统的理性验证
DOI：
10.24963/kr.2021/30
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
M. Wooldridge
中科院分区：
文献类型：
--
作者：
Julian Gutierrez;Lewis Hammond;A. Lin;Muhammad Najib;M. Wooldridge
理性验证是确定在多智能体系统中，在系统中的智能体理性行动的假设下，通过选择共同形成博弈论均衡的策略，将持有哪些时间逻辑属性的问题。该领域以前的工作主要集中在确定性系统上。在本文中，我们发展的理论和算法的合理性验证概率系统。我们专注于并发随机游戏（CSG），它可以用来模拟复杂的多智能体环境中的不确定性和随机性。我们在定性概率环境下研究了非合作博弈和合作博弈的理性验证问题。在前一种情况下，我们认为LTL性质满足的纳什均衡的游戏，在后一种情况下，LTL性质满足的核心。在这两种情况下，我们表明，这个问题是2 EXPTIME-完全的，因此不困难比简单得多的验证问题的模型检查LTL属性的系统建模为马尔可夫决策过程（MDPs）。
Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).
DOI：
10.1007/s10009-015-0378-x
发表时间：
2017-02-01
影响因子：
1.5
作者：
Lomuscio, Alessio;Qu, Hongyang;Raimondi, Franco
通讯作者：
Raimondi, Franco