Title: Theory / Unimportant / CS / Fundamental / Model Checking / LTL / Improved Automata Generation for Linear Temporal Logic
Tags: fromAlgorithm fromImplementation hasNotNewEffectReturnsMeaning StateInitial autDone defToAut
On every note of this deck, unless a note says otherwise:
Chapter: Improved Automata Generation for Linear Temporal Logic

Name: An LTL interpretation
Definition: A function \(\mathbb N\to2^{\mathcal P}\)
Page: 251
Section: 2
Variables: \(\mathcal P\) a set of propositions
Kind: Def
Denoted by: \(\xi\)

Definition: \(t\mapsto\xi(t+i)\)
Page: 251
Section: 2
Variables: \(\mathcal P\) a set of propositions.
\(\xi\) an LTL interpretation
Notation: \(\xi_i\)
Kind: Def
Intuition: xi after i time unit

Name: An elementary set of formulas
Definition: A set of elementary formulas
Page: 251
Section: 2
Kind: Def

Name: A cover of \(A\)
Definition: A set \(C\) of sets \(C_i\) such that \(\left(\bigvee_{C_i\in C}\bigwedge_{\eta_i\in C_i}\eta_i\right)\iff\bigwedge_{\mu\in A}\mu\)
Page: 251
Section: 2
Variables: \(A\) a set of formulas

Page: 253
Implementation: Let the set \(\mathcal I\) of initial states be \(\textbf{Cover}(\{\psi\})\)
Let the set \(\mathcal Q\) of states be initialized to \(\textbf{Cover}(\{\psi\})\).
For each \(s\in\mathcal Q\) not yet considered in this loop:
For each \(r\in\textbf{Cover}(\{\mu\mid X\mu\in s\})\):
add \(r\) to \(\delta(s)\) and to \(\mathcal Q\)
Section: 3
Chapter: Improved Automata Generation for Linear Temporal Logic
Effect: Create automaton structure from \(\psi\)
Variables: \(\psi\) a formula in DNF
Kind: Fig

Definition: The set of positive litterals of \(s\)
Page: 253
Section: 3.2
Variables: \(\mathcal P\) a set of propositions,
Let \(s\) a conjonction of elementary formulas
Notation: \(Pos(s)\)

Definition: The set of negative litterals of \(s\)
Page: 253
Section: 3.2
Variables: \(\mathcal P\) a set of propositions,
Let \(s\) a conjonction of elementary formulas
Notation: \(Neg(s)\)

Page: 252,253
Implementation: [latex]
\textbf{Cover}($A$):\\
-\ return \textbf{cover}($A,\emptyset,\emptyset,\emptyset$)\\
\\
\textbf{cover}($ToCover$,$Current$,$Covered$,$Cover$):\\
-if $ToCover$ is empty:\\
--return $Cover \cup \{Current\}$\\
-Remove $\mu$ from $ToCover$\\
-Add $\mu$ to $Covered$ and to $Current$\\
-If $\mu$ is F or if its negation in NNF belongs to $Current$\\
-- return $Cover$\\
-If $\mu$ is Elementary\\
-- return \textbf{cover}($ToCover$,$Current\cup \{\mu\}$, $Covered$,$Cover$)\\
-If $\mu$ is $\phi\land\psi$\\
-- return \textbf{cover}($ToCover\cup \{\phi,\psi\}\setminus Current$,$Current\cup\{\mu\}$, $Covered$, $Cover$)\\
-If $\mu$ is $\phi\lor\psi$\\
-- return \textbf{cover}($ToCover\cup \{\phi\}\setminus Current$,$Current$, $Covered$,\textbf{cover}($ToCover\cup \{\psi\}\setminus Current$,$Current$,$Covered$,$Cover$))\\
-If $\mu$ is $\phi\mathcal U\psi$\\
-- return \textbf{cover}($ToCover\cup \{\psi\}\setminus Current$,$Current$, $Covered$,\textbf{cover}($ToCover\cup \{\phi,X(\phi\mathcal U\psi)\}\setminus Current$,$Current$,$Covered$,$Cover$))\\
-If $\mu$ is $\phi\mathcal V\psi$\\
-- return \textbf{cover}($ToCover\cup \{\phi,\psi\}\setminus Current$,$Current$, $Covered$,\textbf{cover}($ToCover\cup \{\psi,X(\phi\mathcal U\psi)\}\setminus Current$,$Current$,$Covered$,$Cover$))\\
[/latex]
Section: 3
Chapter: Improved Automata Generation for Linear Temporal Logic
Effect: A cover of \(\psi\) according to GPVW
Variables: \(\mathcal P\) a set of propositions,
Let \(\psi\) a LTL formula over \(\mathcal P\)

Page: 252
Variables: \(\mathcal P\) a set of propositions,
Let \(\psi\) an LTL formula over \(P\)
Section: 3
Chapter: Improved Automata Generation for Linear Temporal Logic
Transitions: The successor of \(s\) is a cover of \(\{\mu\mid X\mu\in s\}\)
States: Set of states: Sets of subformulas of \(\psi\) (restricted to the one accessible from the initial state)
Initial: Initial state: a cover of \(\{\psi\}\)
Name: The automaton recognizing \(\psi\)
Final: Accepting condition: a set \(F_{\mu\mathcal U\eta}\) containing each element either not containing \(\mu\mathcal A\eta\) or containing \(\eta\)
Locations: The generalized labelled Büchi automaton
Labels: Domain of labels: \(2^\mathcal P\)
Labeling function: Labelling function: associating to a set \(s\) the set of subsets of \(\mathcal P\) compatible avec \(s\).
Equivalently: The set of \(X\subseteq\mathcal P\), containing \(Pos(s)\) and disjoint \(Neg(s)\)