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

Bartosz BednarczykBartosz Bednarczyk, Oskar FiukOskar Fiuk

ISBN: 978-3-031-15298-6
Download

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

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.
Weitere Informationen unter:Further Information: Link
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},
  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}
}