Many important properties of multi-agent systems refer to the participants' ability to achieve a given goal, or to prevent the system from an undesirable event. Among intelligent agents, the goals are often of epistemic nature, i.e., concern the ability to obtain knowledge about an important fact \phi. Such properties can be e.g. expressed in ATLK, that is, alternating-time temporal logic ATL extended with epistemic operators. In many realistic scenarios, however, players do not need to fully learn the truth value of \phi. They may be almost as well off by gaining some knowledge; in other words, by reducing their uncertainty about \phi. Similarly, in order to keep \phi secret, it is often insufficient that the intruder never fully learns its truth value. Instead, one needs to require that his uncertainty about \phi never drops below a reasonable threshold. With this motivation in mind, we introduce the logic ATLH, extending ATL with quantitative modalities based on the Hartley measure of uncertainty. The new logic enables to specify agents' abilities w.r.t. the uncertainty of a given player about a given set of statements. It turns out that ATLH has the same expressivity and model checking complexity as ATLK. However, the new logic is exponentially more succinct than ATLK, which is the main technical result of this paper.

翻译：多智能体系统的许多重要性质涉及参与者实现给定目标的能力，或防止系统发生不良事件的能力。在智能体中，目标通常具有认知性质，即涉及获取关于重要事实φ的知识的能力。此类性质可表达于ATLK（即扩展了认知算子的交替时序逻辑ATL）中。然而，在许多现实场景中，参与者无需完全获知φ的真值。他们可能通过获取部分知识而获益——换言之，通过减少关于φ的不确定性。同样，为保守φ的秘密，仅要求入侵者从未完全获知其真值往往不够。相反，需要确保其关于φ的不确定性从未低于合理阈值。基于这一动机，我们引入逻辑ATLH，它通过基于哈特利不确定性度量（Hartley measure of uncertainty）的量化模态扩展了ATL。新逻辑能够基于特定参与者关于给定命题集的不确定性来指定其能力。结果证明，ATLH与ATLK具有相同的表达力与模型检验复杂度。然而，ATLH在简洁性上比ATLK呈指数级提升，这是本文的主要技术成果。