BRICS · Contents · Programme

**A BRICS Mini-Course**

**April 23, 24 and 27, May 6, 1998**

**Lectures by
Igor Walukiewicz
**

**
**

We will consider second order theories that have found applications in program verification and other areas of computer science. We will consider first and second order logics over words and trees. We will also discuss temporal logics and the mu-calculus over these structures. Finally we will consider all these logics over traces. We will be interested in the expressive power of these logics and the complexity of the satisfiability and the model checking problems.

Although we will approach the subject from the program verification perspective we hope that especially complexity issues may be of broader interest as the theories we will discuss proved to be a convenient tool for establishing the complexity of many problems in computer science.

### Thursday April 23, 1998, 15:15-17:00 in Auditorium D3

### Friday April 24, 1998, 13:15-15:00 in Auditorium D4

### Monday April 27, 1998, 10:15-12:00 in Auditorium D1

### Wednesday May 6, 1998, 13:15-14:00 in Colloquium B4