Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting

Bartosz BednarczykBartosz Bednarczyk, Oskar FiukOskar Fiuk

Download

Bartosz Bednarczyk, Oskar Fiuk
Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting
Proceedings of the 28th Workshop on Logic, Language, Information and Computation (WOLLIC 2022), to appear

Details
Bibtex

KurzfassungAbstract
We introduce two versions of Presburger Automata with the Büchi acceptance condition, working over infinite, finite-branching trees. These automata, in addition to the classical ones, allow nodes for checking linear inequalities over labels of their children. We establish tight NP and ExpTime bounds on the complexity of the non-emptiness problem for the presented machines. We demonstrate the usefulness of our automata models by polynomially encoding the two-variable guarded fragment extended with Presburger constraints, improving the existing triply-exponential upper bound to a single exponential.
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{BF2022,
  author    = {Bartosz Bednarczyk and Oskar Fiuk},
  title     = {Presburger B{\"{u}}chi Tree Automata with Applications to Logics
               with Expressive Counting},
  booktitle = {Proceedings of the 28th Workshop on Logic, Language, Information
               and Computation (WOLLIC 2022)},
  year      = {2022},
  month     = {September}
}