Title: Theory / Unimportant / CS / Fundamental / Automata / Infinite / Perrin Pin+10 / 08 Logic
Tags: fromMath mathToDef fromAlgorithm hasNotNewEffectReturnsMeaning mathToSee récupéré toBinaryRelation algoToList

Name: The domain of \(u\)
Definition: \(\{i\in\mathcal N\mid 0\le i\le |u|\}\).
Page: 336
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet
\(u\in A^{\infty}\).
Notation: \(\text{Dom}(u)\)

Definition: \(\mathbb N\cup\{\infty\}\)
Page: 336
Chapter: VIII
Section: 2.3
Notation: \(\mathcal N\)

Definition: The set of positions of the word \(u\) such that \(u(i)=a\)
Page: 336
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet,
\(u\in A^{\infty}\) and
\(a\in A\).
Notation: \(\mathbf a\)

Definition: \((\text{Dom}(u),(\mathbf a)_{a\in A})\)
Page: 336
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet
\(u\in A^{\infty}\)
\(a\in a\).
Notation: \(\mathcal M_u\)

Name: The spectrum of \(\phi\)
Definition: \(\{u\in A^\infty\mid u\text{ satisfies }\phi\}\)
Page: 337
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet, \(\phi\) a formula
Notation: \(S(\phi)\)

Definition: \(S(\phi)\cap A^\circ\), the spectrum of \(\phi\) restricted to elements of cardinality related to \(\circ\)
Page: 337
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet
\(\phi\) a formula
\(\circ\in\{+,*,\omega\}\)
Notation: \(S^\circ(\phi)\)

Definition: \(\{R\}\cup\{\mathbf a\mid a\in A\}\)
Page: 337
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet
\(R\in\{<,S\}\)
Notation: \(\mathcal L_R\)

Definition: The set of first order formulas of signature \(\mathcal L_R\)
Page: 337
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet
\(R\in\{<,S\}\)
Notation: \(F_1(R)\)

\(<\) is:
-definable in \(MF_2(S)\),
-not-definable in \(F_1(S)\).
Page: 338
Chapter: VIII
Section: 2.3
Index: 4
Kind: Prop

Q: \(S\) is:
-[...] in [...].
A: definable; \(F_1(<)\)
Page: 338
Chapter: VIII
Section: 2.3
Index: 4
Kind: Prop

Page: 338
Definition: For all formulas in \(F\), there exists an equivalent formula in \(G\).
Chapter: VIII
Section: 2.3
Variables: \(F,G\) two sets of formulas
Notation: \(F\le G\)
Extra: over integers

Page: 338
Definition: \(F\le G\le F\).
Chapter: VIII
Section: 2.3
Variables: \(F,G\) two sets of formulas
Notation: \(F\equiv G\)

Name: \(u\) satisfies \(\phi\) between \(i\) and \(j\)
Definition: \(u[i,j-1]\) satisfies \(\phi\).
Page: 339
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet, \(u\in A^\infty\), \(\phi(x,y)\) a formula and \(i,j\in \text{Dom}(u)\).

Smaller0: \(MF_2(\tau)\) allows to express finiteness
Greater0: \(\text{WMF}_2(\tau)\)
Page: 340
Chapter: VIII
Section: 2.3
Variables: \(\tau\) a vocabulary
Index: 7
Kind: Prop
Hide middle: yes
Greater1: \(\text{MF}_2(\tau)\)
Connect Greater0: \(\le\)

Definition: The set of monadic second order formulas of signature \(\mathcal L_R\)
Page: 337
Chapter: VIII
Section: 2.3
Variables: \(A\) an alphabet
\(R\in\{<,S\}\)
Notation: \(MF_2(R)\)

Page: 341
Implementation: Existential quantification of \(X_q\) for each \(q\in Q\), such that, the conjonction of the following propreties hold:
-\(X_q\) partition the universe.
-\(\bigvee_{q\in I}X_q(0)\),
-\(\forall x.\exists x+1. S(x,x+)\implies \bigvee_{(q,a,q')\in E}X_q(x)\land \mathrm a(x)\land X_{q+1}(y)\)
-the acceptance condition being the disjonction of:
--\(\exists x\land\neg exists x+1. S(x,y+1)\land\bigvee_{q\in F}X_q(x)\)
--\(\exists^\infty x. \bigvee_{q\in F}X_q(x)\)
Chapter: VIII
Effect: An \(MF_2(<)\) formula defining \(L^{\infty}(\mathcal A)\)
Variables: \(A\) an alphabet,
\(\mathcal A=(Q,A,E,I,F)\) an automaton

Page: 343
Implementation: Create a Büchi automaton recognizing the marked words. Remove the marks from the alphabet.
Section: 3
Chapter: VIII
Effect: A Büchi automaton recognizing \(L(\phi)\)
Variables: \(A\) an alphabet,
\(\phi\in ML_2(A)\)

Definition: \(A\times\{0,1\}^p\times\{0,1\}^q\)
Page: 342
Chapter: VIII
Section: 3
Variables: \(A\) an alphabet,
Notation: \(B_{p,q}\)

Name: The set of marked words
Definition: The set of words of \(B_{p,q}^\omega\) where the \(1+i\)-th component, for \(1\le i\le p\), is 1 exactly once
Page: 342
Chapter: VIII
Section: 3
Variables: \(A\) an alphabet
Notation: \(K_{p,q}\)
Index: ,3
Kind: , Prop
Typ: Star-free

Page: 342-344
Implementation: The conjunction of:
-the definition of \(K_{p,q}\), with \(p\) the number of first-order free variable and \(q\) the number of second order free variables
-The formula obtained by induction on \(\phi\), with:
--atomic cases: straightforward
--Boolean case: straightforward
--Existential case: projection
Section: 3
Chapter: VIII
Effect: A rational expression defining \(L(\phi)\)
Variables: \(A\) an alphabet,
\(\phi\in ML_2(A)\)

Page: 345
Implementation: Transform \(\phi\) into an equivalent automaton, decide whether it accepts a word.
Section: 3
Chapter: VIII
Effect: Deciding whether \(\phi\) is satisfiable
Variables: \(A\) an alphabet,
\(\phi\in ML_2\)

Name: \(w\) satisfies \(\phi\)
Definition: \(b_0\) satisfies \(\phi[\nu]\)
Page: 280
Chapter: XVII
Section: 3
Variables: \(A\) an alphabet,
\(\phi(x_1,\dots,x_p,X_1,\dots,X_q)\) a MSO formula
\(w=(b_0,\dots,b_{p+q})\in K_{p,q}\),
Kind: Prop

Definition: \(S_{p,q}(\phi)\)
Page: 280
Chapter: XVII
Section: 3
Variables: \(A\) an alphabet,
\(\phi(x_1,\dots,x_p,X_1,\dots,X_q)\) a MSO formula
Notation: \(L(\phi)\)
Kind: Prop
Assuming: \(p=q=0\)