Reasoning about memoryless strategies under partial observability and unconditional fairness constraints
Reasoning about memoryless strategies under partial observability and unconditional fairness constraints
复制标题
DOI：
10.1016/j.ic.2015.03.014
复制
发表时间：
2015-06
期刊：
影响因子：
--
通讯作者：
Simon Busard;C. Pecheur;Hongyang Qu;F. Raimondi
中科院分区：
文献类型：
--
作者：
Simon Busard;C. Pecheur;Hongyang Qu;F. Raimondi
摘要交替时序逻辑是一种逻辑推理的策略，代理可以采取实现一个指定的集体目标。这个逻辑存在一些扩展，其中一些联合收割机战略和部分可观性，其他一些包括公平性约束，但据我们所知，没有工作提供了一个统一的框架，战略，部分可观性和公平性约束。这三个概念的整合是很重要的推理时，代理的能力，没有充分的知识的系统，例如，当代理可以假设环境中的行为是一个公平的方式。我们提出了ATLK irF，一个逻辑组合策略下的部分可观性的系统与公平性约束的状态。我们引入了一个模型检测算法ATLK IRF通过扩展算法的全可观性的逻辑变体，我们调查其复杂性。我们验证我们的建议与实验评估。
Abstract Alternating-time Temporal Logic is a logic to reason about strategies that agents can adopt to achieve a specified collective goal. A number of extensions for this logic exist; some of them combine strategies and partial observability, some others include fairness constraints, but to the best of our knowledge no work provides a unified framework for strategies, partial observability and fairness constraints. Integration of these three concepts is important when reasoning about the capabilities of agents without full knowledge of a system, for instance when the agents can assume that the environment behaves in a fair way. We present ATLK irF, a logic combining strategies under partial observability in a system with fairness constraints on states. We introduce a model-checking algorithm for ATLK irF by extending the algorithm for a full-observability variant of the logic and we investigate its complexity. We validate our proposal with an experimental evaluation.