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，通过基于哈特利不确定性测度的量化模态扩展了ATL。新逻辑能够针对给定玩家关于给定陈述集的不确定性来指定智能体的能力。结果表明，ATLH具有与ATLK相同的表达力和模型检测复杂度。然而，新逻辑比ATLK在简洁性上呈指数级提升，这是本文的主要技术成果。