Standard epistemic logic is concerned with describing agents' epistemic attitudes given the current set of alternatives the agents consider possible. While distributed systems can (and often are) discussed without mentioning epistemics, it has been well established that epistemic phenomena lie at the heart of what agents, or processes, can and cannot do. Dynamic epistemic logic (DEL) aims to describe how epistemic attitudes of the agents/processes change based on the new information they receive, e.g., based on their observations of events and actions in a distributed system. In a broader philosophical view, this appeals to an a posteriori kind of reasoning, where agents update the set of alternatives considered possible based on their "experiences." Until recently, there was little incentive to formalize a priori reasoning, which plays a role in designing and maintaining distributed systems, e.g., in determining which states must be considered possible by agents in order to solve the distributed task at hand, and consequently in updating these states when unforeseen situations arise during runtime. With systems becoming more and more complex and large, the task of fixing design errors "on the fly" is shifted to individual agents, such as in the increasingly popular self-adaptive and self-organizing (SASO) systems. Rather than updating agents' a posteriori beliefs, this requires modifying their a priori beliefs about the system's global design and parameters. The goal of this paper is to provide a formalization of such a priori reasoning by using standard epistemic semantic tools, including Kripke models and DEL-style updates, and provide heuristics that would pave the way to streamlining this inherently non-deterministic and ad hoc process for SASO systems.
翻译:标准认知逻辑关注于描述智能体在当前考虑的备选方案集合下的认知态度。尽管分布式系统可以在不提及认知的情况下进行讨论(且常如此),但已有充分论证表明,认知现象正是智能体(或进程)能力边界的关键所在。动态认知逻辑(DEL)旨在描述智能体/进程如何基于新接收的信息(例如对分布式系统中事件与行动的观察)改变其认知态度。从更广泛的哲学视角看,这诉诸一种后验推理方式——智能体依据"经验"更新其认为可能的备选方案集合。但直到近期,鲜有动力对先验推理进行形式化,而这类推理在分布式系统的设计与维护中发挥着重要作用,例如:确定智能体为解决当前分布式任务必须考虑哪些可能状态,以及在运行时出现未预见情形时相应更新这些状态。随着系统日益复杂庞大,"即时"修复设计错误的任务正逐渐转移至个体智能体——这在日益流行的自适应自组织(SASO)系统中尤为显著。此过程并非更新智能体的后验信念,而是要求修改其对系统全局设计与参数的先验信念。本文旨在利用标准认知语义工具(包括克里普克模型与DEL式更新)为先验推理提供形式化框架,并提出启发式方法,为SASO系统中这一固有非确定性且特设的过程简化铺平道路。