Mikołaj Bojańczyk

July 14, 2015

Mikołaj Bojańczyk, Igor Walukiewicz

*Forest algebras.*Logic and Automata, 2008 PDFMikołaj Bojańczyk

*Two-Way Unary Temporal Logic over Trees*Logical Methods in Computer Science, 2009 PDFMikołaj Bojańczyk, Luc Segoufin, Howard Straubing

*Piecewise testable tree languages*Logical Methods in Computer Science, 2012 PDFMikołaj Bojańczyk, Luc Segoufin

*Tree Languages Defined in First-Order Logic with One Quantifier Alternation*Logical Methods in Computer Science, 2010 PDFMikoł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 PDFMikołaj Bojańczyk, Luc Segoufin, Howard Straubing

*Piecewise Testable Tree Languages.*LICS, 2008 PDFMikoł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