Part of the Institute for Theoretical Computer Science of the Department of Computer Science and Automation.
The research focus of the Department of Automata and Logic lies in the areas of methods for the automatic verification of distributed systems and automatic structures. In particular, these investigations use methods from logic and automata theory and therefore belong to the broader field of logic in computer science.
In automatic verification, we try to find a compromise between the expressiveness of specification languages and their algorithmic controllability. In the process, recently gained theoretical insights into distributed models with finitely many internal states are also examined, adapted and extended in terms of their practical relevance.
In addition to these systems, the verification of those with an infinite number of internal states (which can occur, for example, through stacks or string variables) is also of interest. An abstract model of these systems are automatic structures. We investigate these structures from the algorithmic side (Which questions can be solved with which effort?) and from the abstract side (Which model-theoretic properties characterise these structures?).