Mikołaj Bojańczyk

Algebra for finite trees


July 14, 2015
  1. Mikołaj Bojańczyk, Igor Walukiewicz
    Forest algebras. Logic and Automata, 2008   PDF

  2. Mikołaj Bojańczyk
    Two-Way Unary Temporal Logic over Trees Logical Methods in Computer Science, 2009   PDF

  3. Mikołaj Bojańczyk, Luc Segoufin, Howard Straubing
    Piecewise testable tree languages Logical Methods in Computer Science, 2012   PDF

  4. Mikołaj Bojańczyk, Luc Segoufin
    Tree Languages Defined in First-Order Logic with One Quantifier Alternation Logical Methods in Computer Science, 2010   PDF

  5. Mikołaj Bojańczyk, Howard Straubing, Igor Walukiewicz
    Wreath Products of Forest Algebras, with Applications to Tree Logics Logical Methods in Computer Science, 2012   PDF

The main motivation for this group of papers is the following decision problem, whose decidability remains open: decide if a given regular language of finite trees can be defined by a formula of first-order logic that uses predicates for the labels and the descendant relation. In other words, the question is about the tree version of the Schützenberger theorem. Since Schützenberger was so successful with monoids, we thought it would be a good idea to introduce something like monoids for trees, which is the topic of paper [1] that introduces forest algebra. Unfortunately, we were unable to use these monoids to characterize all of first-order logics, but at least some fragments can be described in terms of structural properties of the underlying forest algebras. A survey of algebras for trees can be found here, it is supposed to appear in an upcoming but much-delayed Handbook of Automata Theory.

Forest algebra is a proposal for an algebraic structure describing trees. The idea is to have finitely many sorts (as opposed to the infinitely many sorts of a clone or operad), and to have a set of operations that is independent of the input alphabet (as opposed to the universal algebra approach to finite trees, where the signature depends on the ranked alphabet at hand). Our solution has two sorts, and uses unranked trees.  The paper [1] introduces forest algebra. It also shows that forest algebra and the idea of using unranked trees can simplify notation and allow for conceptually cleaner proofs. The specific example used is the temporal logic EF, which has a straightforward characterization using forest algebra, but which has a nasty one in the case of ranked trees, as shown here

  • Mikołaj Bojańczyk, Igor Walukiewicz
    Characterizing EF and EX tree logics. Theor. Comput. Sci., 2006   PDF

As mentioned at the beginning of this page, the long term goal of this topic is to give an algorithm deciding if a regular language of finite trees can be defined in first-order logic. The papers [2,3,4] give such algorithms, but fragments of first order logic, typically obtained by limiting the quantification pattern. These papers are journal versions of:

  • Mikołaj Bojańczyk
    Two-way unary temporal logic over trees. LICS, 2007   PDF

  • Mikołaj Bojańczyk, Luc Segoufin, Howard Straubing
    Piecewise Testable Tree Languages. LICS, 2008   PDF

  • Mikołaj Bojańczyk, Luc Segoufin
    Tree Languages Defined in First-Order Logic with One Quantifier Alternation. ICALP (2), 2008   PDF

Finally, paper [5] presents an alternative syntax for first-order logic, in terms of wreath products, but without an algorithm deciding whether or not a language can be defined in the logic. The underlying idea is the by-now classical connection between: a) first-order logic; b) temporal logics in the style of CTL*; c) sequential compositions of automata/algebras. The paper is a journal version of:

  • Mikołaj Bojańczyk, Howard Straubing, Igor Walukiewicz
    Wreath Products of Forest Algebras, with Applications to Tree Logics. LICS, 2009   PDF

 

 

 

Leave a Reply

Your email address will not be published.