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

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

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

Bartosz BednarczykBartosz Bednarczyk,  Oskar FiukOskar Fiuk
Bartosz Bednarczyk, Oskar Fiuk
Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting
Technical Report, ICCL, May 2022. Technical Report
  • 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 Logic
@techreport{BF2022,
  author      = {Bartosz Bednarczyk and Oskar Fiuk},
  title       = {Presburger B{\"{u}}chi Tree Automata with Applications to
                 Logics with Expressive Counting},
  institution = {ICCL},
  year        = {2022},
  month       = {May}
}