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.

翻译：我们提出了一种用于建模和分析拜占庭容错多智能体系统的认知逻辑语言及其语义。该逻辑不仅有助于推理智能体的故障状态，还能通过模型更新支持修复与状态恢复的实现。对于每个智能体，除标准的知识模态外，我们的逻辑还提供了一种名为“希望”（hope）的额外模态，能够表达智能体处于正确（无故障）状态，同时引入动态模态以实现智能体正确性状态的变更。这些动态模态被解释为三种类型的模型更新：完全公开更新、更私密更新或涉及事实变更的更新。我们以归约系统的形式为所有变体提供了完全公理化：包含动态模态的公式等价于不含动态模态的公式。因此，它们与“知识与希望”逻辑具有相同的表达能力。通过多个示例，我们展示了该逻辑在建模拜占庭智能体容错分布式计算中故障检测、隔离与恢复（FDIR）方法所实现的多种修复与状态恢复技术时的实用性与灵活性。