Hybrid-Dynamic Ehrenfeucht-Fraisse Games
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918053799788544 |
|---|---|
| author | Badia, Guillermo Gaina, Daniel Knapp, Alexander Kowalski, Tomasz Wirsing, Martin |
| author_facet | Badia, Guillermo Gaina, Daniel Knapp, Alexander Kowalski, Tomasz Wirsing, Martin |
| contents | 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. We also use games to prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_02094 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Hybrid-Dynamic Ehrenfeucht-Fraisse Games Badia, Guillermo Gaina, Daniel Knapp, Alexander Kowalski, Tomasz Wirsing, Martin Logic in Computer Science 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. We also use games to prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism. |
| title | Hybrid-Dynamic Ehrenfeucht-Fraisse Games |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2406.02094 |