| Revue: | Computación y sistemas |
| Base de datos: | PERIÓDICA |
| Número de sistema: | 000383503 |
| ISSN: | 1405-5546 |
| Autores: | Bárcenas, Everardo1 |
| Instituciones: | 1Universidad Veracruzana, Jalapa, Veracruz. México |
| Año: | 2015 |
| Periodo: | Abr-Jun |
| Volumen: | 19 |
| Número: | 2 |
| Paginación: | 407-422 |
| País: | México |
| Idioma: | Inglés |
| Tipo de documento: | Artículo |
| Enfoque: | Analítico, descriptivo |
| Resumen en inglés | It has been recently shown that the fully enriched µ-calculus, an expressive modal logic, is undecidable. In the current work, we prove that this result does not longer hold when considering finite tree models. This is achieved with the introduction of an extension of the fully enriched µ-calculus for trees with numerical constraints. Contrastively with graded modalities, which restrict the occurrence of immediate successor nodes only, the logic introduced in this paper can concisely express numerical constraints on any tree region, as for instance the ancestor or descendant nodes. In order to show that the logic is in EXPTIME, we also provide a corresponding satisfiability algorithm. By succinct reductions to the logic, we identify several decidable extensions of regular tree languages with counting and interleaving operators. It is also shown that XPath extensions with counting constructs on regular path queries can be concisely captured by the logic. Finally, we show that several XML reasoning problems (XPath queries with schemas), such as emptiness and containment, can be optimally solved with the satisfiability algorithm |
| Disciplinas: | Ciencias de la computación |
| Palabras clave: | Procesamiento de datos, Razonamiento automatizado, Lógica modal, Lenguajes formales |
| Keyword: | Computer science, Data processing, Automated reasoning, Modal logic, Formal languages |
| Texte intégral: | Texto completo (Ver HTML) |
