A BRICS Mini-Course
April 23, 24 and 27, May 6, 1998
Lectures by
Igor Walukiewicz
Department of Informatics, Warsaw University, Poland
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.