From: Nathaniel Wesley Filardo Date: Thu, 27 Mar 2014 21:21:57 +0000 (-0400) Subject: Add section for TAGED X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=448726d1b5d8d98a0a56275b33d97da8b9d74a2d;p=autzoo Add section for TAGED Tweak other sections. Partially addresses github nwf/autzoo#2 . --- diff --git a/biblio.bib b/biblio.bib index 586be00..bc4a5c0 100644 --- 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 291ba1b..fc5a4fe 100644 --- 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 39c8d59..a486d36 100644 --- 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 317dcee..8e4a5da 100644 --- 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 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}, +}