Logic and computation theory

Master's seminars

From finite automata to games on arbitrary graphs, from constant to non-elementary time, from classical logic to temporal logics for complex systems. This seminar covers a wide range of subjects in contemporary theoretical computer science. Often, a master's thesis will solve a nontrivial mathematical problem, or give a survey of some area another possibility is implementing an algorithm (e.g., playing a game).

Traditionally, logic studied the laws of thought. Today, computers make it possible to process a big amount of information outside human mind. Not surprisingly, the development of computer science gives rise to new challenges for logic. Out of many fascinating possibilities, we have chosen the following topics.

Complexity theory. Complexity theory studies the resources needed to solve problems, resources such as time and memory, the number of processors, or maybe the number of random bits needed. The security of asymmetric cryptography is based on assumptions from computational complexity, even though these assumptions remain unproved. The connection between complexity theory and logic is a field called descriptive complexity, which shows that questions about the relationships between complexity classes (such as P, NP, PSPACE) can be rephrased as questions about the expressive power of different logics (usually fixpoint extensions of first-order logic).

Mathematical verification of hardware and software. Some computer systems are so important, that their correctness cannot be judged by mere testing; one needs more thorough methods. One of these methods is building a mathematical model of the system, and proving that this model has no incorrect behaviors. Commonly used models involve games, where an evil environment tries to steer the system into an incorrect state, and a controller tries to avoid this. Logic is used to precisely state what incorrect behaviors are, so that an automatic tool can search all behaviors of the model for incorrect ones. Logics used in verification include temporal and fixpoint logics, and the underlying technical tools are often finite automata.

Classical automata theory. Despite being one of the older fields in computer science, automata theory still offers unsolved, but simply stated problems. Consider the following, still open, question about regular expressions: is there a regular language that cannot be described by a regular expression (complementation is allowed) that has no nesting of the star operation? (The star is allowed, but inside a star there is no other star.) The seminar will study such questions, also for more general automata models, such as tree automata, or automata on infinite words.

Modern scientific literature of the subject, including scientific journals and data from Internet. Details are provided by the lecturers at the first meeting.

Knowledge

Student learns about research problems in the current studies in the area of logic in computer science. She or he should start her/his own supervised research, which will become the basis of her/his Master Thesis.

Skills

Student can

1. read scientific papers with understanding,

2. communicate scientific results to others in a clear and attractive way,

3. listen in an attentive manner and ask questions to speakers.

Competence

Students gets knowledge about research methodology in the area of logic in computer science. She or he gets a general knowledge about various publication venues and their scientific prestige.

The required condition is a careful preparation and presentation of at least one lecture during a semester, and---depending on the year of studies--the acceptance of a subject of the Master Thesis, or submission of the thesis itself.