This note sketches the extension of the basic characterisation theorems as the bisimulation-invariant fragment of first-order logic to modal logic with graded modalities and matching adaptation of bisimulation. We focus on showing expressive completeness of graded multi-modal logic for those first-order properties of pointed Kripke structures that are preserved under counting bisimulation equivalence among all or among just all finite pointed Kripke structures.

翻译：本文概述了将基本特征定理（即一阶逻辑的互模拟不变片段）扩展到带有分级模态词的模态逻辑及相应互模拟适配的过程。我们聚焦于证明分级多模态逻辑的表达完备性：对于所有（或仅所有有限）带标记的克里普克结构，那些在计数互模拟等价关系下被保持的一阶性质。