Beyond Regularity for Presburger Modal Logics
| Title | Beyond Regularity for Presburger Modal Logics |
| Publication Type | Conference Paper |
| Year of Publication | 2012 |
| Authors | Carreiro, F, Demri, S |
| Conference Name | 9th Workshop on Advances in Modal Logics (AiML'12) |
| Date Published | 08/2012 |
| Publisher | College Publications |
| Conference Location | Copenhagen, Denmark |
| Keywords | context-free constraint, decidability, Presburger constraint |
| Abstract | Satisability problem for modal logic K with quantier-free Presburger and regularity constraints (EML) is known to be pspace-complete. In this paper, we consider its extension with nonregular constraints, and more specically those expressed by visibly pushdown languages (VPL). This class of languages behaves nicely, in particular when combined with Propositional Dynamic Logic (PDL). By extending EML, we show that decidability is preserved if we allow at most one positive VPL-constraint at each modal depth. However, the presence of two VPL-contraints or the presence of a negative occurrence of a single VPL-constraint leads to undecidability. These results contrast with the decidability of PDL augmented with VPL-constraints. Keywords: Presburger constraint, context-free constraint, decidability |
| URL | http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-aiml12.pdf |
| Refereed Designation | Refereed |
PDF (Full text):
Work Package:
WP2
