Rio de Janeiro, Brazil

Scientific Sponsorship
Interest Group in Pure and Applied Logics (IGPL)
European Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)

Funding
, ,

Organisation
Centro de Informática, Universidade Federal de Pernambuco (CIn-UFPE)
Departamento de Filosofia, Pontifícia Universidade Católica do Rio de Janeiro (FIL-PUC-Rio)
Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro (DI-PUC-Rio)

Title and Abstract of Tutorial Lectures

Some model theory of ordered structures
by Ricardo Bianconi (Departamento de Matemática Pura, Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)

We present the main developments of the so-called o-minimal structures, that is, linearly ordered structures whose definable one dimensional definable sets are union of finitely many points and open intervals whose enpoints are in the structure. The typical examples are the dense linear orders and the real closed fields. We prove the cell-decomposition theorem, number of countable models, present some important o-minimal expansions of the field of real numbers and indicate some applications inside and outside model theory.

Computing with Real Numbers
by Felipe Cucker (Department of Mathematics, City University of Hong Kong, Hong Kong)

During the last few years a theory of computation over the real numbers developed with the aim of laying theoretical foundations for the kind of computations performed in numerical analysis under complete information. In this tutorial we will describe the notions playing major roles in this theory ---with special emphasis on those which do not appear in discrete complexity theory--- and review some of its results.

Model Checking Games
by Erich Grädel (Mathematische Grundlagen der Informatik, RWTH Aachen, Germany)

Model checking problems ("is a given formula true in a given structure?") for almost every logic can be cast as strategy problems ("which player does have a winning strategy in a given game?") for the appropriate evaluation games (also called Hintikka games).

In first-order games all plays are finite and the strategy problem can be solved in linear time in the size of the game. For fixed point logics, the appropriate evaluation games are parity games, which admit also infinite plays. Each position is assigned a priority, and the winner of an infinite play is determined according to whether the least priority seen infinitely often during the play is even or odd. It is open whether winning sets and winning strategies for parity games can be computed in polynomial time. The best algorithms known today are polynomial in the size of the game graph, but exponential with respect to the number of priorities.

An intuitive reason for the good model checking properties of certain logics is that the associated evaluation games remain small. For instance, the restricted quantification in modal or guarded logics limits the number of possible moves in the evaluation games and thus leads to smaller game graphs. Modal and guarded fixed point logics admit efficient model checking if and only if parity games can be efficiently solved. While we do not know whether this is possible in general, we can analyze the structure of parity games and isolate `easy' cases that admit efficient solutions. With this analysis, we also try to make precise some of the game theoretic intuitions that underly algorithmic approaches to automata and model checking problems. We link these `easy games' to logic and thus obtain efficient model checking algorithms for fragments of fixed point logic.

In the tutorial, I will give an overview over model checking algorithms via evaluation games for a number of different logics. In the research talk, I will focus on more recent results concerning parity games and fixed point logics.

The Metalanguage Lambda Prolog and its Implementation
by Gopalan Nadathur (University of Minnesota, USA)

The manipulation of syntactically complex objects like programs, formal specifications, mathematical expressions, types and proofs is of interest in systems such as compilers, interactive theorem provers, symbolic computation systems, type checkers, program transformers and generic derivation systems. The prototyping and implementation of such systems can be simplified by the availability of a programming language, referred to as a metalanguage, that permits flexible representations of the relevant objects and that contains mechanisms useful in reasoning about these objects. The logic programming framework provides a good basis for such a metalanguage because of the support it offers for rule based specifications and for unification and search that are useful in obtaining implementations from such specifications. However, certain enhancements must be made to usual logic programming languages in order to produce a metalanguage that is of general interest. These enhancements include the provision of lambda terms for representing objects by means of their higher-order abstract syntax and mechanisms for controlling the availability and attributes of objects in subparts of a reasoning process. Such additions have been considered in our work and have resulted in a language called Lambda Prolog. In this talk, we will discuss the new features present in Lambda Prolog from the perspective of metalanguage applications and we will outline techniques we have developed for their efficient implementation. The ideas that will be presented are embedded in an abstract machine and compiler based implementation of the language that will also be discussed.

Automata theory and logic
by Igor Walukiewicz (Bordeaux University, France)

The connections between automata theory and logic are strong and fruitful. Good examples of these are: Buchi's proof of decidability of monadic second-order (MSO) theory of infinite words and Rabin's proof of decidability of MSO theory of infinite binary trees. This last theory is one of the strongest known decidable logical theories with many other decidability results being an easy consequence. Recently, theory is one of the strongest known decidable logical theories with many other decidability results being an easy consequence. Recently, automata play a prominent role in understanding of many logical formalisms used in Computer Aided Verification.

In the introductory lecture we will discuss the above theorems and their connections to program logics and verification. In particular, we will examine close relationship with the mu-calculus and infinite games.

At the workshop talk we will survey the expressibility results for different program logics. These results connect program logics to automata with special properties or to fragments of MSO logic. We will also discuss hierarchy results for CTL^*, mu-calculus and MSO logic. The hierarchies are defined in terms of alternation of some operators. A very interesting research topic is to find algorithms deciding each of the levels of the hierarchies.

States of Knowledge (Tutorial)
by Rohit Parikh (Department of Computer and Information Science, Brooklyn College, City University of New York, USA)

When a group of people are thinking about some true formula A, one of them may know it, all of them may know it, or it might be common knowledge. But there are also many other possible states of knowledge and they can change when communication takes place. What states of knowledge are possible? What is the dynamics of such changes? And how do they affect possible co-ordinated action? We describe some developments in this domain.

Last modified: July 23, 2002, 10:25:33 GMT-0300.