Title: Theory / Unimportant / CS / Fundamental / Model Checking / toSort / Safraless decision procedure
Tags: hasSeenConjDef récupéré

Name: A Safra tree
Definition: A labelled oriented tree \((T,f,e,M)\), with:
-\(T\subseteq\{1,\dots,2n\}\)
-\(f:T\to T^*\) a function mapping each node on the ordered sequence of its children,
-\(e:T\to\mathcal P(Q)\setminus\emptyset\), the labelling function
-\(M\subseteq T\), the set of marked nodes
-The root is 1
-\(M\) is a set of leaves
-\(\bigcup_{u\in f(v)}e(u)\subsetneq e(v)\)
-\(v,w\) not related by the ancestor relation implies \(e(v)\cap e(w)=\emptyset\)
Page: 47
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
Extra: Requirements are given other cards

Name: A set of direction
Typ: An arbitrary set
Page: 3
Section: 2
Denoted by: \(D\)

Name: A \(D\)-tree
Definition: A set \(T\subseteq D^*\) closed under prefix relation
Page: 3
Section: 2
Variables: \(D\) a set of directions

Name: A full \(D\)-tree
Definition: \(D^*\) as a \(D\)-tree
Page: 3
Section: 2
Variables: \(D\) a set of directions

Name: A path in \(T\)
Definition: A subset of \(T\), containing \(\epsilon\), and for each element it contains an unique successor, if such a successor exists.
Page: 3
Section: 2
Variables: \(D\) a set of directions,
\(T\) a \(D\)-tree

Name: A \(\Sigma\)-labelled \(D\)-tree
Definition: The pair \(\langle T,\tau\rangle\) with \(T\) a \(D\)-tree and \(\tau:T\to\Sigma\)
Page: 3
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet

Name: A transducer
Definition: \(S\) the set of states,
Page: 3
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet
Definition2: \(s_{in}\in S\),
Conjdef: \(\langle D,\Sigma, S,s_{in},\eta,L\rangle\) with
Definition3: \(\eta:S\times D\to S\), Its deterministic transition function
Definition4: \(L:S\to\Sigma\), Its labelling function
Denoted by: \(\mathcal T\)

Name: A regular \(\Sigma\)-labeled \(D\)-tree
Definition: The full \(D\)-tree whose labelling function is defined by a transducer
Page: 3
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet

Name: The size of \(\mathcal T\)
Page: 3
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal T\) a regular \(D\)-tree
Notation: The size of the minimal transducer which generates \(\mathcal T\)

Definition: The set of positive Boolean formulas over \(X\)
Page: 3
Section: 2
Variables: \(X\) a set
Notation: \(\mathcal B^+(X)\)

Name: \(Y\) satisfies \(\theta\)
Definition: \(\theta\) holds when elements of \(Y\) are assigned true and other elements are assigned false
Page: 4
Section: 2
Variables: \(X\) a set
\(\theta\in\mathcal B^+(X)\)
\(Y\subseteq X\)

Name: An alternating tree automaton
Definition: \(Q\) a set,
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
Definition2: \(q_{in}\in Q\),
Conjdef: \(\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) with
Definition3: \(\delta:Q\times\Sigma\to\mathcal B^+(D\times Q)\),
Definition4: \(\alpha\) an acceptance condition

Name: A run of \(\mathcal A\) on \(\langle T,\tau\rangle\)
Definition: A \((T\times Q)\)-labeled \(\mathbb N\)-tree \(\langle T_r,r\rangle\) such that:
-\(\epsilon\in T_r\), \(r(\epsilon)=\langle\epsilon,q_{in}\rangle\)
-for each \(y\in T_r\) with \(r(y)=\langle x,q\rangle\) and \(\delta(q,\tau(x))=\tau\), there is a set \(S=\{(c_i,q_i)\mid i\}\subseteq D\times Q\) such that \(S\) satisfies \(\theta\) and \(y\cdot y\in T_r\) and \(r(y\cdot i)=\langle x\cdot c_i,q_i\rangle\) for each \((c_i,q_i)\in S\)
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton,
\(\langle T,\tau\rangle\)

Name: An accepting run
Definition: A run whose all paths satisfy the acceptance condition.
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton,
\(\langle T,\tau\rangle\) \(\Sigma\)-labelled full \(D\)-tree

Definition: The set of state \(q\in Q\) such that there are infintely many \(y\in\pi\) such that \(r(y)\)'s second element is \(q\)
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton,
\(\langle T,\tau\rangle\) \(\Sigma\)-labelled full \(D\)-tree
\(\pi\) a path in \(T_r\)
Notation: \(inf(\pi)\)

Name: A parity acceptance condition
Definition: A finite set \(\{F_i\mid 1\le i\le h\}\) with \(F_i\subseteq F_{i+1}\) and \(F_h=Q\).
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton

Name: A path which satisfy the Büchi acceptance condition
Definition: A path \(\pi\) such that \(inf(\pi)\) intersects \(\alpha\)
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton
\(\langle T,\tau\rangle\) \(\Sigma\)-labelled full \(D\)-tree

Name: A path which satisfy the co-Büchi acceptance condition
Definition: A path \(\pi\) such that \(inf(\pi)\) is disjoint from \(\alpha\)
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton
\(\langle T,\tau\rangle\) a \(\Sigma\)-labelled full \(D\)-tree

Name: A path which satisfy the parity acceptance condition
Definition: A path \(\pi\) such that the minimal \(i\) such that \(inf(\pi)\) intersects \(F_i\) is even.
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\{F_i\mid 1\le i\le h\}\rangle\) an alternating tree automaton
\(\langle T,\tau\rangle\) \(\Sigma\)-labelled full \(D\)-tree

Name: The index of the automaton
Definition: \(h\)
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\{F_i\mid 1\le i\le h\}\rangle\) an alternating tree automaton

Name: A tree accepted by \(\mathcal A\)
Definition: A tree which admits a run which accepts it.
Page: 4
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) an alternating tree automaton

Name: A deterministic alternating automaton
Definition: An alterating automaton which is both non-deterministic and universal
Page: 5
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,

Name: A universal alternating automaton
Definition: An alternating automaton such that each formulas are conjunctions of atoms in \(D\times Q\)
Page: 5
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,

Name: A non-deterministic alternating automaton
Definition: An alterating automaton such that, when rewritten in DNF, each \(c\in D\) occurs at most once in each conjunct.
Page: 5
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,

Name: A word automaton
Definition: An alternating automaton when \(D=1\)
Page: 5
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,

Name: An alternating weak tree automaton
Definition: An alterating automaton whose set of sets is a totally pre-ordered set and each \(q'\) occuring in some \(\delta(q,\sigma)\) is at most \(q\).
Page: 5
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,

Definition: its branching mode satisfy \(X\)
Page: 5
Section: 2
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,
<\(X\in\{D,N,U, A\}\)
\(Y\in\{B,C,P,R,S,W\}\),
\(Z\in\{W,T\}\)
Notation: \(XYZ\)
Definition2: \(Y\) its acceptance condition
Conjdef: An alternating automaton such that
Definition3: \(Z\) depending on whether we consider word or tree

Smaller0: UCT
Greater0: APT
Page: 5
Section: 3
Smaller to greater: is less expressive than
Greater to smaller: is more expressive than
Counterexample: The language of \(\{0,1\}\)-labeled trees whose every pathes have finitely many \(x\) such that \(\tau(x)=0\)
Hide sides: yes

Name: Its equivalent \(UPT\)
Definition: \(,D,Q,q_{in},\delta,(alpha,Q)\rangle\)
Page: 5
Section: 3
Variables: \(D\) a set of directions,
\(\Sigma\) an alphabet,\(\mathcal A=\langle\Sigma,D,Q,q_{in},\delta,\alpha\rangle\) a UCT
Notation: is less expressive than
Typ: APT