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

From International Center for Computational Logic

Toggle side column

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

Bartosz BednarczykBartosz Bednarczyk,  Oskar FiukOskar Fiuk
Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting


Bartosz Bednarczyk, Oskar Fiuk
Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting
In Agata Ciabattoni, Elaine Pimentel, Ruy J. G. B. de Queiroz, eds., Proceedings of the 28th Workshop on Logic, Language, Information and Computation (WOLLIC 2022), volume 2022 of Logic, Language, Information, and Computation, 295--308, September 2022. Springer International Publishing
  • 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.
  • Weitere Informationen unter:Other info: Link
  • Forschungsgruppe:Research Group: Computational Logic
@inproceedings{BF2022,
  author    = {Bartosz Bednarczyk and Oskar Fiuk},
  title     = {Presburger B{\"{u}}chi Tree Automata with Applications to Logics
               with Expressive Counting},
  editor    = {Agata Ciabattoni and Elaine Pimentel and Ruy J. G. B. de Queiroz},
  booktitle = {Proceedings of the 28th Workshop on Logic, Language, Information
               and Computation (WOLLIC 2022)},
  series    = {Logic, Language, Information, and Computation},
  volume    = {2022},
  publisher = {Springer International Publishing},
  year      = {2022},
  month     = {September},
  pages     = {295--308}
}