Task 7: Logics, games, and efficient query evaluation
Objectives
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.
Notes
- Julian Bradfields' presentation of Task 7 in Edinburgh. [slides]
- Discussions on the above (to follow).
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 ] |
