# Global Numerical Constraints on Trees

@article{Brcenas2014GlobalNC, title={Global Numerical Constraints on Trees}, author={E. B{\'a}rcenas and J. Lavalle-Mart{\'i}nez}, journal={Log. Methods Comput. Sci.}, year={2014}, volume={10} }

We introduce a logical foundation to reason on tree structures with
constraints on the number of node occurrences. Related formalisms are limited
to express occurrence constraints on particular tree regions, as for instance
the children of a given node. By contrast, the logic introduced in the present
work can concisely express numerical bounds on any region, descendants or
ancestors for instance. We prove that the logic is decidable in single
exponential time even if the numerical constraints… Expand

#### 19 Citations

A Counting Logic for Trees

- Mathematics, Computer Science
- Computación y Sistemas
- 2015

It is proved that the fully enriched μ -calculus, an expressive modal logic, is undecidable when considering finite tree models, and several XML reasoning problems, such as emptiness and containment, can be optimally solved with the satisfiability algorithm. Expand

Query reasoning on data trees with counting

- Computer Science
- LANMR
- 2016

An EXPTIME extension of regular paths with data tests and counting operators is identified in terms of a closed under negation Presburger tree logic, which applies for standard query reasoning. Expand

On Regular Paths with Counting and Data Tests

- Mathematics, Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2016

An EXPTIME extension of regular paths with data tests and counting operators is identified in terms of a closed under negation Presburger tree logic, which applies for standard query reasoning. Expand

Depth-First Reasoning on Trees

- Computer Science
- Computación y Sistemas
- 2018

This paper proposes a satisfiability algorithm for the mu-calculus extended with converse modalities and interpreted on unranked trees based on a depth-first search and proves the algorithm to be correct (sound and complete) and optimal. Expand

Reasoning on expressive description logics with arithmetic constraints

- Mathematics, Computer Science
- 2016 International Conference on Electronics, Communications and Computers (CONIELECOMP)
- 2016

It is shown that μALCTIO, which is known to be undecidable and that subsumes ALCQIOreg, is inEXPTIME in the case of tree models, and that knowledge base reasoning, TBoxes and ABoxes, can also be decided in EXPTIME. Expand

A Satisfiability Algorithm For The Mu-Calculus For Trees With Presburger Constraints

- Computer Science
- 2019 7th International Conference in Software Engineering Research and Innovation (CONISOFT)
- 2019

A satisfiability algorithm for the $\mu-$calculus interpreted on tree models and extended with converse modalities and Presburger arithmetic operators, based on a breadth-first search in a Fischer-Lardner construction of tree models is described. Expand

On the Model Checking of the Graded μ-calculus on Trees

- Mathematics, Computer Science
- MICAI
- 2015

A linear-time model checking algorithm for the graded \(\mu \)-calculus when models are finite unranked trees is introduced. Expand

(Hyper)sequent Calculi for the ALC(S4) Description Logics

- Computer Science
- Computación y Sistemas
- 2016

This paper proposes a cut-free tree hypersequent calculus for terminological reasoning in the Description Logic ALC and shows it is sound and complete, and a complexity analysis and an implementation are provided. Expand

Hyper)sequent Calculi for the ALC(S4) Description Logics

- Mathematics
- 2016

Description logics (DL) form a well-known family of knowledge representation languages. One of its main applications is on the Semantic Web as a reasoning framework in the form of the Ontology Web… Expand

CTL* with graded path modalities

- Computer Science
- Inf. Comput.
- 2018

The significance of this work is that G is much more expressive than as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity. Expand

#### References

SHOWING 1-10 OF 37 REFERENCES

Query Reasoning on Trees with Types, Interleaving, and Counting

- Mathematics, Computer Science
- IJCAI
- 2011

This work considers the problem of query containment in the presence of type constraints for a class of regular path queries extended with counting and interleaving operators, and provides a logic-based framework supporting these operators which can be used to solve common query reasoning problems such as satisfiability and containment of queries in exponential time. Expand

Efficient static analysis of XML paths and types

- Computer Science
- PLDI '07
- 2007

An algorithm to solve XPath decision problems under regular tree type constraints and its use to statically type-check XPath queries is presented and the decidability of a logic with converse for finite ordered trees is proved. Expand

Node Selection Query Languages for Trees

- Computer Science
- AAAI
- 2010

The study of node-selection query languages for (finite) trees has been a major topic in the recent research on query languages for Web documents. On one hand, there has been an extensive study of… Expand

A logic you can count on

- Computer Science
- POPL '04
- 2004

We prove the decidability of the quantifier-free, static fragment of ambient logic, with composition adjunct and iteration, which corresponds to a kind of regular expression language for… Expand

Counting in Trees for Free

- Mathematics, Computer Science
- ICALP
- 2004

It is shown here that a decidable logic is obtained if the authors use a modal fixpoint logic instead of Presburger tree automata and how it can be used to express numerical document queries. Expand

The Emptiness Problem for Tree Automata with Global Constraints

- Computer Science, Mathematics
- 2010 25th Annual IEEE Symposium on Logic in Computer Science
- 2010

The decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality is proved. Expand

Regular expression types for XML

- Computer Science
- ICFP '00
- 2000

The subtyping algorithm developed here is a variant of Aiken and Murphy's set-inclusion constraint solver, to which are added several optimizations and two new properties: the algorithm is provably complete, and it allows a useful "subtagging" relation between nodes with different labels in XML trees. Expand

Conditional XPath

- Computer Science
- TODS
- 2005

It is shown that there exists a natural expansion of Core XPath in which every first-order definable path in XML document trees is expressible, and this expansion is called Conditional XPath. Expand

Numerical document queries

- Mathematics, Computer Science
- PODS '03
- 2003

It is sketched how classical monadic second-order logic by Presburger predicates can be extended also to answer questions like, e.g., whether the total price of the jazz music downloaded so far exceeds a user's budget. Expand

Automata-based verification of programs with tree updates

- Mathematics, Computer Science
- Acta Informatica
- 2009

This paper describes a verification framework for Hoare-style pre- and post-conditions of programs manipulating balanced tree-like data structures, and shows that, under few restrictions, one can automatically compute the effect of tree-updating program statements on the set of configurations represented by a TASC, which makes TASC a practical verification tool. Expand