Tutorial day: 6 SEPTEMBER

Conference: 7–9 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.

Benedikt Bollig (Topic TBA)

Antonín Kučera (Topic TBA)

Registration is open until August 7, 2016.

Keynotes

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.

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.

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.

Tutorials

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?

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).

Transducers (session chair:
Anca Muscholl)

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.

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).]

Sets with atoms (session chair:
Sławomir Lasota)

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.

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.

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.