log in


6–9 SEPTEMBER 2016

Tutorial day: 6 SEPTEMBER
Conference: 7–9 SEPTEMBER

The goal of Highlights conferences is to integrate the community working on logic, games and automata.


Talk submission deadline: June 3, 2016.
Notification: June 13, 2016.
Tutorial day: September 6, 2016.
Conference: September 7-9, 2016.


  1. Highlights 2015 (Prague, 15–18 September)
  2. Highlights 2014 (Paris, 2–5 September)
  3. Highlights 2013 (Paris, 18-21 September)


There are no proceedings. You present your best work, be it published elsewhere or yet unpublished.


The conference is three days long. The contributed talks are around ten minutes.


The participation costs are modest. Brussels is easy to reach.


Let's use the conference model that is so successful in other fields, like mathematics.



Meena Mahajan
Andreas Maletti
Marc Zeitoun


Benedikt Bollig (Topic TBA)
Antonín Kučera (Topic TBA)


Sławomir Lasota
Anca Muscholl


Thomas Schwentick (Chair)
Roderick Bloem
Aiswarya Cyriac
Claire David
Anuj Dawar
Jacques Duparc
Henning Fernau
Paul Gastin
Matthew Hague
Jarkko Kari
Barbara König
Stephan Kreutzer
Christof Löding
Luke Ong
Joël Ouaknine
R. Ramanujam
Pierre-Alain Reyner
Emanuel Sallinger
Ulrike Sattler
Szymon Toruńczyk
Igor Walukiewicz


Véronique Bruyère (Main)
Emmanuel Filiot (Main)
Véronique Bastin
Thomas Brihaye
Pascaline Browaeys
Luc Dartois
Gilles Geeraerts
Quentin Hautem
Ismaël Jecker
Nathan Lhote
Noémie Meunier
T. Van-Anh Nguyen
Guillermo A. Pérez
Mickaël Randour
Stéphane Le Roux


Dietmar Berwanger
Mikołaj Bojańczyk
Tomáš Brázdil
Thomas Colcombet
Anuj Dawar
Hugo Gimbert
Erich Grädel
Christof Löding
Aniello Murano
Moshe Vardi



The goal of Highlights conferences is to integrate the community working on logic, games and automata. Papers on these topics are dispersed across many conferences, which makes them difficult to follow.

A visit to Highlights conference should offer a wide picture of the latest research in the area and a chance to meet everybody in the field, not just those who happen to publish in one particular proceedings volume.

We encourage you to attend and present your best work, be it already published or not, at the Highlights conference!


Representative areas include, but are not restricted to:

  • logic and finite model theory
  • automata theory
  • games for logic and verification


You submit a talk, not a paper. Hence, submissions should have a single author, who is the speaker. Since you should only present your favorite result of the year, there should be at most one submission per speaker. The abstract, of 1-2 pages, may include a list of coauthors.

There are no formal proceedings and we encourage submission of work presented elsewhere.


Talk submissions are done via the Highlights 2016 EasyChair site

The submission deadline is June 3, 2016. Notifications will be sent by June 13, 2016.


Registration is open until August 7, 2016.




All tutorials and talks will take place in the Forums of the Université Libre de Bruxelles (ULB) campus La Plaine; click here to view in Google Maps.


There are several hotels and hostels around Brussels which offer a wide range of prices. ULB is easily accessible from everywhere in town using the city’s public transportation.


Information about public transportation in Brussels is avaible at the STIB-MIVB website; for trains, visit NMBS-SNCB.


From the Brussels-Zaventem airport, you can use the public transportation to get to the city or ULB quite easily. The fastest way is to take a train to Brussels Central station from the airport (and then follow the instructions below). Otherwise, at the airport, take bus line 12 (preferably) or 21. They follow the same route, although the 21 stops everywhere whereas the 12 is “express”; however the 12 does not run after 8PM or on week-ends. Exit the bus at the Schuman station to take the subway. If you want to get to the ULB, take line 5 directionHermann-Debroux, and stop at Delta. Brussels is also served by the smaller Brussels South Charleroi airport. There are buses every 30 minutes to take you from the airport to Brussels South station.


From Gare de Midi/Zuidstation/Brussels South station: take metro line 2 or 6 direction Simonis-Elisabeth (counter-clockwise wrt. metro ring) change at station Arts-Loi to metro line 5 direction Hermann-Debroux(this metro can be taken directly from Gare Centrale/Central station) exit metro at station Delta.


Leave station at exit ULB/Plaine (on the right after the Relay shop). Go to the Forums by following the path; when encountering a small patio with the cafeteria on the right, keep in the same direction, the Forums will be on your left after the patio.


Meena Mahajan Arithmetic Circuits: Classes, Structure, Completeness …

In this talk I will review recent developments in algebraic complexity theory. I will outline some major results concerning structure, completeness and closure. I will describe some techniques that have been central to obtaining these results, including extreme depth reduction, partial derivatives, and padding.

Andreas Maletti: Tree Automata in Parsing and Machine Translation

We will discuss how tree automata were rediscovered in the area of statistical parsing of natural language sentences and demonstrate that some techniques developed in that area might also be beneficial in automata theory. On the example of syntax-based machine translation, we will demonstrate the other direction showing how automata theory can provide solutions to problems in natural language processing. With the identification of the exact expressive power in terms of standard models and known closure properties for them, we developed a syntax-based translation system that can translate not only a single parse, but rather the full parse forest delivered by the parser.

Marc Zeitoun: From membership to covering via separation

The membership problem is the standard mean to investigate the expressive power of fragments of MSO over classical structures, such as words or trees. It asks for an algorithm taking as input a regular language, and deciding whether it can be expressed within the fragment under study. It has been solved successfully for many natural fragments of first-order logic, but for some of them the situation is stuck since the 70s. This is the case for levels of the ‘quantifier alternation hierarchy’, which stratify first-order logic: membership algorithms have been obtained for lower ones only. In view of recent progress for some of these levels, a reason may be that membership is too restrictive as a framework.

In this talk, I will introduce two problems called ‘separation’ and ‘covering’, which both generalize membership. Separation takes as input two regular languages rather than just one, while covering takes as input a finite number of regular languages. I will explain the connections between the three problems, and why it is interesting to consider them in order to better understand logical fragments of MSO.


Benedikt Bollig: Automata and Logics for Distributed Systems

Automata are a popular model of computer systems, making them accessible to formal methods and, in particular, synthesis and model checking. While classical finite-state automata are suitable to model sequential boolean programs, models of distributed and concurrent systems involve several interacting processes and extend finite-state machines in many respects. Roughly, we may classify system models according to their communication paradigm (shared variables, message passing, broadcasting), the type of a process (finite-state, recursive, timed), or the number of processes (static, dynamic, bounded, parameterized).

In this tutorial, we survey automata models for several combinations of the above-mentioned characteristics. We also present suitable specification formalisms such as monadic second-order logic, temporal logic, and rational expressions. In particular, we will compare the expressive power of automata and logics, give translations of specifications into automata, and show how to solve the model-checking problem: Does a given automaton satisfy its specification?

Antonin Kučera: Methods and tools for solving infinite-state stochastic games

The tutorial focuses on methods and tools for solving turn-based stochastic games with infinitely many states. Typically, such games are obtained as game-theoretic extensions of established computational models, such as pushdown automata, one-counter automata, vector addition systems with states, lossy channel systems, etc. An important step towards solving such games is a detailed understanding of both non-deterministic and fully probabilistic variants of the model, which often requires new concepts and proof techniques, especially in the fully probabilistic subcase.

We start with the reachability objective, and identify the main differences between finite-state and infinite-state games. In particular, we show that optimal strategies do not necessarily exist in infinite-state stochastic games, and even if they do, they may require infinite memory. Further, we show that infinite-state stochastic games are not weakly determined in the subclass of memoryless strategies. Then, we show how to solve the reachability objective for some concrete classes of infinite-state stochastic games. In particular, we concentrate on games over stateless pushdown automata and one-counter systems.

A useful tool for analyzing infinite-state stochastic systems are martingales. We give a brief introduction to martingales and the associated toolbox (optional stopping theorem, Azuma–Hoeffding inequality), and show how these can be applied to the analysis of one-counter stochastic processes and games.

In the end of the tutorial, we present an overview of existing results and mention some open problems.

The tutorial does not require any special knowledge beyond the fundamentals of probability theory (in particular, no prelimary knowledge about martingales is assumed).

Invited Sessions


Emmanuel Filiot: Automata, Logic and Algebra for Word Transductions

This talk will survey old and recent results about word transductions, i.e. functions mapping (finite) words to words. Connections between automata models (transducers), logic and algebra will be presented. Starting with rational functions, defined by (one-way) finite transducers, and the canonical model of bimachines introduced by Reutenauer and Schützenberger, the talk will also target the more expressive class of functions defined by two-way transducers and their equivalent MSO-based formalism.

Helmut Seidl: Equivalence of Deterministic Tree-to-String Transducers Is Decidable

Top-down tree-to-string transducers recursively process their structured input data while producing output in an unstructured way, namely as a string. Let yDT denote the class of all deterministic top-down tree-to-string transducers. In the presentation, we show that equivalence of two such transducers is decidable – a problem which has been open for more than 30 years.

As non-equivalence can be witnessed by an input on which the two transducers differ, decidability of equivalence follows if only an effective proof system can be provided for certifying equivalence whenever it holds. We indicate how such a proof system can be constructed using powerful techniques from commutative algebra.

While in general not much is known about the complexity of the decision problem, we also present special cases where polynomial upper bounds can be obtained.

[Joint work with Sebastian Maneth (Edinburgh) and Gregor Kemper (München).]


Szymon Toruńczyk: Towards complexity theory with atoms

I will discuss various classical computational problems, generalized to the setting where the instances are potentially infinite sets with atoms. In particular, we will focus on constraint satisfaction problems, such as 3-colorability, unreachability, Horn-SAT, solvability of systems of linear equations, where the instance is an infinite structure (graph, formula) built out of atoms, with a finite description. It turns out that tight classical complexity results lift to the infinite setting. Moreover, many classical algorithms can be lifted to this setting in a natural way.

Eryk Kopczyński and Michał Szynwelski: Programming with atoms (tool demonstration)

A demo presentation of two simple programming languages designed to manipulate infinite, but first-order definable structures, such as the set of all intervals with rational endpoints. One of the languages is implemented as a Haskell module, while the other as a C++ library. Internally, infinite sets are represented by logical formulas that define them, whereas an external SMT solver is invoked to check their basic properties.

Murdoch James Gabbay: Consistency of Quine’s NF using nominal techniques

Naive set theory has one rule; naive sets comprehension: If φ is a predicate, then {a | φ(a)} is a set. This is inconsistent by Bertrand Russell’s famous observation of 1901 that {a | a ∉ a} ∈ {a | a ∉ a} if and only if {a | a ∉ a} ∉ {a | a ∉ a}. Solutions proposed included Zermelo-Fraenkel set theory, simple type theory, and Quine’s New Foundations (NF).

NF works by restricting comprehension to stratifiable formulae; those in which variables can be assigned ‘levels’, which are natural numbers, such that if a ∈ b occurs and a has level n, then b must have level n+1. Russell’s example is ruled out because a ∉ a cannot be stratified.

Consistency of NF has been an open problem since it was proposed by Quine in 1937. I will present a claimed proof of consistency for Quine’s NF (paper available on my webpage and on arXiv from www.gabbay.org.uk/papers.html#conqnf), exhibiting it as a corollary of a new view of the foundations of logic and computation based on nominal techniques which I have been developing now for several years.


designed and delivered