Title: Theory / Unimportant / CS / Fundamental / Automata / Infinite / Perrin Pin+10 / 01 Definition
Tags: fromMath mathToDef récupéré mathToSee fromImplication fromAlgorithm closed omegaRecognizable hasNotNewEffectReturnsMeaning hasSeenConjDef omegaDeterministicRecognizable defToAlgebra setAdditionMultiplication typWTF counterExample mullerRecognizable omegaCoDeterministicRecognizable

Name: A rational set
Definition: letters
Page: 005
Chapter: 1
Kind: Table
Definition2: Union denoted \(\cup\)
Conjdef: Either
Definition3: concatenation, denoted \(\cdot\)
Definition4: finite iteration, denoted \(*\)
Definition5: infinite iteration, denoted \(\omega\)

Name: Letters
Definition: The elements of an alphabet.
Page: 006
Chapter: 1
Section: 2
Name2: Symbols

Name: Countable set
Definition: A set \(A\) such that there exists an injective map from \(A\) to \(\mathbb N\).
Page: 007
Chapter: 1
Section: 2

Q: [...], it is denoted [...].
A: A finite sequence of elements of \(A\); by mere juxtaposition
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.
Notation: A (finite) word on \(A\)

Question: The concatenation operation admits
Answer: a neutral element.
Page: 007
Chapter: 1
Section: 2

Page: 007
Chapter: 1
Section: 2
Name: The free-monoid on \(A\)
Set: The set of words on \(A\).
Variables: \(A\) be an alphabet.
Notation: \(A^*\)
*: Concatenation
1: Empty word
Zero divisors: \(\epsilon\)

Page: 007
Chapter: 1
Section: 2
Name: The free-semigroup on \(A\)
Set: The set of non-empty words on \(A\).
Variables: \(A\) be an alphabet.
Notation: \(A^+\)
*: Concatenation
Zero divisors: None

Definition: The number of occurrences \(a\) in \(u\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet,
\(a\in A\)
\(u\in A^*\).
Notation: \(|u|_a\)

Definition: The number of letters in \(u\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet and \(u\in A^*\).
Notation: \(|u|\)

Definition: \(u(r)\dots u(s)\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet, \(r\le s<n\), let \(u\) be a word on \(a\) of length at least \(n\).
Notation: \(u[r,s]\)

Definition: The set of infinite words on \(A\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.
Notation: \(A^{\mathbb N}\)
Notation2: \(A^\omega\)

Definition: \(A^*\cup A^\omega\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.
Notation: \(A^\infty\)

Name: A factor of \(v\)
Definition: \(u\in A^*\) such that \(u=v[s,r]\) for some \(s,r\in\mathbb N\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet
\(v\in A^\infty\).

Name: A left factor of \(v\)
Definition: A finite word \(u\) such that there exists \(w\in A^*\) such that \(v=uw\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet and \(v\in A^\infty\).
Name2: a prefix of \(v\)

Name: A suffix of \(v\)
Definition: A word \(x\) such that there exists \(w\in A^*\) such that \(v=wx\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet and \(v\in A^\infty\).
Name2: A right factor of \(v\)

Name: A proper factor \(v\)
Definition: A word \(u\) such that here exists \(x,y\in A^\infty\), at least one non-empty, such that \(xuy=v\).
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet
\(v\in A^\infty\)

Name: A strict factor \(v\)
Definition: A word \(u\) such that there exists \(x,y\in A^\infty\), both non-empty, such that \(xuy=v\).
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet and \(v\in A^\infty\).

Name: The prefix order
Definition: The relation «be a left factor of».
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.

Definition: \(u\le v\)
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet, and \(u,v\in A^\infty\).
Notation: \(u\le_{lex}v\)
Definition2: \(u=xau'\) and \(v=xbv'\) with \(u',v'\in A^\infty\), \(a,b \in A\) and \(a< b\).
Conjdef: either

Name: A period of \(u\)
Definition: \(p\in\mathbb N\) such that for all \(k\in\mathbb N\), \(u_k=u_{k+p}\) when \(y_{k+p}\) is defined.
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet, and \(u\in A^\infty\).

Name: An ultimate period of \(u\)
Definition: \(p\in\mathbb N\) such that there exists \(k_0\ge0\) such that for all \(k\ge k_0\), \(a_k=a_{k+p}\).
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet, and \(u\in A^\omega\).

Name: Ultimately periodic word
Definition: An infinite word \(u\in A^\omega\) which admits an ultimate period.
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet.

Name: The shift of \(u\)
Definition: The infinite word \(v\in A^\omega\) such that \(v_i=u_{i+1}\); that is, the word \(u\) without its first letter.
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet
\(u\in A^\omega\)
Notation: \(\sigma(u)\)

Name: Stable subet of \(A^\omega\)
Definition: A set \(X\) such that \(\sigma(X)\subseteq X\).
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet

Name: A shift-invariant \(\omega\)-language
Definition: An \(\omega\)-language \(X\) such that \(\sigma(X)= X\).
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet.

Smaller0: \(p\) is a period of \(u\)
Greater0: \(\sigma^p(u)=u\)
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet,
\(p\in\mathbb N\)
\(u\in A^\omega\).
Smaller to greater: iff

Name: Prefix-free language
Definition: The elements of \(X\) are incomparable for the prefix relation.
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet
\(X\subseteq A^*\).
Name2: Prefix language

Name: Prefix-closed language
Definition: A language which contains the prefixes of all of its elements.
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.

Smaller0: the complement of \(X\) is prefix-closed
Greater0: \(X\) is a right ideal
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet,
\(X\subseteq A^*\).
Hide middle: yes
Extra: counter example ?

Name: A tree
Definition: \(N\) is a nonempty set whose elements are called nodes of the tree
Page: 009
Chapter: 1
Section: 2
Definition2: \(r\) is a distinguished element of \(N\) called the root of the tree
Conjdef: A tuple \((N,r,p)\) where
Definition3: \(p:N\setminus\{r\}\to N\) is a mapping associating with each node distinct from the root a unique node called its parent
Definition4: such that, for each node \(n\in N\), there is an integer \(k\ge0\) such that \(p^k(n)=r\).

Name: A child of \(n\)
Definition: An element \(m\in N\) such that \(p(m)=n\).
Page: 009
Chapter: 1
Section: 2
Variables: \((N,r,p)\) be a tree
\(n\in N\).

Name: Parent of \(n\)
Definition: \(p(n)\).
Page: 009
Chapter: 1
Section: 2
Variables: \((N,r,p)\) be a tree
\(n\in N\)

Name: An ancestor of \(n\)
Definition: \(p^k(n)\) for some \(k\in\mathbb N\).
Page: 009
Chapter: 1
Section: 2
Variables: \((N,r,p)\) be a tree and \(n\in N\).

Name: A descendant of \(n\)
Definition: An element \(m\) such that \(p^k(m)=n\).
Page: 009
Chapter: 1
Section: 2
Variables: \((N,r,p)\) be a tree
\(n\in N\).

Name: The subtree rooted at \(n\)
Definition: \((N_n,n,p_n)\), where \(N_n\) is the set of descendants of \(n\) and \(p_n\) is the restriction of \(p\) to \(N_n\).
Page: 009
Chapter: 1
Section: 2
Variables: \((N,r,p)\) be a tree
\(n\in N\)

Question: The tree associated to \(X\) is
Answer: \((X,\epsilon,\sigma)\).
Page: 010
Chapter: 1
Section: 2
Variables: \(X\) be a prefix-closed set on alphabet \(A\)

Name: The arity of \(n\)
Definition: The number of children of \(n\).
Page: 010
Chapter: 1
Section: 2
Variables: \((N,r,p)\) be a tree
\(n\in N\).

Name: An oriented tree
Definition: A tree, with a function \(f:N\to N^*\) associating to each node the ordered list of its children.
Page: 010
Chapter: 1
Section: 2

Name: Equivalent oriented trees
Definition: Two oriented trees \(T=(N,r,f)\) and \(T'=(N',r',f')\) such that there exists a bijection \(\sigma:N\to N'\) such that \(\sigma(r)=r'\) and for all \(n\in N\), \(\sigma(f(n))=f(\sigma(n))\).
Page: 010
Chapter: 1
Section: 2

Name: A planar tree
Definition: A class of trees under the equivalence relation.
Page: 010
Chapter: 1
Section: 2

Name: A labelled tree
Definition: A pair \((T,e)\) of a tree \(T\) and a function \(e:N\to V\) from \(N\) into a set \(V\) of labels.
Page: 012
Chapter: 1
Section: 2
Kind: Proposition

Name: A path from \(n\) to \(m\)
Definition: A sequence \(n=n_0,n_1,\dots,n_k=m\) such that \(n_{i}\) is the parent of \(n_{i+1}\).
Page: 012
Chapter: 1
Section: 2
Variables: \(T\) be a tree, and \(n,m\in N\).
Kind: Proposition

Q: -[...]
-[...]
-[...]
A: union; set product: \(XY=\{xy\mid x\in X,y\in Y\}\); star operation: \(X^*=\{x_1\dots x_n\mid n\ge 0\text{ and }x_i\in X\}\)
Page: 13
Chapter: 1
Section: 3
Variables: \(S\) a semigroup.
Name: Rational operations

Name: The class of rational subsets of \(S\)
Definition: The smallest class containing finite set and closed under rational operations.
Page: 13
Chapter: 1
Section: 3
Variables: \(S\) a semigroup.

Name: A rational expression
Definition: Expressions using symbols from the alphabet \(A\), \(\cup,\cdot,^+,^*\)
Page: 13
Chapter: 1
Section: 3
Variables: \(A\) an alphabet

Definition: \(\left\{x_0x_1\dots\mid \forall i\ge0, x_i\in X\setminus \{1\}\right\}\).
Page: 14
Chapter: 1
Section: 3
Variables: \(S\) a semigroup
\(X\subseteq S\).
Notation: \(X^\omega\)

Definition: \(X^*\cup X^\omega\)
Page: 14
Chapter: 1
Section: 3
Variables: \(S\) a semigroup
\(X\subseteq S\)
Notation: \(X^\infty\)

Definition: \((X+Y)^\omega\)\(=(X^*Y)^\omega+(X+Y)^*X^\omega\)
Page: 14
Chapter: 1
Section: 3
Variables: \(A\) an alphabet
\(X,Y\subseteq A^*\).
Index: 1 (1)
Kind: Prop

Definition: \((XY)^\omega\)\(=X(YX)^\omega\)
Page: 14
Chapter: 1
Section: 3
Variables: \(A\) an alphabet and \(X,Y\subseteq A^*\).
Index: 1 (1)
Kind: Prop

Question: \(XX^\omega=\)
Answer: \(X^\omega\)
Page: 14
Chapter: 1
Section: 3
Variables: \(A\) an alphabet and \(X,Y\subseteq A^*\).
Index: 1 (2)
Kind: Prop

Question: \((X^+)^\omega=\)
Answer: \(X^\omega\)
Page: 14
Chapter: 1
Section: 3
Variables: \(A\) an alphabet and \(X,Y\subseteq A^*\).
Index: 1 (3)
Kind: Prop

Name: An alphabetic morphism
Definition: A function from \(A\) to \(B\).
Page: 16
Chapter: 1
Section: 3
Variables: \(A, B\) alphabets

Definition: \(\{\phi(x)\mid x\in X\}\).
Page: 16
Chapter: 1
Section: 3
Variables: \(A, B\) alphabets, \(X\subseteq A^\infty\) and \(\phi:A^+\to B^+\)
Notation: \(\phi(X)\)

Name: The class of \(\omega\)-rational sets
Page: 16, 29
Section: 3
Chapter: 1
Index: 3.3 5.5
Kind: Prop
Under: morphism
Under2: inverse of morphism
Under3: quotient ?
Under4: union?

Name: An automaton
Definition: \((Q,A,E)\) or \((Q,A,E,I,F)\) where \(A\) is an alphabet, \(Q\) the set of states, \(E\subseteq Q\times A\times Q\), \(I,F\subseteq Q\).
Page: 16
Chapter: 1
Section: 4

Name: A finite automaton
Definition: An automaton with a finite set of states and alphabet.
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton

Name: A countable automaton
Definition: An automaton with a countable set of states and alphabet.
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton

Name: Consecutive transitions
Definition: A pair of transitions of the form \((p,a,q)\) and \((q,a',r)\).
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton.

Name: A (in)finite path in \(\mathcal A\)
Definition: A (in)finite sequence of consecutive transitions.
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton.

Name: The origin of the path
Definition: \(q_0\).
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton and \(e_0=(q_0,a_0,q_1), e_1=(q_1,a_1,q_2),\dots\) a (in)finite path.

Q: [...] is [...].
A: The end of the path; \(q_{n+1}\) if it contains \(n\) transitions
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton and \(e_0=(q_0,a_0,q_1), e_1=(q_1,a_1,q_2),\dots\) a (in)finite path.

Q: [...] is [...].
A: The label of the path; \(a_0a_1\dots\)
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton and \(e_0=(q_0,a_0,q_1), e_1=(q_1,a_1,q_2),\dots\) a (in)finite path.

Name: A state visited by the path
Definition: A state \(q_i\).
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton
\(e_0=(q_0,a_0,q_1), e_1=(q_1,a_1,q_2),\dots\) a (in)finite path.
Name2: A state passed through by the path

Definition: The set of infinitely repeated states.
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A\) an automaton
\(e_0=(q_0,a_0,q_1), e_1=(q_1,a_1,q_2),\dots\) an infinite path \(p\).
Notation: \(\text{Inf}(p)\)

Name: A final path
Definition: A path \(e_0=(q_0,a_0,q_1),\dots, e_n=(q_n,a_n,q_{n+1})\) with \(q_{n+1}\in F\).
Page: 16
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\) an automaton.

Name: Successful path
Definition: Path which is both initial and final.
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\) an automaton.

Name: The set of words recognized by \(\mathcal A\)
Definition: The set of labels of successful path in \(\mathcal A\).
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\) an automaton
Notation: \(\mathcal L^*(\mathcal A)\)

Name: A recognisable (finite) language
Definition: recognized by a finite automaton.
Page: 17, 22
Chapter: 1
Section: 3, 4
Variables: \(A\) an alphabet
Index: 4
Kind: Theo,
Definition2: rational
Conjdef: A language, equivalently

Q: In the representation of an automaton [...]
A: the initials states
Page: 18
Chapter: 1
Section: 4
Denotedby: 2

Q: In the representation of an automaton [...].
A: the final states
Page: 18
Chapter: 1
Section: 4
Denotedby: outgoing arrow

Name: Automaton with deterministic transition
Definition: An automaton such that for all \(q\in Q\) and \(a\in A\), there is at most one state \(q'\) such that \((q,a,q')\in E\).
Page: 18
Chapter: 1
Section: 4

Name: Deterministic finite automaton
Definition: Automaton with deterministic transition and a unique initial state.
Page: 18
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\)

Name: The transition function
Definition: The function mapping \((q,a)\in Q\times A\) to the only state \(q'\) such that \((q,a,q')\in E\).
Page: 18
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\) deterministic,
Context: Automata
Notation: \(\cdot \)

Definition: \(((q\cdot a)\cdot w)\)
Page: 18
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\) deterministic, \(q\in Q\), \(a\in A\) and \(w\in A^+\)
Notation: \((q\cdot aw)\)

Definition: The set of states \(q\) which are the end of a path in \(\mathcal A\) with label \(w\) going out from some state of \(S\)
Page: 18
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\),
\(S\subseteq Q\), and
\(w\in A^*\)
Notation: \(\delta(q,w)\)

Name: The deterministic version of \(\mathcal A\)
Definition: \(\left(\mathcal P(Q),A,\delta,I,\{P\subseteq Q\mid P\cap Q\ne \emptyset\} \right)\)
Page: 19
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\)
Kind: Prop

Question: The set recognized by the deterministic version of \(\mathcal A\) is
Answer: the set recognized by \(\mathcal A\).
Page: 19
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\)

Name: The set of recognisable subsets of \(A^*\)
Page: 20
Section: 4
Chapter: 1
Index: 2
Variables: \(A\) an alphabet
Kind: Prop
Under: union
Condition: finite
Under2: intersection
Under3: set difference
Under4: Concatenation?
Under5: Left/right quotient?
Under6: Complement?
Under7: Morphism ?
Under8: Inverse of morphism

Name: The reversed automaton
Definition: \((Q,A,E^r)\) with \(E^r\) defined as \(\{(q,a,b)\mid (p,a,q)\in E\}\).
Page: 20
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\)
Notation: \(\mathcal A^r\)

Name: An automaton with a co-deterministic transition
Definition: An automaton \(\mathcal A\) such that \(\mathcal A^r\) is deterministic.
Page: 20
Chapter: 1
Section: 4

Q: \(\mathcal A\) is [definition] if [...]
A: unambiguous; for all \(p,q\in Q\), \(w\in A^*\), there is at most one path from \(p\) to \(q\) labelled by \(w\)
Page: 20
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E)\)

Name: The transition matrix of \(\mathcal A\)
Definition: A \(Q\times Q\) matrix, whose \((p,q)\)-th coefficient is \(\{a\in A\mid (p,a,q)\in E\}\).
Page: 20
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E)\)

Smaller0: \(\mathcal A\) is deterministic and co-deterministic
Greater0: \(\mathcal A\) is unambiguous
Page: 20
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E)\)
Hide middle: yes

Question: \((X^n)^\omega=\)
Answer: \(X^\omega\)
Page: 14
Chapter: 1
Section: 3
Variables: \(A\) an alphabet, \(n>0\) and \(X,Y\subseteq A^*\).

Definition: \(\{xy\mid x\in X,y\in Y\}\)
Page: 20
Chapter: 1
Section: 3
Variables: \(A\) an alphabet and \(X,Y\subseteq\mathcal P(A^*)\)
Notation: \(XY\)

Definition: The matrix whose \((p,q)\)-th component is \(M_{p,q}+N_{p,q}\).
Page: 20
Chapter: 1
Section: 3
Variables: \(A\) an alphabet,
\(M,N\subseteq\mathcal P(A^*)^{Q\times Q}\)
\(Q\) a set of states
Notation: \((M+N)\)

Definition: The matrix whose \((p,q)\)-th component is \(\sum_{r\in Q}M_{p,r}N_{r,q}\).
Page: 21
Chapter: 1
Section: 3
Variables: \(A\) an alphabet, \(M,N\subseteq\mathcal P(A^*)^{Q\times Q}\) and \(Q\) a set of states
Notation: \(MN\)

Definition: \(\sum _{n\ge 0}T^n\).
Page: 21
Chapter: 1
Section: 3
Variables: \(A\) an alphabet,
\(Q\) a set of states
\(T\subseteq\mathcal P(A^*)^{Q\times Q}\)
Notation: \(T^*\)

Q: [...] is the unique solution of [...].
A: \(T^*\); \(X=1+XT\)
Page: 21
Chapter: 1
Section: 3
Variables: \(A\) an alphabet, \(T\subseteq\mathcal P(A^*)^{Q\times Q}\) and \(Q\) a set of states

Smaller0: \(L\) is recognisable
Page: 22
Chapter: 1
Section: 3
Variables: \(A\) an alphabet
\(L\subseteq A^*\)
Index: 4
Kind: Theo
Smaller to greater: iff

Name: A Büchi automaton
Definition: An automaton.
Page: 25
Chapter: 1
Section: 5

Name: Final infinite path
Definition: A path which visits \(F\) infinitely often.
Page: 25
Chapter: 1
Section: 5
Variables: \(\mathcal A\) a Büchi automaton.

Name: Successful path
Definition: Initial and final path
Page: 25
Chapter: 1
Section: 5
Variables: \(\mathcal A\) a Büchi automaton.

Definition: The set of infinite word recognized by \(\mathcal A\).
Page: 25, 36
Chapter: 1
Section: 5
Variables: \(\mathcal A\) a Büchi automaton.
Notation: \(L^\omega(A)\)
Definition2: \(\overrightarrow{L^+(\mathcal A)}\) (assuming \(\mathcal A\) deterministic)

Definition: recognized by a Büchi automaton \(\mathcal A\).
Page: 25, 340, 346
Chapter: 1, VIII, VIII
Section: 5, 3, 3
Variables: \(A\) an alphabet
Notation: A recognisable \(\omega\)-language
Definition2: defined in \(\exists MF_2(<)\) with existential quantification in front and then first-order formula
Conjdef: A language in \(A^\omega\)
Definition3: defined in \(WMF_2(<)\) with existential quantification in front and then first-order formula

Name: An \(\omega\)-unambiguous Büchi automaton
Definition: A Büchi automaton such that each infinite words is the label of at most one infinite path.
Page: 25
Chapter: 1
Section: 5

Name: Co-deterministic Büchi automaton
Definition: A Büchi automaton whose transition function is co-deterministic and any word in \(A^\omega\) is the label of at most one final path.
Page: 25
Chapter: 1
Section: 5
Variables: \(\mathcal A\)

Name: A co-complete Büchi automaton
Definition: A Büchi automaton such that any word in \(A^\omega\) is the label of at least one final path.
Page: 25
Chapter: 1
Section: 5

Smaller0: \(\mathcal A\) is (co)-deterministic
Greater0: \(\mathcal A\) is unambiguous
Page: 25
Chapter: 1
Section: 5
Variables: \(\mathcal A\) a Büchi automaton.

Q: \(\mathcal A\) is [...] if [...].
A: complete; any word in \(A^\omega\) is the label of at least one initial path
Page: 25
Chapter: 1
Section: 5
Variables: \(\mathcal A\) a Büchi automaton.

Smaller0: \(X\) is nonempty recognisable
Greater0: an ultimately periodic word
Page: 27
Chapter: 1
Section: 5
Variables: \(A\) an alphabet
\(X\subseteq A^\omega\)
Kind: Lem
Prefix Greater: \(X\) contains

Name: Accessible state
Definition: A state with a finite initial path in \(\mathcal A\) ending in it.
Page: 27
Chapter: 1
Section: 5
Variables: \(\mathcal A\) an automaton.

Name: Co-accessible state
Definition: A state from which there is an infinite final path in \(\mathcal A\).
Page: 27
Chapter: 1
Section: 5
Variables: \(A\) an alphabet, \(\mathcal A\) a Büchi automaton

Name: Trim automaton
Definition: An automaton where each state \(q\) is accessible and co-accessible.
Page: 27
Chapter: 1
Section: 5

Triming an automaton:
-conserve being deterministc
-conserve finiteness.
Page: 27
Chapter: 1
Section: 5
Index: 2
Kind: Prop

Transforming an automaton into a complete one:
-conserve being deterministc
-conserve finiteness.
Page: 27
Chapter: 1
Section: 5
Index: 3
Kind: Prop

Definition: The set of states occuring infinitely often in \(r\)
Page: 5
Variables: \(A\) an automaton,
\(r\) a run on \(A\)
Notation: \(lim(r)\)

Smaller0: \(L_\omega(A_1\times A_2)\)
Greater0: \(L_\omega(A_1)\cap L_\omega(A_2)\)
Page: 5
Variables: \(A_i\) automata,
Smaller to greater: \(\subseteq\)
Greater to smaller: \(\supseteq\)

Question: \(L_\omega(A_1\times A_2)\) is
Answer: The set of words going infinitely often and simultaneously in accepting states of both automata
Page: 5

Name: The neutral element of concatenation
Page: 7
Chapter: 1
Section: 2
Notation: \(\epsilon\)

Question: \(X^+X^\omega\) equals
Answer: \(X^\omega\)
Page: 14
Chapter: 1
Section: 3
Index: 1(2)
Kind: Prop

Name: recognisable subsets of \(B^\omega\)
Page: 29
Section: 5
Chapter: I
Kind: Prop
Under: inverse of morphism

Definition: The set of words \(u\in A^\omega\) having infinitely many prefixes in \(L\).
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(L\subseteq A^*\)
Notation: \(\vec L\)

Question: \(\overrightarrow{a^*b}\) is
Answer: \(\emptyset\)
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(L\subseteq A^*\)
Index: 1
Kind: Ex

Question: \(\overrightarrow{(ab)^+}\) is
Answer: \((ab)^\omega\)
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(L\subseteq A^*\)
Index: 1
Kind: Ex

Question: \(\overrightarrow{(a^*b)^+}\) is
Answer: \((a^*b)^\omega\)
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(L\subseteq A^*\)
Index: 1
Kind: Ex

Smaller0: \(\overrightarrow{L^+(\mathcal A)}\)
Greater0: \(L^\omega(\mathcal A)\)
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(\mathcal A\) a Büchi automaton
Index: 1
Kind: Prop
Smaller to greater: equals
Assuming: \(\mathcal A\) deterministic

Name: A deterministic subset of \(A^\omega\)
Definition: A subset of \(A^\omega\) recognized by a deterministic Büchi automaton
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet
Index: 1
Kind: Prop

Smaller0: \(X\) is of the form \(\vec L\) for some \(L\subseteq A^+\)
Greater0: \(X\) is recognisable by a deterministic Büchi automaton
Page: 32
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 2
Kind: Theo
Smaller to greater: iff

Smaller0: \(X\) can be recognized by a countable deterministic automaton
Greater0: \(X\) is recognisable by a countable deterministic Büchi automaton
Page: 31
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 2
Kind: Theo
Smaller to greater: iff
Assuming: \(A\) is countable

Smaller0: \(X=\vec L\) for some \(L\subseteq A^+\) recognisable
Greater0: \(X\) is is recognized by a finite deterministic Büchi automaton
Page: 33
Chapter: I
Section: 6
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 3
Kind: Cor
Smaller to greater: iff

Name: The class of deterministic subset of \(A^\omega\)
Page: 33
Section: 6
Chapter: I
Index: 4
Variables: \(A\) an alphabet
Kind: Prop
Under: union
Under2: intersection
Not3: not
Under3: complementation

Question: Construction of the automaton accepting the intersection of those two automata ?
Answer: \((Q_1\times Q_2\times\{0,1\},A,\delta, (i_1,i_2,1),Q_1\times F_2\times 1)\).
The third element of the state memorizes the fact that the current path has visited a state of \(F_1\) since its last visit to \(F_2\). So the states of \(F_1\) are accepting only once between to visits to \(F_2\).
Page: 33
Chapter: I
Section: 6
Variables: \(\mathcal A_1,\mathcal A_2\) deterministic Büchi automata
Index: 4
Kind: Prop

Name: A Muller automaton
Definition: \((Q,A,E)\) a finite deterministic automaton
Page: 35
Chapter: I
Section: 7
Variables: \(A\) an alphabet
Definition2: \(i\in Q\) the initial state,
Conjdef: \((Q,A,E,i,\mathcal T)\), with
Definition3: \(\mathcal T\subseteq \mathcal P(Q)\) the table of the automaton

Name: Its initial state
Page: 35
Chapter: I
Section: 7
Variables: \(A\) an alphabet,
\(\mathcal A\) a muller automaton
Denoted by: \(i\)
DefType: An element of \(Q\)

Name: The table of the automaton
Typ: A subset of \(\mathcal P(Q)\)
Page: 35
Section: 7
Chapter: I
Variables: \(A\) an alphabet,
\(\mathcal A\) a muller automaton
Denoted by: \(\mathcal T\)

Name: An initial path
Definition: A path starting at \(i\)
Page: 35
Chapter: I
Section: 7
Variables: \(A\) an alphabet,
\((Q,A,E,i,\mathcal T)\) a muller automaton

Name: A final path
Definition: A path \(p\) such that \(Inf(p)\in\mathcal T\)
Page: 35
Chapter: I
Section: 7
Variables: \(A\) an alphabet,
\((Q,A,E,i,\mathcal T)\) a muller automaton

Name: A successful path
Definition: An initial final path
Page: 35
Chapter: I
Section: 7
Variables: \(A\) an alphabet,
\((Q,A,E,i,\mathcal T)\) a muller automaton

Smaller0: \(L\) is recognized by a Muller automaton
Greater0: \(L\) is \(\omega\)-rational
Page: 35, 37
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(L\subseteq A^\omega\)
Index: 1, 2
Kind: Theo, Prop
Extra: counter example ?
Greater2: a trim Muller automaton
Connect Greater1: and \(L\) is recognized by
Greater3: a complete Muller automaton
Connect Greater2: and by

Name: An admissible set of states
Definition: A set \(T\subseteq Q\) such that there exists an infinite inital path \(p\) such that \(Inf(p)=T\)
Page: 36
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,i,\mathcal T)\) a Muller automaton

Name: A Trim Muller automaton
Definition: An automaton whose every states are accessible and co-accessible, and whose final sets are admissible.
Page: 36
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet

Name: A co-accessible state
Definition: A state \(q\) such that there is an infinite final path starting in \(q\)
Page: 36
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(\mathcal A\) a muller automaton

Name: An accessible state
Definition: A state \(q\) such that there is an initial path ending in \(q\)
Page: 36
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(\mathcal A\) a muller automaton

Page: 36
Implementation: Computing the SCC. Testing whether \(T\) belongs to a SCC
Section: 7.1
Chapter: I
Effect: Testing whether \(T\) is admissible
Variables: \(A\) an alphabet,
\(\mathcal A\) a muller automaton
\(T\subseteq Q\)

Page: 36
Implementation: Computing the SCC. Testing whether each leaf accessible form \(q\) contains an accepting state
Section: 7.1
Chapter: I
Effect: Testing whether \(q\) is co-accessible
Variables: \(A\) an alphabet,
\(\mathcal A\) a muller automaton
\(q\in Q\)

Smaller0: \(\bigcap_iL^\omega(\mathcal A_i)\)
Greater0: \(L^\omega(\prod\mathcal A_i)\)
Page: 38
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(\mathcal A_i=(Q_i,A,E_i,i_i,\mathcal T_i)\) Muller automata
Index: 5
Kind: Prop
Smaller to greater: is equal to

Smaller0: \(X\) is a Boolean combination of subsets of \(A^\omega\) recognisable by finite Büchi determinstic automata
Greater0: \(X\) is recogized by a Muller automaton
Page: 38
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Smaller to greater: iff

Question: Boolean combination of determinstic Büchi automata accepting \(L^\omega(\mathcal A)\)
Answer: \(\bigcup_{T\in\mathcal T}\bigcup_{t\in T}L^\omega(E,i,t)\setminus \bigcup_{t\not\in T}L^\omega(E,i,t)\)
Page: 38
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,i,\mathcal T)\) a Muller automaton

Page: 38
Implementation: \((Q,A,E,i,\{T\mid T\cap \mathcal T\ne\emptyset\})\)
Section: 7.1
Chapter: I
Effect: A Muller automaton accepting the same language.
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,i,\mathcal T)\) a determinstic Büchi automatona

Name: A Rabin automaton
Definition: \((Q,a,E)\) a deterministic automaton
Page: 39
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet
Definition2: \(i\in Q\) the initial state,
Conjdef: A tuple \((Q,A,E,i,\mathcal R)\) with
Definition3: \(\mathcal R=\left\{(L_j,U_j)\mid j\in J\right\}\) a famility of pair of set of states

Name: A successful path
Definition: An infinite path visiting finitely often \(L_j\) and infinitely often \(U_j\) for some \(j\in J\)
Page: 39
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet,
\((Q,A,E,i,\{L_j,U_j\mid j\in J\})\) a Rabin automaton

Question: A Rabin automaton accepting \(L(\mathcal A)\).
Answer: \((Q,A,E,i,\{(\emptyset, F)\})\)
Page: 39
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,i,F)\) a determinstic Büchi automatona

Smaller0: \(X\) is accepted by a finite Rabin automaton
Greater0: \(X\) is accepted by a Muller automaton
Page: 39
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 7
Kind: Prop
Smaller to greater: iff

Smaller0: \(X\) is accepted by a Rabin automaton with \(n\) pairs
Greater0: \(X\) is a union of \(n\) differences of recognisable determinstic subsets of \(A^\omega\)
Page: 39
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 7
Kind: Prop
Smaller to greater: iff

Page: 39
Implementation: \((Q,A,E,i,\mathcal T)\) with \(\mathcal T\) the set of \(T\subseteq Q\) disjoint from \(L_j\) and intersecting \(U_j\) for some \(j\)
Section: 7.2
Chapter: I
Effect: An equivalent Muller automaton
Variables: \(A\) an alphabet,
\((Q,A,E,i,\{L_j,U_j\mid j\in J\})\) a Rabin automaton
Index: 7
Kind: Prop

Name: A Streett automaton
Definition: \((Q,a,E)\) a deterministic automaton
Page: 41
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet
Definition2: \(i\in Q\) the initial state,
Conjdef: A tuple \((Q,A,E,i,\mathcal S)\) with
Definition3: \(\mathcal S=\left\{(L_j,U_j)\mid j\in J\right\}\) a famility of pair of set of states

Name: A successful path
Definition: An infinite initial path such that, for each \(j\in J\), either it visits \(L_j\) a finite number of times, or it visits \(U_j\) an infinite number of times.
Page: 41
Chapter: I
Section: 7.2
Variables: \(A\) an alphabet,
\((Q,A,E,i,\{L_j,U_j\mid j\in J\})\) a Streett automaton

Name: A Muller automaton with full table
Definition: -for every admissible set \(T\in\mathcal T\) and for every admissible set \(T'\) containing \(T\), \(T'\in\mathcal T\)
Page: 41
Chapter: I
Section: 7.3
Variables: \(A\) an alphabet
Conjdef: A Muller automaton \(\mathcal A=(Q,A,E,i,\mathcal T)\) such that

Smaller0: \(\mathcal A\)'s table is full
Greater0: \(\mathcal A\) is equivalent to a finite determinstic Büchi automaton
Page: 41
Chapter: I
Section: 7.3
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,i,\mathcal T)\) a Muller automaton
Smaller to greater: iff

Page: 42
Implementation: \((\mathcal P(Q)\times Q,(\emptyset,i),\{\emptyset\}\times Q\})\) with:
\[(S,q)\cdot a=\left\{\begin{array}{ll}(\emptyset,q\cdot a)&\text{if $S\cup \{q\cdot a\}$ contains an element of $\mathcal T$}\\ (S\cup \{q\cdot a\},q\cdot a)&\text{otherwise}\end{array}\right.\]
The state \((S,q)\) corresponds to: a state \(q\), and the set of states crossed since last time \(S\) belonged to \(\mathcal T\)
Section: 7.3
Chapter: I
Effect: Equivalent finite deterministic Büchi automaton
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,i,\mathcal T)\) a Muller automaton
Assuming: \(\mathcal A\) with full table

Name: A transition Büchi automaton
Definition: A \(5\)-tuple \((Q,A,E,I,F)\) where:
-\((Q,A,E)\) is a finite automaton,
-\(I\subseteq Q\),
-\(F\subseteq E\)
Page: 43
Chapter: I
Section: 8
Variables: \(A\) an alphabet

Name: Its set of final transitions
Typ: Subset of \(E\)
Page: 43
Section: 8
Chapter: I
Variables: \(A\) an alphabet,
\(\mathcal A\) a transition Büchi automaton
Denoted by: \(F\)
Notation: circled letters in the automaton's representation

Name: A final path
Definition: A path going through \(F\) infinitely often
Page: 43
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) a transition Büchi automaton

Name: A successful path
Definition: An initial final path
Page: 43
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) a transition Büchi automaton

Name: A transition Muller automaton
Definition: \((Q,A,E)\) is a finite automaton,
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet
Definition2: \(I\subseteq Q\),
Conjdef: A \(5\)-tuple
Definition3: \(\mathcal T\subseteq \mathcal P(E)\)

Definition: The set of transitions taken infinitely often by \(p\)
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) a transition Büchi automaton,
\(p\) a path
Notation: \(\text{Inf}_{\mathcal T}(p)\in\mathcal T\)

Name: A final path
Definition: A path such that \(\text{Inf}_{\mathcal T}(p)\in\mathcal T\)
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) a transition Büchi automaton

Smaller0: \(X\) is accepted by a Büchi automaton
Greater0: \(X\) is accepted by a transition Büchi automaton
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 1
Kind: Prop
Smaller to greater: iff

Smaller0: \(X\) is accepted by a co-deterministic Büchi automaton
Greater0: \(X\) is accepted by a co-deterministic transition Büchi automaton
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet
\(X\subseteq A^\omega\)
Index: 1
Kind: Prop
Smaller to greater: iff
Context: Infinite alphabet

Smaller0: \(X\) is accepted by a co-complete Büchi automaton
Greater0: \(X\) is accepted by a co-complete transition Büchi automaton
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(X\subseteq A^\omega\)
Index: 1
Kind: Prop
Smaller to greater: iff

Question: Equivalent transition Büchi automaton.
Answer: \((Q,A,E,I,\{(p,a,q)\in E\mid p\in F\})\)
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) a Büchi automaton
Index: 1
Kind: Prop

Question: Equivalent Büchi automaton.
Answer: \((Q\times\{\top,\bot\},A,E',I\times\{\top,\bot\},\{(p,\top)\in (p,\_,\_)\in F\})\) with \(E'\) containing [$]((p,\llbracket(p,a,q)\in F\rrbracket),a,(q,\_))[/$] for \((p,a,q)\in E\).
Page: 44
Chapter: I
Section: 8
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) a transition Büchi automaton
Index: 1
Kind: Prop

Page: 45
Implementation: \((E\cup\{j\},A,E',j,\mathcal T)\) with:
-\(j\) a new state
-\(E'\) contains \((j,a,(i,a,q))\) for \((i,a,q)\in E\) and \(\left((q_1,a_1,q_2),a_2,(q_2,a_2,q_3)\right)\) for \((q_{i},a_i,q_{i+1})\in E\),
Section: 8
Effect: Its equivalent transition Muller automaton.
Variables: \((Q,A,E,i,\mathcal T)\) a Muller automaton

Question: Its equivalent Muller automaton
Answer: exists
Page: 45
Section: 8
Variables: \((Q,A,E,i,\mathcal T)\) a transition Muller automaton
Index: 2
Kind: Prop
Extra: Not described

Name: The child function of the tree
Typ: \(T\to T^*\)
Page: 47
Section: 9
Chapter: 1
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\)
Notation: \(f\)

Name: Its labelling function
Typ: \(T\to\mathcal P(Q)\setminus\emptyset\)
Page: 47
Section: 9
Chapter: 1
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\)
Notation: \(e\)

Name: Its set of marked state
Typ: A set of leaves of \(T\)
Page: 47
Section: 9
Chapter: 1
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\)
Context: Büchi automaton
Notation: \(M\)

Name: Its set of nodes
Typ: A subset of \(\{1,\dots,2n\}\)
Page: 47
Section: 9
Chapter: 1
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\)
Notation: \(T\)

Name: The root of \(\mathcal B\)
Definition: 1
Page: 47
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\(\mathcal B=(Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\)
\(v,w\in T\)

Question: \(T\)'s cardinal is
Answer: at most \(n\)
Page: 47
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\(T\in \mathcal T_n\)

Definition: \(e(v)\setminus\bigcup_{w\in f(v)} e(w)\)
Page: 47
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in \mathcal T_n\),
\(v\in T\)
Notation: \(r(v)\)
Index: 2
Kind: Prop

Name: \(v_1\) is on the left of \(v_2\)
Definition: \(f(a)=\dots p_1\dots p_2\dots \) with \(p_i\in f(a)\) the ancestor of \(v_i\) and \(a\) the least common ancestor of \(v_1\) and \(v_2\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in \mathcal T_n\),
\(v_1,v_2\in T\) distinct
Notation: \(v_1<v_2\)

Name: The first step for computing the transition function
Definition: The four tuple \((T,f,v\mapsto\delta(e(v),a),\emptyset)\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(a\in A\)
Notation: \((T,f,e_1,M_1)\)

Definition: An injective function from \(T\) to \(\{1,\dots,2n\}\setminus T\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
Notation: \(\overline\cdot\)

Definition: \(\{\overline v\mid v\in T\}\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(\overline{T}\)

Definition: \(f(v)\overline v\) for \(v\in T\)
\(\epsilon\) for \(v\in \overline T\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(f_2(v)\)

Definition: \(e_1(v)=\delta(e(v),a)\) for \(v\in T\),
\(e_1(w)\cap F\) for \(v=\overline w\) and \(w\in T\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(e_2(v)\)

Name: The second step of computing the transition in Safra's algorithm
Definition: \((T\cup\overline T,f_2,e_2,\overline T)\) with:
\(e_2(v)\) being \(e_1(v)=\delta(e(v),a)\) and \(e_2(\overline v)\) being \(e_1(v)\cap F\) for \(v=\overline w\) and \(w\in T\) and
\(f_2(v)=f(v)\overline v\),
\(f_2(\overline v)=\epsilon\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \((T_2,f_2,e_2,M_2)\)

Name: The third step of computing the transition in Safra's algorithm
Definition: \((T\cup\overline T,f_2,e_3,\overline T)\) with:
\(e_3(v)\) being \(e_2(v)\setminus\bigcup_{w<v}e_2(w)\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \((T_2,f_2,e_3,M_2)\)

Definition: \(e_2(v)\setminus\bigcup_{w<v}e_2(w)\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
\(v\in T\)
Notation: \(e_3(v)\)

Definition: The set of \(v\in T_2\) such that \(e_3(v)\ne\emptyset\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
\(v\in T\)
Notation: \(T_4\)
Index: (4)

Definition: \(v: T_4\to T_4^*\), equals to \(f_2(v)\) with elements of \(T_2\setminus T_4\) erased
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
\(v\in T\)
Notation: \(f_4\)
Index: (4)

Name: The fourth step of computing the transition in Safra's algorithm
Definition: \(\left(T_4,f_4,{e_2}_{|T_4}, M_2\cap T_4\right)\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
\(v\in T\)
Notation: \((T_4,f_4,e_4,M_4)\)
Index: (4)

Definition: The set of \(v\in T_4\) which either belong to \(M_4\) or such that \(e_4(v)=\bigcup_{w\in f(v)}e_4(w)\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(M_5\)
Index: (5)

Definition: The elements of \(T_4\) without ancestor in \(M_5\).
I.e. The set of \(v\in T_2\) such that \(e_3(v)\ne\emptyset\), without ancestor in \(M_5\), i.e.
the set of \(v\) and \(\overline v\), for \(v\in T\), such that \(e_3(v)\ne\emptyset\), without ancestor in \(M_5\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(T_5\)
Index: (5)

Definition: \((T_5,f_5,e_5,M_5)\), with
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(\Delta(R,a)\)
Index: (5)

Definition: The restriction of \(f_4\) to elements of \(T_5\), with child of \(T_4\setminus T_5\) deleted.
I.e.The restriction of \(f_2\) to elements of \(T_5\), with child of \(T_2\setminus T_5\) deleted.
I.e. \(f_5(v)\) is \(f(v)\overline v\), without the elements not in \(T_5\), for \(v\in T\), and \(f_5(\overline v)\) is \(\epsilon\) for \(\overline v\in T_5\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(f_5\)
Index: (5)

Definition: The restriction of \((e_4)_{\mid T_5}\), i.e. \((e_3)_{\mid T_5}\), i.e.
\(e_2(v)\setminus \bigcup_{w<v}e_2(w)\) for \(v\in T_5\)
Page: 48
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(\overline\cdot:T\to\{1,\dots,2n\}\setminus T\)
Notation: \(e_5\)
Index: (5)

Name: Label
Definition: A non-empty subset of \(Q\)
Page: 47 https://swt.informatik.uni-freiburg.de/teaching/WS2015-16/AutomataTheory/Resources/Slides/safradeterminizationalgorithm-seminarslides-adityaoak.pdf
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
Name2: MacroState

Name: The set of Safra tree
Page: 47 https://swt.informatik.uni-freiburg.de/teaching/WS2015-16/AutomataTheory/Resources/Slides/safradeterminizationalgorithm-seminarslides-adityaoak.pdf
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
Notation: \(\mathcal T_n\)

Name: Its initial state in the Safra's automaton
Definition: \((\{1\},1\mapsto \epsilon,1\mapsto I,\emptyset)\) if \(I\cap F=\emptyset\),
\((\{1\},1\mapsto \epsilon,1\mapsto I,\{1\})\) if \(I\subseteq F\),
\((\{1,2\},\{1\mapsto 2,2\mapsto\epsilon\},\{1\mapsto I,2\mapsto I\cap F\},\{2\})\) otherwise
Page: 49
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,

Name: Its acceptance condition
Definition: \(\{(L_v,U_v)\mid v\in \{1,\dots,2n\}\}\), with:
\(L_v\) the set of \((T,\_,\_,\_)\in\mathcal T_n\) where \(v\not \in T\),
\(R_v\) the set of \((\_,\_,\_,M)\in\mathcal T_n\) where \(v\in M\).
Page: 49
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,

Name: Safra's automaton
Definition: \((\mathcal T_n,A,\Delta,i,\mathcal R)\) with \(i\), \(\mathcal R\) as defined for this automaton
Page: 49
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
Notation: \(\mathcal D\)
Typ: Rabin automaton

Name: Safra's automaton construction, first step
Definition: \(e_1\) is the function sending \(v\) to \(\delta(e(v),a)\), everything is unchanged
Page: 49
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(a\in A\)

Name: Safra's automaton construction, second step
Definition: Each node \(v\) of \(T\) have a new last leaf \(\overline v\), whose label is the final states of the label of \(v\)
Page: 49
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(a\in A\)

Name: Safra's automaton construction, third step
Definition: For each label \(v\), the label of elements to its left are removed. (Ensuring that \(e(v)\cap e(w)=\emptyset\) when there is no ancestor relation)
Page: 49
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(a\in A\)

Name: Safra's automaton construction, fourth step
Definition: Nodes with empty label are removed
Page: 55
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(a\in A\)

Name: Safra's automaton construction, fifth step
Definition: Considering nodes \(v\) whose label is equal to the union of the label of its descendant. Descendant are removed, the node is marked
Page: 55
Chapter: 1
Section: 9
Variables: \(Q=\{1,\dots,n\}\),
\((Q,A,E,I,F)\) a finite Büchi automaton,
\((T,f,e,M)\in\mathcal T_n\),
\(a\in A\)

Name: The class of recognisable subsets of \(A^\omega\)
Page: 56
Section: 9
Chapter: 1
Index: 4
Kind: Theo
Under: complement

Question: Example of \(\omega\) language whose complementation leads to an explosion in size of Büchi automaton.
Answer: \(A=\{0,\dots,n\}\),
\(L=\left(\bigcup_{0<i\le n}iA^*i\right)^\omega\)
Page: 56
Chapter: 1
Section: 9
Index: 5
Kind: Theo

Question: \(\mu^*\)
Answer: is the Lebesgue outer measure
Page: 59
Chapter: 13
Section: 2
Variables: \(r\in\mathbb N\),
\(\mu\) the Lebesgue measure on \(\mathbb R^r\)
Index: C
Kind: Prop

Name: A measurable envelope of \(A\)
Definition: A set \(A\subseteq E\in\Sigma\) such that \(\mu(F)=0\) for every \(F\in\Sigma\) \(F\subseteq E\setminus A\).
Page: 59
Chapter: 13
Section: 2
Variables: \((X,\Sigma,\mu)\) a measure space,
\(A\subseteq X\)
Index: D, E(a)
Kind: Def, Lem
Definition2: A set \(A\subseteq E\in\Sigma\) such that \(\mu(F\cap E)=\mu^*(F\cap A)\) for every \(F\in\Sigma\).
Name2: A measurable cover of \(A\)

Q: Equivalently:
-[...].
-[...].
A: A set \(A\subseteq E\in\Sigma\) such that \(\mu(F\cap E)=\mu^*(F\cap A)\) for every \(F\in\Sigma\); A set \(A\subseteq E\in\Sigma\) such that \(\mu(F)=0\) for every \(F\in\Sigma\) \(F\subseteq E\setminus A\)
Page: 59
Chapter: 13
Section: 2
Variables: \((X,\Sigma,\mu)\) a measure space,
\(A\subseteq X\)
Index: D, E(a)
Kind: Def, Lem
Name: A measurable envelope of \(A\)

Question: A measurable enveloppe of \(A\cap H\) is
Answer: \(E\cap H\)
Page: 59
Chapter: 13
Section: 2
Variables: \((X,\Sigma,\mu)\) a measure space,
\(A\subseteq X\),
\(A\subseteq E\in \Sigma\) a measurable enveloppe,
\(H\in\Sigma\)
Index: E(c)
Kind: Lem

Question: A measurable enveloppe of \(\bigcup A_n\) is
Answer: \(\bigcup E_n\)
Page: 59
Chapter: 13
Section: 2
Variables: \((X,\Sigma,\mu)\) a measure space,
\((A_n)\subseteq X\),
\((A_n)\subseteq (E_n)\in \Sigma\) measurable enveloppe,
Index: E(c)
Kind: Lem

Question: The measurable enveloppe of \(A\) for the Lebesgue measure is
Answer: exists
Page: 59
Chapter: 13
Section: 2
Variables: \(r\in \mathbb N\),
\(A\subseteq\mathbb R^r\)
Index: E(f)
Kind: Lem

Q: A set \(A\subseteq X\) such that, equivalently:
-[...]
-[...]
-[...]
A: \(X\) is a measurable envelope of \(A\); \(\mu^*(F\cap A)=\mu F\) for every \(F\in \Sigma\); \(\mu F=0\) for each measurable \(F\subseteq X\setminus A\)
Page: 60
Chapter: 13
Section: 2
Variables: \((X,\Sigma,\mu)\) a measure space,
Index: F
Name: A set of full outer measure
Name2: a thick set

Name: The arity of \(T\)
Definition: the maximal arity of the elements of \(N\).
Page: 010
Chapter: 1
Section: 2
Variables: \(T=(N,r,p)\) be a tree.
Context: Tree

Name: An initial path
Definition: A path whose first state belongs to \(I\).
Page: 17
Chapter: 1
Section: 4
Variables: \(\mathcal A=(Q,A,E,I,F)\) an automaton.

Name: A normalized automaton
Definition: An automaton which has only one initial state, without input and one final state, without output.
Page: 22
Chapter: 1
Section: 3
Variables: \(A\) an alphabet and
\(\mathcal A\) an automaton

Name: An ultimate period of \(u\)
Definition: An integer \(p\) such that \(\sigma^{q}(u)=\sigma^{p+q}(u)\) for some \(q\in\mathbb N\).
Page: 009
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet,
\(u\in A^\omega\).

Name: An \(\omega\)-rational set
Definition: A finite union of sets of the form \(YZ^\omega\) with \(X,Y\) rationals subsets of \(A^*\).
Page: 15, 28
Chapter: 1
Section: 3, 5
Variables: \(A\) an alphabet
Index: 2, 4
Kind: Theo
Definition2: The least set containing finite set, closed under union, \(^*\) and \(^\omega\)
Definition3: A recognisable subset of \(A^\omega\)

Definition: The only word \(v\) such that \(xv=u\).
Page: 008
Chapter: 1
Section: 2
Variables: \(A\) be an ordered alphabet, and \(u,x\in A^\infty\).
Notation: \(x^{-1}u\)
Assuming: \(x\) is a prefix of \(u\)

Name: An infinite word on the alphabet \(A\)
Definition: An infinite sequence of elements of \(A\).
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.

Question: Infinite words are denoted by
Answer: juxtaposition.
Page: 007
Chapter: 1
Section: 2
Variables: \(A\) be an alphabet.

Smaller0: every node has finite arity
Greater0: \(T\) contains an infinite path
Page: 13
Chapter: 1
Section: 2
Variables: \(T\) a tree
Kind: Prop
Hide middle: yes
Smaller1: \(T\) is infinite
Name: König's lemma

Question: The coefficients of \(T^*\) are
Answer: rational subsets of \(A^*\).
Page: 21
Chapter: 1
Section: 3
Variables: \(A\) an alphabet,
\(\mathcal A\) a finite automaton,
\(T\) its transition matrix.
Kind: Prop

Name: the Catalan number \(C_n\)
Definition: The number of planar trees with \(n\) nodes.
Page: 011
Chapter: 1
Section: 2
Variables: \(n\in\mathbb N\)
Kind: Proposition
Definition2: \[\frac{(2n-2)!}{n!(n-1)!}\].

Definition: \(\prod Q_i\)
Page: 38
Chapter: I
Section: 7.1
Variables: \(A\) an alphabet,
\(\mathcal A_i=(Q_i,A,E_i,i_i,\mathcal T_i)\) Muller automata
Notation: \(\prod\mathcal A_i\)
Definition2: \(A\)
Conjdef: The muller automaton
Definition3: \(\prod E_i\)
Definition4: \((i_i)_{i}\)
Definition5: \(\prod\mathcal T_i\)