The Semantic Web lays its foundations on the study of graph and tree logics. One of the most expressive graph logics is the fully enriched μ-calculus, which is a modal logic equipped with least and greatest fixed-points, nominals, inverse programs and graded modalities. Although it is well-known that the fully enriched μ-calculus is undecidable, it was recently shown that this logic is decidable 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 the logic is decidable in EXPTIME. This is achieved by the introduction of a satisfiability algorithm based on a Fischer-Ladner model construction that is able to handle binary encodings of Presburger constraints. © Springer-Verlag 2013.
CITATION STYLE
Bárcenas, E., & Lavalle, J. (2013). Expressive reasoning on tree structures: Recursion, inverse programs, presburger constraints and nominals. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8265 LNAI, pp. 80–91). https://doi.org/10.1007/978-3-642-45114-0_7
Mendeley helps you to discover research relevant for your work.