Limit-Computable Mathematics (LCM) is a fragment of classical logic. LCM is based on the notions of limit-computation, which models trial-and-error learning processes in Gold's computational learning theory. LCM enables us to "execute" a class of classical proofs in intuitive manner. We will give a survey of ongoing researches on its mathematical foundations and its possible applications to formal proof developments.
Automata, Logic, and XML
Frank Neven
(Limburgs Universitair Centrum)
We survey some recent developments in the broad area of automata and logic which are motivated by the advent of XML. In particular, we consider unranked tree automata, tree-walking automata, and automata over infinite alphabets. We focus on their connection with logic and on questions imposed by XML.
Mu-calculus via Games
Damian Niwinski
(Warsaw University)
To acquaint with the Mu-calculus, a game is perhaps a most natural example. If the goal of a player is to reach some desirable position in finite time, the set of positions that guarantee the win can be computed as a least fixed point. If, on the contrary, the aim is to stay forever within a set of some safe positions, the winning set can be presented as a greatest fixed point. More sophisticated winning conditions arise naturally in games modeling potentially infinite behavior of reactive systems. It turns out that, again, they can be captured by fixed points, but in general mutually dependent least and greatest fixed point operators are necessary.However games are more than just an illustration of the expressive power of the Mu-calculus. Indeed, the very meaning of truth of a fixed--point formula under a given interpretation can be, most naturally, explained by a certain infinite game (specifically, parity game). This gives a valuable insight into the calculus which otherwise is often perceived as illegible by human eye.
What is more, the game semantics reduces the Mu-calculus model-checking to the problem of solving parity games. The latter takes as input a finite arena (``rules'') of a game and computes as output the set of winning positions of a designated player or, more ambitiously, her winning strategy. The complexity of solving parity games has a rare status of both NP and co-NP (actually, UP and co-UP, where UP stands for unambiguous nondeterministic polynomial time). It is a challenge to place the problem in P or perhaps in a probabilistic class like RP or BPP.
What have we gained by reducing the model-checking problem to the problem of solving games, besides simplicity ? One may hope that ideas and techniques of game theory will prove useful here. Indeed, transferring the problem to a class of more general games with a unique real game value was used by Jurdzinski for the UP upper bound, and by Petersson and Vorobyov for a suebexponential randomized algorithm for parity games. One may expect that further exploration of these connections may open a new perspective on the Mu-calculus, perhaps relating it to the fixed-point results underlying the concepts of equilibriums in game theory.
In my talk I will first explain the aforementioned game semantics of the Mu-calculus, which is essentially due to Emerson and Jutla, although the ideas can be traced back to Gurevich and Harrington, and even further to Büchi. Then I will survey a number of approaches to the Mu-calculus model-checking problem via games.
Home | Call for Papers | Programme Committee | Scientific Programme | Conference Arrangements | Photos Last modified: Thu Jun 13 10:40:43 BST 2002