Add section for TAGED

Tweak other sections.  Partially addresses github nwf/autzoo#2 .

diff --git a/biblio.bib b/biblio.bib
index 586be0089fdf184ca367ce00e8896ecce404cf8c..bc4a5c08765439150e345e8e1078011e6e1a43c7 100644 (file)
--- a/biblio.bib
+++ b/biblio.bib
@@ -153,6 +153,22 @@ mechanism. We combine the above constructions adequately to provide an algorithm
        keywords = {Algorithm Analysis and Problem Complexity, Computation by Abstract Devices, Discrete Mathematics in Computer Science, Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation}
 }
 
+@incollection{filiot:sltv,
+       location = {Berlin, Heidelberg},
+       title = {Satisfiability of a Spatial Logic with Tree Variables},
+       volume = {4646},
+       isbn = {978-3-540-74914-1, 978-3-540-74915-8},
+       url = {http://link.springer.com/10.1007/978-3-540-74915-8_13},
+       pages = {130-145},
+       booktitle = {Computer Science Logic},
+       publisher = {Springer Berlin Heidelberg},
+       author = {Filiot, Emmanuel and Talbot, Jean-Marc and Tison, Sophie},
+       editor = {Duparc, Jacques and Henzinger, Thomas A.},
+       urldate = {2014-03-27},
+       date = {2007},
+       langid = {english},
+}
+
 @article{aho:pa,
        title = {Syntax directed translations and the pushdown assembler},
        volume = {3},

diff --git a/main.tex b/main.tex
index 291ba1b128ca30dbb1ffd6e9dfa192b1577ad7a6..fc5a4fe7bc8a827d62d65658517facb523ef336c 100644 (file)
--- a/main.tex
+++ b/main.tex
@@ -214,6 +214,9 @@ or \url{http://www.gnu.org/licenses/agpl-3.0.txt}) or any later version.}}
 \newcommand{\stsf}{\ensuremath\mathcal{Q}_f}
 \newcommand{\stsi}{\ensuremath\mathcal{Q}_i}
 
+\newcommand{\lab}[1]{\ensuremath{\mbox{label}\paren{#1}}}
+\newcommand{\tr}[1]{\ensuremath{\mbox{label}\paren{#1}}}
+
 \newcommand{\maininclude}[2]{\section{#1} \label{sec:#2} \input{#2}}
 
 \newcommand{\Note}[1]{}
@@ -248,6 +251,7 @@ or \url{http://www.gnu.org/licenses/agpl-3.0.txt}) or any later version.}}
 \maininclude{Constraints Between Brothers}{zoo-tree/awcbb}
 \maininclude{Reduction Automata}{zoo-tree/ra}
 \maininclude{Homomorphism-Equality Automata}{zoo-tree/tahom}
+\maininclude{Tree Automata with Global Equality and Disequality}{zoo-tree/taged}
 \maininclude{Rigid Tree Automata}{zoo-tree/rta}
 
 %\part{Infinite Trees}

diff --git a/treeautintro.tex b/treeautintro.tex
index 39c8d597176265148699a44bab52c13bd5c6c4f9..a486d36075d2cbed30f78b77802849c8e306feed 100644 (file)
--- a/treeautintro.tex
+++ b/treeautintro.tex
@@ -45,6 +45,14 @@ are in $\Sigma$ must agree with the first projection of the run itself, and
 all positions of $t$ which are in $\config$ must be so-labeled by the run.
 \Note{That's not very clear, but I think it's right.}
 
+For a run $r$, we define $\tr(r|_p)$ to be the function which returns the
+$\Sigma$ of the original tree at position $p$. (Symbolically, $\tr =
+\pi_1$.)
+Similarly, we define 
+$\lab(r|_p)$ as the (partial) function which returns
+the output configuration at position $p$. ($\lab = \pi_2 \mbox{inr}^{-1}
+\pi_2$.)
+
 \subsection{Nondeterminism}
 
 \subsection{Plies}
@@ -54,6 +62,7 @@ where $\delta$ is restricted to manipulation of trees of the form
 $\mathcal{T}(\Sigma_+ \sqcup \config)$.
 
 \subsection{Local Constraints}
+\label{sec:treeaut:con:loc}
 
 A natural novelty of tree automata is one of {\em constraints} between
 positions in a (sub)tree.  One way of inducing such constraints is to

diff --git a/zoo-tree/rta.tex b/zoo-tree/rta.tex
index 317dcee2209e53cbd5de9d5af1d5046ba3421339..8e4a5dacbded7a54629db92a645c8c8f177fd279 100644 (file)
--- a/zoo-tree/rta.tex
+++ b/zoo-tree/rta.tex
@@ -8,9 +8,9 @@ root equal sub-trees.)
 
 
 \subsection{Relation to other classes}
-RTA are a strict sub-class of TAGED (\autoref{sec:zoo-tree/taged}; Sec. 3.1) but are a
-super-class of TAGED+ (at possible exponential complexity; see Prop. 2 and
-\cite{filiot:tagc}).
+RTA are a strict sub-class of TAGED (\autoref{sec:zoo-tree/taged};
+\cite[Sec. 3.1]{jacquemard:rta}) but are a super-class of TAGED+ (at
+possible exponential complexity; see Prop. 2 and \cite{filiot:tagc}).
 
 \Note{Other classes also discussed in Sec. 3: TAC, DAG automata, TA1M,
 ACRV.}

diff --git a/zoo-tree/taged.tex b/zoo-tree/taged.tex
new file mode 100644 (file)
index 0000000..854c67a
--- /dev/null
+++ b/zoo-tree/taged.tex
@@ -0,0 +1,33 @@
+Tree Automata with Global Equality and Disequality (TAGED) were introduced
+by \cite{filiot:sltv} and further results were published in
+\cite{filiot:tagc}.  A TAGED automaton is a regular tree automaton (with
+state set $\sts$) together with two relations:
+\begin{itemize}
+  \item $=_A \subset \sts^2$ reflexive and symmetric,
+  \item $\neq_A \subseteq \sts^2$ irreflexive and symmetric.
+\end{itemize}
+A run $r$ of a TAGED automaton is a run of the underlying regular automaton
+which additionally satisfies, for all positions $p$ and $p'$ in the run,
+\begin{itemize}
+  \item $\lab{r|_p} =_A    \lab{r|_{p'}} \Rightarrow \tr{r|_p} = \tr{r|_{p'}}$,
+  \item $\lab{r|_p} \neq_A \lab{r|_{p'}} \Rightarrow \tr{r|_p} \neq \tr{r|_{p'}}$.
+\end{itemize}
+
+\paragraph{Sub-classes} Polarized forms (``positive'' and ``negative'') are
+also defined as TAGED automata without disequalities (resp. equalities).  A
+``vertically bounded'' TAGED is an automaton in which there is a static
+bound on the number of globally-disequal states on each root-to-leaf path. 
+
+Unless otherwise indicated, references in this table are to
+\cite{filiot:tagc}.
+\autinfo{
+  member={NP-complete; Prop 1},
+  empty={Positive: EXPTIME-complete (Thm 1),
+         Negative: NEXPTIME-complete (Thm 2),
+         Vert. Bound: 2NEXPTIME (Thm 4)},
+  univ={No; Prop 5},
+  union={Yes, polarization-preserving; Prop 2},
+  intersect={Yes, polarization-preserving; Prop 2},
+  compl={No; Prop 4},
+  determinize={No; Prop 3},
+}