m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-10-14 14:37:13 +0200
committerMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-10-14 14:37:13 +0200
commit946e713c1a9df6f751538b62f6098431add67fc8 (patch)
tree528cd70f5353b5147f3d5b4711ae86d9350be9d2
parent518b9cc6d75555bc6c3a95bd6b734361de023079 (diff)
Add references in text
-rw-r--r--mgr.tex14
1 files changed, 8 insertions, 6 deletions
diff --git a/mgr.tex b/mgr.tex
index fd09164..d780602 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -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