Presburger Constraints in Trees

Authors

  • Everardo Barcenas Universidad Nacional Autónoma de México
  • Edgard Benítez Guerrero Universidad Veracruzana
  • Jesús Lavalle Benemérita Universidad Autónoma de Puebla
  • Guillermo Molero Castillo Universidad Nacional Autónoma de México

DOI:

https://doi.org/10.13053/cys-1-1-2940

Keywords:

Presburger arithmetic, modal logics, automated reasoning, XPath, regular languages, interleaving

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 alinear 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 XPathqueries and XML schemas.

Author Biographies

Everardo Barcenas, Universidad Nacional Autónoma de México

Researcher at Conacyt. Ph. D. from INRIA.

Edgard Benítez Guerrero, Universidad Veracruzana

Professor

Jesús Lavalle, Benemérita Universidad Autónoma de Puebla

Professor

Guillermo Molero Castillo, Universidad Nacional Autónoma de México

Researcher

Downloads

Published

2020-03-25

Issue

Vol. 24 No. 1 (2020): 24(1)2020

Section

Articles

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.