Current (finished und unfinished) Projects:

• Recently I wrote a symbolic model checker for monadic second-order logic (MSO) on words and trees.
  As far as I know, this is the first (trial) of the implementation of a fully symbolic model-checker for MSO. Here,
  fully symbolic means that also states are encoded by OBDDs. The intention is (in contrast to the standard
  model-checking approach) that we want to evaluate complex queries (which require huge automata) in relatively
  small structures (compared to the huge states-space of traditional model-checking).
  Resume: Unfortunately, formulas that cause huge (and hence intractable) automata do not behave much better here and
  have the additional drawback of a very inefficient treatment (e.g. minimizing automata and reachability
  analysis)
• Parameterized Complexity of Model-Checking: there are still some cases that have to be settled,
  i.e. cases in which there is a considerable gap between the best known upper and lower bound.
  Most importantly, a better upper bound for first-order logic on planar graphs.
• Semi-Structured Data: Can logic provide successful tools to study the expressability of the recently emerging query
  languages for tree-structured data (such as XQUERY)? Lower Bounds ...?
• Query evaluation on compressed tree-instances: by fusing identical subtrees, tree structured data (e.g. XML documents)
  can be compressed considerably. After devising efficient (fixed-parameter linear time) algorithms that evaluate
  Core-XPATH and monadic DATALOG queries on such compressed instances, the question is whether we can go
  any further and find an efficient fragment of XQUERY.
  As for the first fragments, this question includes practical testing with "real-life" XML documents.
• First-order model-checking on relational structures: it is widely known that first-order logic corresponds to the relational
  calculus, which itself constitutes a large fragment of SQL. Storing intermediate results as binary decision diagrams
  (OBDDs), we hope that hard queries become tractable. Here again we put emphasis on rather small structures, but hard
  queries. A prototype will be implemented in SML using the OBDD-interface for BuDDy.