Presentation
The methods of logic and language theory are applied to graphs and other combinatorial objects such as maps that formalize graph drawings. For this purpose, the main logical language is the logic of the monadic second order (LSOM). Its importance rests on the equivalence between the definability in LSOM of a set of trees, finite or infinite, and the recognizability by finite automaton. There is no satisfactory notion of a "general" automaton of graphs. It exists only for terms (words are a special case, to which can be added Mazurkiewicz traces) and trees with roots (ordered or not). These notions apply to classes of objects structured in a tree-like manner. Graphs are not naturally structured. Nevertheless different types of structuring have been defined and allow to extend to certain classes of graphs the equivalence mentioned above between recognizability and logical definability.
Four types of results and research themes result from this.
- With a view to extending the methods of language theory to graphs, the LSOM replaces automata and allows the definition of transformations which generalise the transductions of words and trees based on automata. Graph composition operations make it very easy to define algebraic graph grammars. The corresponding classes are preserved by transductions. We thus obtain a robust extension (we can give this term a precise technical meaning) of several fundamental notions of language theory.
- The satisfaction of a SWOT formula with a graph of a given tree width or click width is decidable. The above-mentioned notions of graph structuring are therefore also relevant to OSL from this point of view.
- All problems which can be specified in LSOM and in particular many NP-complete problems can be solved in polynomial (often even linear) time on structured graph classes. This approach extends to optimization, enumeration and enumeration problems. The proof of the general theorem does not provide an implementation possibility because of the size of the automata associated with the formulas and the algorithmic difficulty of the decomposition of graphs having say more than 100 vertices. An interesting possibility under study consists in defining a fragment of the LSOM which is interesting from a practical point of view but for which calculations remain concretely possible, and another one consists in using automata which calculate at each stage the transition to be carried out (fly-automata).
- Many concepts of graph theory, such as decompositions, graph representations by intersections of combinatorial or geometric objects can be fruitfully formalised in LSOM. This applies to both countable and finite graphs.
All of these themes have a large number of open problems and potential applications to related fields studied in the team. Two of these topics are particularly well studied :
- The study of graph decompositions is a very rich field, both in terms of the structural theory of graphs (highlighted for 30 years by the work of Robertson, Seymour and their continuators) and in terms of algorithmic applications, whether or not related to logic. We can cite the search for efficient decomposition algorithms, the definition of new decompositions, especially for hypergraphs and relational structures, as well as decompositions based on planar graphs and not only on trees.
- The rapid verification of graph properties by means of labels attached to vertices is a domain where the association of graph decompositions, logic (first-order and monadic second-order), and properties of particular classes of graphs (notably bounded arboricity, planarity, exclusion of minors) is particularly fruitful. This research is done in close collaboration with the "Combinatorics and Algorithms" team.
This research is clearly of a fundamental nature, but it is motivated by applications to the construction of algorithms for verifying graph properties and building efficient algorithms.