Mikołaj Bojańczyk, Igor Walukiewicz
Forest algebras. Logic and Automata, 2008 PDF
Mikołaj Bojańczyk
Two-Way Unary Temporal Logic over Trees Log. Methods Comput. Sci., 2009 PDF
Mikołaj Bojańczyk, Luc Segoufin, Howard Straubing
Piecewise testable tree languages Log. Methods Comput. Sci., 2012 PDF
Mikołaj Bojańczyk, Luc Segoufin
Tree Languages Defined in First-Order Logic with One Quantifier Alternation Log. Methods Comput. Sci., 2010 PDF
Mikołaj Bojańczyk, Howard Straubing, Igor Walukiewicz
Wreath Products of Forest Algebras, with Applications to Tree Logics Log. Methods Comput. Sci., 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