Title: Theory / Unimportant / CS / Fundamental / Model Checking / LTL / Efficient Buchi Automata from LTL Formulae
Tags: fromImplication hasSeenConjDef fromAlgorithm fromImplementation hasNotNewEffectReturnsMeaning
On every note of this deck, unless a note says otherwise:
Chapter: Efficient Büchi automata from LTL formulae

Name: Labeled generalized Büchi automaton
Definition: \(Q\) a finite set of states
Page: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Definition2: \(Q_0\subseteq Q\) the set of initial states
Conjdef: A tuple with
Definition3: \(\delta: Q\to 2^Q\),
Abbreviation: LGBA
Extra: Efficient Buchi Automata from LTL Formulae S2. P.2
Simple On-the-fly Automatic Verification of Linear Temporal Logic S3. P4
Definition4: \(\mathcal F\subseteq 2^Q\) the set of accepting sets
Definition5: \(D\) a finite set of label,
Definition6: \(\mathcal L:Q\to 2^D\) the labelling function

Name: An accepting run
Definition: A run \(\rho=(\rho_i)_{i\in\mathbb N}\) such that for each \(F\in\mathcal F\) there exists \(q_i\in F\) appearing infinitely often in \(\rho\)
Page: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Variables: \(\langle Q,Q_0,\delta,\mathcal F,D,\mathcal L\rangle\) a LGBA

Name: A run
Definition: \((\rho_i)_{i\in\mathbb N}\) with \(\rho_0\in Q_0\) and \(\rho_{i+1}\in\delta(\rho_i)\)
Page: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Variables: \(\langle Q,Q_0,\delta,\mathcal F,D,\mathcal L\rangle\) an LGBA
Denoted by: \(\rho\)

Name: An infinite word accepted by \(\mathcal A\)
Definition: \((\sigma_i)_i\) such that there exists an accepting run \((\rho_i)\) with \(\sigma_i\in \mathcal L(\rho_i)\)
Page: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Variables: \(\mathcal A=\langle Q,Q_0,\delta,\mathcal F,D,\mathcal L\rangle\)
Denoted by: \(\sigma\)

Definition: \(\langle Q,\{q\},\delta,\mathcal F,D,\mathcal L\rangle\)
Page: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Variables: \(\mathcal A=\langle Q,Q_0,\delta,\mathcal F,D,\mathcal L\rangle \) a generalized labelled Büchi automaton
Notation: \(\mathcal A^q\)

Smaller0: \(\phi\mathsf U\psi\)
Greater0: \(\psi\lor(\phi\land\mathsf X(\phi\mathsf U\psi))\)
Page: 3
Chapter: Efficient Buchi Automata from LTL Formulae
Section: 2
Variables: \(\phi,\psi\) LTL formulae
Smaller to greater: is equivalent to

Smaller0: \(\phi\mathsf R\psi\)
Greater0: \(\psi\land(\phi\lor\mathsf X(\phi\mathsf R\psi))\)
Page: 3
Chapter: Efficient Buchi Automata from LTL Formulae
Section: 2
Variables: \(\phi,\psi\) LTL formulae
Smaller to greater: is equivalent to

Name: An elementary formula in LTL
Definition: A constant
Page: 3
Chapter: Efficient Buchi Automata from LTL Formulae
Section: 2
Definition2: A formula starting with \(\mathsf X\)
Conjdef: Either
Definition3: An atomic proposition

Name: An elementary cover of \(\phi\)
Definition: A cover containing elementary formulas.
Page: 3
Chapter: Efficient Buchi Automata from LTL Formulae
Section: 2
Variables: \(\phi\) an LTL formula

Page: 3
Implementation: Applying a tableau rule to each subformula which is not below an \(\mathsf X\) and applyng a DNF normalization procedure
Section: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Effect: Computing an elementary cover of \(\phi\)
Variables: \(\phi\) an LTL formula

Name: Its fair set
Page: 2
Chapter: Efficient Buchi Automata from LTL Formulae
Variables: \(\mathcal A=\langle Q,Q_0,\delta,\mathcal F,D,\mathcal L\rangle\) a labelled generalized Biuchi automaton
Notation: \(\mathcal F\)
Name2: Its set of acceptance conditions

Question: \(\phi\land\psi\)
Answer: is equivalent to \(\phi\)
Page: 4
Variables: \(\phi,\psi\) formulas
Assuming: \(\phi\) implies \(\psi\)

Question: \(\phi\land\psi\)
Answer: is equivalent to \(\mathbf F\)
Page: 4
Variables: \(\phi,\psi\) formulas
Assuming: \(\phi\) implies \(\neg\psi\)

Question: \(\phi\mathcal U\psi\)
Answer: is equivalent to \(\psi\)
Page: 4
Variables: \(\phi,\psi\) formulas
Assuming: \(\phi\) implies \(\psi\)

Question: \(\phi\mathcal U\psi\) is equivalent to
Answer: \(\mathbf T\mathcal \psi\)
Page: 4
Variables: \(\phi,\psi\) formulas
Assuming: \(\neg\psi\) implies \(\phi\)

Question: \(\phi\mathcal U(\psi\mathcal U r)\) is equivalent to
Answer: \(\mathbf \psi\mathcal U r\)
Page: 4
Variables: \(\phi,\psi\) formulas
Assuming: \(\phi\) implies \(\psi\)

Question: \(\mathcal X\mathbf T\)
Answer: is equivalent to \(\mathbf T\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\phi\mathcal U\mathbf F\)
Answer: is equivalent to \(\mathbf F\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{GGF} \phi\)
Answer: is equivalent to \(\mathcal{GF}\phi\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{FGF} \phi\)
Answer: is equivalent to \(\mathcal{GF}\phi\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{XGF} \phi\)
Answer: is equivalent to \(\mathcal{GF}\phi\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{F}(\phi\land\mathcal{GF}\psi)\)
Answer: is equivalent to \(\mathcal{F}\phi\land(\mathcal{GF}\psi)\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{G}(\phi\lor\mathcal{GF}\psi)\)
Answer: is equivalent to \((\mathcal{G}\phi)\lor(\mathcal{GF}\psi)\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{X}(\phi\land\mathcal{GF}\psi)\) is equivalent to
Answer: \((\mathcal{X}\phi)\land(\mathcal{GF}\psi)\)
Page: 4
Variables: \(\phi,\psi\) formulas

Question: \(\mathcal{X}(\phi\lor\mathcal{GF}\psi)\)
Answer: is equivalent to \((\mathcal{X}\phi)\lor(\mathcal{GF}\psi)\)
Page: 4
Variables: \(\phi,\psi\) formulas

Smaller0: \((\phi\mathcal R\psi)\lor(\phi\mathcal Rr)\)
Greater0: \(\phi\mathcal R(\psi\lor r)\)
Page: 4
Chapter: Efficient Büchi automata from LTL formulae
Variables: \(\phi,\psi,r\) formulas
Smaller to greater: is equivalent to

Smaller0: \(\mathcal{XF}(\phi)\)
Greater0: \(\mathcal{FX}(\phi)\)
Page: 4
Chapter: Efficient Büchi automata from LTL formulae
Variables: \(\phi,\psi,r\) formulas
Smaller to greater: is equivalent to

Smaller0: \(X(\phi)\land X(\psi)\)
Greater0: \(X(\phi\land\psi)\)
Page: 4
Chapter: Efficient Büchi automata from LTL formulae
Variables: \(\phi,\psi,r\) formulas
Smaller to greater: is equivalent to

Smaller0: \(\mathcal{GF}\phi\lor\mathcal{GF}\psi\)
Greater0: \(\mathcal{GF}(\phi\lor\psi)\)
Page: 4
Chapter: Efficient Büchi automata from LTL formulae
Variables: \(\phi,\psi,r\) formulas
Smaller to greater: is equivalent to

Name: A minterm
Definition: A conjonction of litterals corresponding to distinct variables
Page: wp
Chapter: Efficient Büchi automata from LTL formulae

Name: A prime implicant of \(F\)
Definition: A \(\subseteq\)-minimal implicant
Page: wp
Chapter: Efficient Büchi automata from LTL formulae
Variables: \(X\) a set of atomic variables
\(F\) a boolean formula

Name: An implicant of \(F\)
Definition: A set of litterals whose conjunction implies \(F\)
Page: wp
Chapter: Efficient Büchi automata from LTL formulae
Variables: \(X\) a set of atomic variablesLet \(F\) a boolean formula

Definition: \(\bigwedge\{\psi\mid\phi_i=X\psi.\text{ for some }i\}\)
Page: 5
Chapter: Efficient Büchi automata from LTL formulae
Section: 4
Variables: \(\gamma=\bigwedge\phi_i\), with \(\phi_i\) elementary
Notation: \(N(\gamma)\)
Index: 2
Kind: Def

Definition: \(\psi_0\in\Phi(\psi_0)\),
Page: 6
Chapter: Efficient Büchi automata from LTL formulae
Section: 4
Variables: \(\psi_0\) an elementary cover
Notation: \(\Phi(\psi_0)\) and \(\Gamma(\psi_0)\)
Index: 2
Kind: Def
Definition2: for each \(\gamma\in\Gamma(\psi_0)\), \(N(\gamma)\in\Phi(\psi_0)\), the set of facts required to be true at next moment
Conjdef: The smallest sets that satisfy the following constraints
Definition3: for each \(\Psi\subseteq\Phi(\psi_0)\), \(P(\bigwedge\Psi)\subseteq\Gamma(\psi_0)\) with \(P\) the set of prime implicants
Intuition: one set of formulae \(\Phi(\psi_0)\), and a set of terms \(\Gamma(\psi_0)\) such that the automaton for \(\psi_0\) will be obtained from elementary covers for a subset of the formulae in \(\Phi(\psi_0)\), and will have states corresponding to a subset of \(\Gamma(\psi_0)\)

Name: Tableau rules
Definition: Rewritting rules ensuring that no Until nor Release appear before a neXt
Page: 3
Context: LTL