Abstract:
The first part of the talk is an overview of the theory of recognisability for words, ground terms and graphs. A set S is recognisable if its membership problem “does x belong to S?” can be answered using an amount of memory that does not depend on x. For words and ground terms, recognisability is equivalent to the existence of an automaton that traverses the input structure in a predefined order, while labelling its constituent substructures with finitely many states. For graphs, there is no universally-accepted notion of automata, mainly because graphs do not have canonical traversal orders, in general. In this case, one defines recognisability using homomorphisms into finite algebras.
A definition of recognisability is considered to be “robust” if it has a logical characterisation. For words and ground terms, recognisability coincides with definability in Monadic Second Order (MSO) logic. For graphs, in general, there is no known equivalence between recognisability and logical definability. However, for graphs of bounded tree-width, recognisability coincides with definability in MSO extended with modulo constraints on the cardinality of sets, a fragment called Counting MSO (CMSO).
The second part of the talk presents new results, for graphs of tree-width at most k, where k=2 (and perhaps also k=3, if science will advance more by September). We introduce regular grammars and regular expressions that provide compact syntactic representations of (all) recognisable sets of graphs of tree-width at most k. We show that these representations can be converted into recogniser algebras of singly-exponential size, which provides EXPTIME-algorithms for the problems of emptiness, intersection and inclusion between sets of graphs represented in these ways. The effectiveness of these algorithms has been tested on a prototype implementation, with encouraging results. We conclude with a number of open problems, both theoretical and practical.
Short Bio:
Radu Iosif is Research Director at CNRS since October 2022. Before that he had been CNRS researcher at CNRS (2002-2022). He obtained a PhD from Politecnico di Torino (2000) and Habilitation from University of Grenoble Alpes (2016). His research focuses on program verification using logics and automata theory, with a recent focus on parametric verification. He authored over 70 publications in international journals and conferences, with h-index 26 and 2200+ citations (Google scholar).
