, 
, 
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)
Definability in o-minimal expansions of the real numbers
by Ricardo Bianconi (Departamento de Matemática Pura, Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)
We present some recent results and problems concerning definable sets and functions in o-minimal expansions of the field of real numbers by analytic functions. Namely, conditions for a complex valued holomorphic function to be definable in such structures; an application to transcendental number theory (some estimates connected to Schanuel's conjecture).
Sparseness and NP-hardness over the reals
by Felipe Cucker (Department of Mathematics, City University of Hong Kong, Hong Kong)
We extend the combinatorial notion of sparseness for discrete sets to a geometric notion for sets over the reals. Then we extend Mahaney's Theorem (on the non existence of sparse NP-complete sets) to some settings of real number computations and we discuss some open problems related to these extensions.
Model Checking Games for Fixed Point Logics
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 Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations
by Gopalan Nadathur (University of Minnesota, USA)
Many metalanguages and logical frameworks have emerged in recent years that use the terms of the lambda calculus as data structures. A common set of questions govern the suitability of a representation for lambda terms in the implementation of such systems: alpha convertibility must be easily recognizable, sharing in reduction steps, term traversal and term structure must be possible, comparison and unification operations should be efficiently supported and it should be possible to examine terms embedded inside abstractions. Explicit substitution notations for lambda calculi provide a basis for realizing such requirements. We discuss here the issues related to using one such notation---the suspension notation of Nadathur and Wilson---in this capacity. This notation has been used in two significant practical systems: the Standard ML of New Jersey compiler and the Teyjus implementation of Lambda Prolog. We expose the theoretical properties of this notation, highlight pragmatic considerations in its use in implementing operations such as reduction and unification and discuss its relationship to other explicit substitution notations.
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
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 29, 2002, 16:25:33 GMT-0300.