Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version)
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916946337857536 |
|---|---|
| author | Bednarczyk, Bartosz Kieroński, Emanuel |
| author_facet | Bednarczyk, Bartosz Kieroński, Emanuel |
| contents | We study the Guarded Fragment with Regular Guards (RGF), which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2EXPTIME-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying, in a natural sense, the maximal EXPSPACE-complete fragment of RGF. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_09218 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version) Bednarczyk, Bartosz Kieroński, Emanuel Logic in Computer Science We study the Guarded Fragment with Regular Guards (RGF), which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2EXPTIME-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying, in a natural sense, the maximal EXPSPACE-complete fragment of RGF. |
| title | Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.09218 |