diff options
author | Marcin Chrzanowski <mc370754@students.mimuw.edu.pl> | 2021-10-14 14:37:13 +0200 |
---|---|---|
committer | Marcin Chrzanowski <mc370754@students.mimuw.edu.pl> | 2021-10-14 14:37:13 +0200 |
commit | 946e713c1a9df6f751538b62f6098431add67fc8 (patch) | |
tree | 528cd70f5353b5147f3d5b4711ae86d9350be9d2 | |
parent | 518b9cc6d75555bc6c3a95bd6b734361de023079 (diff) |
Add references in text
-rw-r--r-- | mgr.tex | 14 |
1 files changed, 8 insertions, 6 deletions
@@ -78,12 +78,14 @@ might not always be feasible or desirable. Already model checking is known to be computationally difficult for various interesting logics, but the situation can improve when restricting the class of structures considered. For example, MSO model checking is NP-hard in general, -but Courcelle showed that deciding if an MSO sentence holds in a structure of -bounded treewidth can be done in time linear in the size of the structure. % TODO: referencja do Courcella +but \textcite{courcelle1990} showed that deciding if an MSO sentence holds in a +structure of bounded treewidth can be done in time linear in the size of the +structure. Similarly, query evaluation of MSO queries on bounded treewidth structures was -shown to be polynomial in the size of the structure and the output by Courcelle -and Mosbah. Their result was improved by Frick, Flum, and Grohe to linear time. +shown to be polynomial in the size of the structure and the output by +\textcite{courcelle1992}. Their result was improved by \textcite{flum2001} to +linear time. In this work, instead of evaluation, we will instead consider \definedterm{query answering}. In this setting, we are insterested in alrogithms that first @@ -161,8 +163,8 @@ being output. \textcite{bagan2006} introduced this second notion and showed that enumerating MSO queries is \lineardelaylin\ on trees. This in particular means that enumerating MSO queries for formulae whose free variables are all first order is in \constantdelaylin, and \textcite{kazana2013} revisit this result, -proving it using Colcombet's deterministic factorization forests rather than -Bagan's intricate indexing structure. +proving it using deterministic factorization forests due to \textcite{colcombet} +rather than Bagan's intricate indexing structure. Colcombet's result could likely be used to solve the problem of branch infix regular queries, which we introduce as a subproblem of MSO query answering in |