Hybrid-Dynamic Ehrenfeucht-Fraisse Games
Guillermo Badia, Daniel Gaina, Alexander Knapp, Tomasz Kowalski, Martin Wirsing

TL;DR
This paper introduces a flexible, modular extension of Ehrenfeucht-Fraisse games tailored for hybrid-dynamic logics, enabling new characterizations of logical equivalence and relationships with bisimulation.
Contribution
It presents a novel, parameterized game framework for hybrid-dynamic logics, establishing a modular Fraisse-Hintikka Theorem and analyzing the connection between game equivalence and bisimulation.
Findings
Countable game equivalence is generally weaker than bisimulation.
Under certain conditions, game equivalence coincides with bisimulation.
Elementary equivalence implies isomorphism for reachable image-finite Kripke structures.
Abstract
Ehrenfeucht-Fraisse 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- Fraisse 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 Fraisse-Hintikka Theorem for hybrid-dynamic propositional logic and its various fragments. We study the relationship between countable game equivalence (determined by countable Ehrenfeucht- Fraisse 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.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsStochastic processes and financial applications · Simulation Techniques and Applications · Markov Chains and Monte Carlo Methods
