Perspectives in Verification
November 17–18, 2005 — Cachan

November 17
10:00-11:00		 Wolfgang Thomas Download
Slides
Perspectives in algorithmic model theory
A promising task of automata theory is to contribute to an algorithmic theory of (infinite) models, an emerging field which is useful, for example, in the verification of infinite-state systems. We start from two alternative presentations of structures: by the description in terms of finite automata and by the construction from canonical structures using appropriate transformations. We then enter a short comparison with classical model theory and in this context discuss the solution of arithmetical constraints. Finally, we give an overview of some tracks on which an algorithmic and automata based theory of models can be further developed.
November 17
11:00-12:00		 Anca Muscholl Download
Slides
First-order logic with infinite alphabets
In a data word (or data tree) each position carries a label from a finite alphabet and a data value from some infinite domain. We consider fragments of first-order logic over data words and data trees which allow for equality comparisons of data. We show that the satisfiability problem for the two-variable logic (with successor and order relation) on data words is decidable, actually the question is equivalent to Petri net reachability. For data trees we show that two-variable logic with successor is decidable on unranked trees.

This is joint work with Mikolaj Bojanczyk (Warsaw Univ.), Claire David (LIAFA), Thomas Schwentick (Dortmund Univ.) and Luc Segoufin (INRIA)

November 17
14:15-15:15		 Martin Grohe
Law enforcement on hypergraphs
It is well-known that many hard algorithmic problems become tractable when restricted to instances of bounded tree width. Gottlob et al. introduced a new form of tree-like decompositions of hypergraphs called hypertree decompositions. They proved that constraint satisfaction problems are even tractable for instances of bounded hypertree width. Jointly with D. Marx, we generalised this further to instances of bounded fractional hypertree width, which is derived from yet another type of decompositions called fractional hypertree decompositions.

All these tree-like decompositions of graphs and hypergraphs can be characterised by search games; the game for tree-width is Seymour and Thomas's "robber and cops game". Such games give a good intuition for the strength of the various decompositions and the corresponding invariants.

This talk is an introduction into decompositions of hypergraphs and their game characterisations.

References:
November 17
16:00-18:00		 Ralf Treinen Download
Slides
Symbolic Constraint Solving
Constraints are a means to specify tuples of data. To be useful, a constraint system has to come with effective means to manipulate (in ways that depend on the application) constraints and to test for their satisfiability. Predicate logic being the natural framework for specifying tuples of data, a constraint system is defined by a logical language, an interpretation, and a set of formulas which are called the constraints.

A constraint system can be employed in at least two different ways:

  • to enhance and to to generalize a computational mechanism which is based on the notion of sets of tuples, such as logic programming, theorem proving, or data bases. A constraint-based formalism can be seen as a two-tired architecture, consisting of a constraint system providing a declarative view to tuples of data, and a computational extension which operates on constraints via logical operations. Since constraint processing is part of the execution, efficiency is an important issue here.
  • to analyze a computational mechanism which may itself be constrained-based. In this case, constraints are used to express assertions about possible tuples of values that can occur in an execution of the mechanism. Examples of such constraint-based analyses are analysis of imperative programs, redundancy in constrained inference systems, and symbolic verification of cryptographic protocols. Here, expressivity of the constraint system is more important than efficiency.
After a short glimpse at the two most prominent methods for symbolic constraint solving, namely syntactic simplification and simulation by automata, I will present in some more detail two results on constraint solving by reachability analysis in inference systems:
  • the problem of entailment of subsumption constraints over feature trees (joint work with Müller and Niehren)
  • the security problem for cryptographic protocols modulo the equational axioms of exclusive or and homomorphism (joint work with Delaune, Lafourcade, and Lugiez)

Though part of the workshop program, this session will be governed by the usual rules of a defense.

November 18
09.00-10.00		 André Arnold Download
Slides
On simulation theorems in mu-calculi
As shown by Muller and Schupp, the core of Rabin's Complementation lemma is that every alternating tree automata is equivalent to a non deterministic one, which is a theorem in the mu-calculus over binary trees. More generally, we call Simulation Theorem a result that states that every formula of a given mu-calculus is equivalent to a formula in some "normal form".

We give some examples of such Simulation Theorems and we address the question of whether they are special cases of a single Simulation Theorem.

November 18
10.00-11.00		 Erich Grädel Download
Slides
Complexity measures for directed graphs
It is well-known that many algorithmic problems on graphs that are computationally intractable in general become simple if the graphs ressembles a tree. Tree width, which measures the resemblance to trees is therefore a fundamental complexity measure on graphs. It can be characterised in several ways, for instance by tree decompositions or in terms of a game in which a number of cops try to catch a robber on the graph. Both, the notion of tree width, and its characterisation via games generalise to other structures such as hypergraphs and arbitrary relational structures.

In this talk we discuss and compare similar complexity measures for directed graphs that are relevant for problems where the direction of the edges is crucial. Notably this is the case for the analysis of games. We will focus on the notion of DAG-width which measures how closely a graph ressembles a directed acyclic graph, and the notion of entanglement which measures to what extent the cycles of the graph are intertwined. Both measures can be defined by way of games that are similar in spirit to the robber and cops games used to describe tree width.

While DAG-width allows for decompositions that are smilar to tree decompositions, entanglement is intimately connected to the computational and descriptive complexity of the modal μ-calculus. It turns out that parity games can be efficiently solved if either the entanglement or the DAG-width of the underlying game graph is bounded.

November 18
11.15-12.15		 Amir Pnueli Download
Slides
Program synthesis in action
November 18
13.45-14.45		 Paul Gastin Download
Slides
On the synthesis of distributed controllers
Given a distributed architecture and a specification, the distributed synthesis consists in finding a local controller for each process of the system so that the controlled behavior of the distributed system meets the specification. This problem depends on several parameters: the class of architectures under consideration, the semantics used for the behaviors, the specification language, and the type of memory allowed for the controllers. Pnueli and Rosner proved that the distributed synthesis problem is undecidable for very simple architectures and a synchronous semantics. Several other results followed both for the synchronous and the asynchronous semantics showing that the problem is undecidable for most architectures and decidable for very specific ones.

In this presentation, I will first describe the distributed synthesis problem and some results obtained in the past both for the synchronous and the asynchronous semantics. I will then present recent work obtained in collaboration with Lerman, Sznajder and Zeitoun showing that, under suitable hypotheses, the problem is decidable for a large class of architectures, in contrast to most undecidability results obtained so far.

November 18
14.45-15.45		 Igor Walukiewicz Download
Slides
Pushing the limits of pushdown verification
A celebrated result of Rabin says that the monadic second order (MSO) theory of the full infinite binary tree is decidable. From there it follows that MSO theory of any regular tree is decidable. One can think of a regular tree as a tree that is an unraveling of a finite graph, or equivalently, as the unraveling of the state graph of a finite automaton.

A push-down tree is the unraveling of a graph of configurations of a push-down automaton. Such a tree may have an infinite number of non-isomorphic subtrees, hence it may be not regular. Still MSO theory of any push-down tree is decidable.

In this talk we will consider extensions of this result in two directions: (i) to larger class of graphs and (ii) to larger class of processes. An important example of extension of the first type is obtained by considering machines with a stack of higher order. The extensions of second type permit to talk about non-regular properties of executions such as boundedness of the stack size. The goal of this talk is to survey recent results on the subject showing that it is quite rich and far from being exhausted.

About LSV