GAMES logo Nodes: Edinburgh
Aachen Bordeaux Edinburgh Paris Rice Uppsala Warsaw Vienna

Task 7: Logics, games, and efficient query evaluation


Game-theoretic techniques will be used to attack unresolved problems of expressiveness, such as fixed point hierarchies and the associated algorithmic questions. Model checking games will be used for efficient formula evaluation with applications to verification and query evaluation. The network will develop algorithms and perform systematic complexity and scalability studies for query evaluation, concentrating on structural properties of data that have been shown to significantly reduce query complexity.


Background literature

[1] W. Thomas, Automata on infinite objects, in Handbook of Theoretical Computer Science (J. van Leeuwen, ed.), vol. B: Formal Methods and Semantics, pp. 133-192, Elsevier Science Publishers, 1990.
[ BibTeX ]
[2] C. Stirling and P. Stevens, Practical model-checking using games, in TACAS 1998, no. 1384 in LNCS, pp. 85-101, 1998.
[ BibTeX ]
[3] E. Grädel, Guarded fixed point logic and the monadic theory of trees, Theoretical Computer Science, vol. 288, pp. 129-152, 2002.
[ BibTeX ]