We provide an epistemic logical language and semantics for the modeling and analysis of byzantine fault-tolerant multi-agent systems. This not only facilitates reasoning about the agents' fault status but also supports model updates for implementing repair and state recovery. For each agent, besides the standard knowledge modality our logic provides an additional modality called hope, which is capable of expressing that the agent is correct (not faulty), and also dynamic modalities enabling change of the agents' correctness status. These dynamic modalities are interpreted as model updates that come in three flavours: fully public, more private, or involving factual change. We provide complete axiomatizations for all these variants in the form of reduction systems: formulas with dynamic modalities are equivalent to formulas without. Therefore, they have the same expressivity as the logic of knowledge and hope. Multiple examples are provided to demonstrate the utility and flexibility of our logic for modeling a wide range of repair and state recovery techniques that have been implemented in the context of fault-detection, isolation, and recovery (FDIR) approaches in fault-tolerant distributed computing with byzantine agents.

翻译：我们提出了一种用于建模与分析拜占庭容错多智能体系统的认知逻辑语言与语义框架。该框架不仅支持对智能体故障状态的推理，还支持通过模型更新实现修复与状态恢复。针对每个智能体，除标准知识模态外，我们的逻辑还引入了一种称为"希望"的附加模态，用以表达智能体处于正确（非故障）状态，同时提供动态模态以实现智能体正确性状态的变更。这些动态模态被解释为三种类型的模型更新：完全公开型、半私有型及涉及事实变更型。我们以归约系统的形式为所有变体提供了完备的公理化体系：含有动态模态的公式等价于不含动态模态的公式。因此，其表达能力与知识-希望逻辑保持相同。本文通过多个示例展示了该逻辑在建模各类修复与状态恢复技术时的实用性与灵活性，这些技术已在拜占庭智能体容错分布式计算领域的故障检测、隔离与恢复（FDIR）方法中得到实际应用。