One of the important research fields of theoretical and applied computer science and mathematics is the study of algorithmic, logical and model theoretic properties of structures and their interactions. By a structure we mean typical objects that arise in computer science and mathematics such as data structures, programs, transition systems, graphs, large databases, XML documents, algebraic systems including groups, integers, fields, Boolean algebras and so on.

From a mathematics point of view these are natural objects of study and the theory of computable structures initiated by Malcev and Rabin in the 60s witnesses it. This mathematical study has been one of the most active areas of research in the last decade. {}From a computer science point of view, there has been a growing interest in understanding infinite structures. The need for this study comes from the fact that one cannot usually put bounds on typical objects of computer science such as the sizes of databases, programs, XML documents, stacks, communication buffers, and so on. Moreover, these objects are usually not seen as static components but are modified in a dynamic way, which leads to systems with infinite state spaces, i.e., infinite transition systems. These transition systems can be modeled by infinite graphs, where nodes correspond to states of the system and edges correspond to transitions between the states. Properties of such systems can be expressed in logical formalisms and it is an algorithmic task to determine the validity of such formulas or to calculate the set of states satisfying a certain property. In computer science, the following aspects for a logical theory of such systems are of interest.

• Infinite systems in computer science are usually represented by some finite description or abstract machine; system states are then configurations of that abstract machine.
• These system states have some internal structure that determines the global properties of the system. E.g., they may be represented by natural numbers, finite strings, trees, or graphs and transitions are defined by transducers on the data structures.
• The emphasis is put on efficient algorithms for the verification of system properties that are specified in a suitable logical language.

Several aspects of such a unified theory have already been addressed in the past. These include:

• Computable model theory, a branch of classical model theory and recursion theory, considers structures that are presented in some effective (and thus finite) way. An emphasis in this field is to study algorithmic properties of structures by comparing complexities of their undecidable features. Typical important structures in this context such as arithmetic of natural numbers do not have decidable first order theories. Essential tools of research here are the Turing degrees and methods of recursion theory.
• The theory of automatic structures, a newly formed direction of research in which structures are represented by finite state machines such as finite automata, tree automata, $\omega$-automata, etc. In contrast to computable model theory, an emphasis here is given to understanding the algorithmic properties of structures by comparing complexities of their decidable features. All these structures have decidable first order theories. The development of this theory is based on methods of complexity theory, finite combinatorics, model theory and automata theory.
• Classes of infinite graphs that are generated by some kind of abstract machines and that lead to decidable monadic second-order theories became an active research topic in recent years. Currently, the most general class of graphs with decidable monadic second-order theories is the Caucal hierarchy. Graphs that are generated by ground tree rewriting systems constitute a class, were monadic second-order logic is undecidable in general, but first-order logic with reachability is still decidable.
• Several approaches for model-checking systems with infinite state spaces were developed in the past by researchers working in verification. Typical examples in this context are unbounded communication buffers, stacks in procedural programming languages, or parameterized systems.

At this seminar, researchers from all these fields met. To give the non-specialists a general overview of the flavor, topics, methods, and open questions of the other fields, we had five keynotes given by Igor Walukiewicz, Wolfgang Thomas, Denis Hirschfeldt, Sasha Rubin, and Parosh Aziz Abdulla. These were complemented by contributed talks of the participants that span the whole spectrum laied out above.