In this paper, we investigate the probabilistic variants of the strategy logics ATL and ATL* under imperfect information. Specifically, we present novel decidability and complexity results when the model transitions are stochastic and agents play uniform strategies. That is, the semantics of the logics are based on multi-agent, stochastic transition systems with imperfect information, which combine two sources of uncertainty, namely, the partial observability agents have on the environment, and the likelihood of transitions to occur from a system state. Since the model checking problem is undecidable in general in this setting, we restrict our attention to agents with memoryless (positional) strategies. The resulting setting captures the situation in which agents have qualitative uncertainty of the local state and quantitative uncertainty about the occurrence of future events. We illustrate the usefulness of this setting with meaningful examples.

翻译：本文研究了不完美信息下策略逻辑ATL和ATL*的概率变体。具体而言，当模型转移具有随机性且主体采用统一策略时，我们提出了新的可判定性与复杂度结果。即，这些逻辑的语义基于具有不完美信息的多主体随机转移系统，该系统融合了两种不确定性来源：主体对环境的局部可观测性，以及系统状态转移发生的可能性。由于在此设定下模型检测问题通常不可判定，我们将关注点限制于采用无记忆（位置型）策略的主体。由此得到的框架刻画了主体对局部状态具有定性不确定性，并对未来事件的发生具有定量不确定性的场景。我们通过有意义的示例说明了该框架的实用性。