| Journal: | Computación y Sistemas |
| Database: | PERIÓDICA |
| System number: | 000457796 |
| ISSN: | 1405-5546 |
| Authors: | Bárcenas, Everardo1 Benítez Guerrero, Edgard2 Lavalle, Jesús3 Molero Castillo, Guillermo1 |
| Institutions: | 1Universidad Nacional Autónoma de México, Ciudad de México. México 2Universidad Veracruzana, Xalapa, Veracruz. México 3Benemérita Universidad Autónoma de Puebla, Puebla. México |
| Year: | 2020 |
| Season: | Ene-Mar |
| Volumen: | 24 |
| Number: | 1 |
| Pages: | 281-303 |
| Country: | México |
| Language: | Inglés |
| Document type: | Artículo |
| Approach: | Aplicado, descriptivo |
| English abstract | The fully enriched μ-calculus is an expressive propositional modal logic with least and greatest fixed-points, nominals, inverse programs and graded modalities. Several fragments of this logic are known to be decidable in EXPTIME. However, the full logic is undecidable. Nevertheless, it has been recently shown that the fully enriched μ-calculus is decidable in EXPTIME when its models are finite trees. In the present work, we study the fully-enriched μ-calculus for trees extended with Presburger constraints. These constraints generalize graded modalities by restricting the number of children nodes with respect to Presburger arithmetic expressions. We show that this extension is decidable in EXPTIME. In addition, we also identify decidable extensions of regular tree languages (XML schemas) with interleaving and counting operators. This is achieved by a linear characterization in terms of the logic. Regular path queries (XPath) with Presburger constraints on children paths are also characterized. These results imply new optimal reasoning (emptiness, containment, equivalence) bounds on counting extensions of XPath queries and XML schemas |
| Disciplines: | Matemáticas |
| Keyword: | Matemáticas aplicadas, Aritmética Presburger, Lógica modal, Razonamiento automatizado, XML, Lenguaje regular, Intercalación |
| Keyword: | Applied mathematics, Presburger arithmetic, Modal logic, Automated reasoning, XML, Regular languages, Interleaving |
| Full text: | Texto completo (Ver HTML) Texto completo (Ver PDF) |
