Ehrenfeucht-Fra\"iss\'e games provide means to characterize elementary equivalence for first-order logic, and by standard translation also for modal logics. We propose a novel generalization of Ehrenfeucht- Fra\"iss\'e games to hybrid-dynamic logics which is direct and fully modular: parameterized by the features of the hybrid language we wish to include, for instance, the modal and hybrid language operators as well as first-order existential quantification. We use these games to establish a new modular Fra\"iss\'e-Hintikka Theorem for hybrid-dynamic propositional logic and its various fragments. We study the relationship between countable game equivalence (determined by countable Ehrenfeucht- Fra\"iss\'e games) and bisimulation (determined by countable back-and-forth systems). In general, the former turns out to be weaker than the latter, but under certain conditions on the language, the two coincide. We also use games to prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism.

翻译：Ehrenfeucht-Fraïssé博弈为刻画一阶逻辑的基本等价性提供了方法，并通过标准转换同样适用于模态逻辑。我们提出了一种针对混合动态逻辑的Ehrenfeucht-Fraïssé博弈新推广方法，该方法直接且完全模块化：其参数化取决于我们希望包含的混合语言特征，例如模态与混合语言算子以及一阶存在量化。我们利用这些博弈为混合动态命题逻辑及其各类片段建立了新的模块化Fraïssé-Hintikka定理。我们研究了可数博弈等价性（由可数Ehrenfeucht-Fraïssé博弈决定）与互模拟关系（由可数往返系统决定）之间的关联。一般而言，前者弱于后者，但在特定语言条件下两者具有一致性。我们还通过博弈证明了对于可达的像有限Kripke结构，基本等价性蕴含同构关系。