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）方法中，对多种已实现的修复与状态恢复技术进行建模时的实用性与灵活性。