Fixed-point Logics and Reasoning about Trees (FLiRT)
The workshop will gather young researchers and world top experts in various areas of theoretical
computer science related to fixed-point logics. These areas include automata theory,
game theory, web languages and coalgebras. The event will be hosted by the Institute for Logic,
Language and Computation (ILLC) of the University of Amsterdam (UvA) and will take place
in the Euclides building (Plantage Muidergracht 24, Room P.020).
More about FLiRT
The FLiRT workshop will coincide with the public PhD defenses of Gaëlle Fontaine
and Amélie Gheerbrant, whose theses are both in the field of computational logic.
More specifically, both theses focus on the phenomenon of recursion, which is prominent in computer science, mathematics,
logic and other areas such as game theory and linguistics. Fixed-point logics are a modern
tool to give a logical formalization of recursion and have considerable applications in computer
science. Both theses study proof-theoretical and model-theoretical aspects, such as completeness
or definability, of particular fixed-point logics, including μ-calculus and fixed-point extensions of
first-order logic. The techniques used emphasize the strong link with other areas.
The purpose of this workshop is to bring together researchers from all these different areas.
For instance, automata theory has given a very insightful understanding of fixed-point formulas.
This connection has also found many applications in the field of verification. Majority of industrial
strength verification packages are based on translation of logical formulas to automata.
Game theory provides another major area for recursion, as recursive procedures play a
crucial role in game theory. Fixed-point logics are also very important in complexity theory and
for the foundations of database theory and XML. In the context of XML, there is a particular
focus on trees, which serve as the standard theoretical abstraction of XML documents. Fixed-point
logics have also been extended to the setting of coalgebras, which generalize the notion of state-based
evolving systems, such as words and trees. The workshop aims to provide a forum for
discussing current developments in the area.
- Valentin Goranko
Title: "Seeing the forest for the trees: a glimpse through first-order logic"
Abstract: With every class of linear orders one can uniformly define several naturally associated classes of trees, which, in general, may
have different first-order theories. I will discuss these classes of trees, will present some general results about the axiomatization of their first-order theories,
and will indicate some problems arising in this research, related to the possible existence of nondefinable paths in trees. (Based on joint work with Ruaan Kellerman.)
- Georg Gottlob
Title: "A Family of Logical Query Languages for New Applications"
Abstract: I will report on a recently introduced family of Datalog-based languages, called
Datalog+-, which is a new framework for tractable ontology querying, and for a variety
of other applications. Datalog+- extends plain Datalog by features such as existentially
quantified rule heads, and, at the same time, restricts the rule bodies so to achieve decidability
and tractability. The favourable decidability and complexity results are based
on two different paradigms: One is guardedness, and the other is a new paradigm we call
- Erich Grädel
Title: "Fixed-point logics, linear algebra, and the quest for a logic
for polynomial time"
Abstract: The most important open problem of finite model theory is the question whether
there exists a logic that captures polynomial time, in the sense that a property of finite
structures is definable in the logic if, and only if, it can be decided in polynomial time.
Natural candidates for such a logic are suitable extensions of the fixed-point logics LFP
(least fixed-point logic) and IFP (inflationary fixed-point logic). A well-known such extension
is fixed-point logic with counting which captures polynomial time on several interesting
classes of structures including planar graphs, structures of bounded tree-width
and all classes of graphs with forbidden minors, but fails to do so on the class of all finite
It has recently been shown that solving systems of linear equations is a problem that separates
polynomial time from fixed-point logic with counting. This motivates the extension
of fixed-point logic by operators from linear algebra such as ranks of definable matrices,
similarity of matrices and so on. At this point it is not known whether such extensions
lead to a logic that captures polynomial time.
Title: "On separation question in the alternating fixpoint hierarchy"
Balder ten Cate
Title: "Unary negation"
Abstract: The talk reports on recent joint work with Luc Segoufin (INRIA/ENS Cachan), in which we propose a new decidable fragment of first-order logic, and of fixed point logic.
These fragments are based on the idea of restricting the use of negation to subformulas in one free variable. They are not only computationally but also model-theoretically well behaved,
and they generalize several existing formalisms, such as conjunctive queries, monadic datalog, modal logic and the μ-calculus.
Title: "Frame definability for classes of trees in the μ-calculus"
Abstract: This talk is based on a joint work with Thomas Place. We study the expressive power of the μ-calculus at the level of frames. The expressive power of the μ-calculus on the level of models (labeled graphs) is well understood and captured by the Janin-Walukiewicz theorem. On the level of frames (graphs without labeling), nothing is known. In the setting of frames, the proposition letters correspond to second-order variables over which we quantify universally.
We compare the expressive power of the mu-calculus and monadic second-order logic on frames, in the particular case when the frames have a tree structure. Our main result is a characterization of those monadic second-order formulas that are equivalent on trees (seen as frames) to a formula of the μ-calculus.
Title: "Fixed-point logics on finite game trees"
Abstract: The talk will elaborate on recent joint work with Johan van Benthem, in which we showed how to define game solution concepts for finite games in extensive form. For that purpose, we used fixed-point extensions of first-order logics like monadic least fixed-point logic FO(LFP1), which happens to be very well-behaved on ``plain'' finite trees (which differ from game trees by the fact that they do not incorporate any preference order over the leaves). However, if the satisfiability problem for FO(LFP1) is decidable on finite trees, we will explain that it is undecidable on finite game trees. We will also point out that such structures can be represented as a specific type of ``data trees'', while terminal nodes in game trees can be represented as the corresponding type of ``data words''. Such structures have been introduced and studied in the context of program verification and XML query languages. This suggest a possible transfer of techniques and results (in particular decidability and undecidability results) from one framework to the other.