Many problems in compositional synthesis and verification of multi-agent systems -- such as rational verification and assume-guarantee verification in probabilistic systems -- reduce to reasoning about two-player multi-objective stochastic games. This motivates us to study the problem of characterizing the complexity and memory requirements for two-player stochastic games with Boolean combinations of qualitative reachability and safety objectives. Reachability objectives require that a given set of states is reached; safety requires that a given set is invariant. A qualitative winning condition asks that an objective is satisfied almost surely (AS) or (in negated form) with non-zero (NZ) probability. We study the determinacy and complexity landscape of the problem. We show that games with conjunctions of AS and NZ reachability and safety objectives are determined, and determining the winner is PSPACE-complete. The same holds for positive boolean combinations of AS reachability and safety, as well as for negations thereof. On the other hand, games with full Boolean combinations of qualitative objectives are not determined, and are NEXPTIME-hard. Our hardness results show a connection between stochastic games and logics with partially-ordered quantification. Our results shed light on the relationship between determinacy and complexity, and extend the complexity landscape for stochastic games in the multi-objective setting.

翻译：组合式多智能体系统的合成与验证中的许多问题——例如概率系统中的理性验证与假设-保证验证——可归结为对双人多目标随机博弈的推理。这促使我们研究具有定性可达性与安全性目标布尔组合的双人随机博弈的复杂度特征与内存需求问题。可达性目标要求到达给定状态集合；安全性要求给定集合保持不变。定性获胜条件要求目标以几乎必然（AS）或（否定形式）非零（NZ）概率被满足。我们研究了该问题的确定性判定与复杂度图景。我们证明了具有AS与NZ可达性及安全性目标合取的博弈具有确定性，且判定获胜方是PSPACE完全的。这一结论同样适用于AS可达性与安全性的正布尔组合及其否定形式。另一方面，具有定性目标完整布尔组合的博弈不具有确定性，且是NEXPTIME难的。我们的硬度结果揭示了随机博弈与具有偏序量词逻辑之间的联系。本研究结果阐明了确定性与复杂度之间的关系，并拓展了多目标设定下随机博弈的复杂度图景。