Nicolas Markey

Abstract

We introduce a new class of automata (which we coin EU-automata) running on infininte trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata.

We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logic QCTL (which extends CTL with quantification over atomic propositions) and for MSO. On the one hand, we obtain decision procedures with optimal complexity for QCTL satisfiability and model checking; on the other hand, we obtain an algorithm for translating any QCTL formula with k quantifier alternations to formulas with at most one quantifier alternation, at the expense of a (k+1)-exponential blow-up in the size of the formulas. Using the same techniques, we prove that any MSO formula can be translated into a formula with at most four quantifier alternations (and only two second-order-quantifier alternations), again with a (k+1)-exponential blow-up in the size of the formula.

@techreport{arxiv2410.18799-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Arbitrary-arity Tree Automata and QCTL},
  number =              {2410.18799},
  year =                {2024},
  month =               oct,
  doi =                 {10.48550/arXiv.2410.18799},
  institution =         {arXiv},
  abstract =            {We~introduce a new class of automata (which we coin
                         \emph{EU-automata}) running on infininte trees of
                         arbitrary (finite) arity. We~develop and study
                         several algorithms to perform classical operations
                         (union, intersection, complement, projection,
                         alternation removal) for those automata, and
                         precisely characterise their complexities. We~also
                         develop algorithms for solving membership and
                         emptiness for the languages of trees accepted by
                         EU-automata. \par We~then use EU-automata to obtain
                         several algorithmic and expressiveness results for
                         the temporal logic \textsf{QCTL} (which extends
                         \textsf{CTL} with quantification over atomic
                         propositions) and for \textsf{MSO}. On the one hand,
                         we obtain decision procedures with optimal
                         complexity for \textsf{QCTL} satisfiability and
                         model checking; on the other hand, we obtain an
                         algorithm for translating any \textsf{QCTL} formula
                         with \(k\) quantifier alternations to formulas with
                         at most one quantifier alternation, at~the~expense
                         of a \((k+1)\)-exponential blow-up in the size of
                         the formulas. Using the same techniques, we~prove
                         that any \textsf{MSO} formula can be translated into
                         a formula with at most four quantifier alternations
                         (and only two second-order-quantifier alternations),
                         again with a \((k+1)\)-exponential blow-up in the
                         size of the formula.},
}