Title: Theory / Unimportant / CS / Fundamental / Model Checking / LTL / Simple on-the-fly automatic verification of linear temporal logic
Tags: fromAlgorithm fromImplementation hasNotNewEffectReturnsMeaning autDone defToAut stateInitialTransitionAlphabetLabel

Page: 4
Implementation: A string: name of the node
Incoming: Nodes with incoming edges leading to current node
New: Set of temporal properties that must hold at the current state and have not yet been processed
Old: Set of temporal properties that must hold at the current state and have already been processed
Next: Temporal properties that must hold in all states that are immediate succesors of states atisfying the properties in Old
Father: The name of the node from which the current one has been split
Section: 3
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Name: A graph node

Page: 7
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: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Effect: The states of a LGBA recognizing the language of \(\psi\)
Variables: \(\psi\) a LTL formula

Page: 6,8
Implementation: [latex]
function \textsc{f?}($\phi$):\\
-return \textsc{expand}([$Name\Leftarrow
Father\Leftarrow\textbf{new\_name()},
Incoming\Leftarrow\{\text{init}\}, New\Leftarrow\{\phi\},Old\Leftarrow\emptyset,Next\Leftarrow\emptyset$],$\emptyset$)
\\
\\
function \textsc{expand}($Node,Nodes\_Set$):\\
-if $New(Nodes)$ is empty:\\
--If there exists in $Nodes\_Set$ a set with same $Old$ and same $Next$:\\
---Add $Node$'s incoming to it\\
---return $Nodes\_Set$\\
--return \textsc{expand}([$Name\Leftarrow
Father\Leftarrow\textbf{new\_name()},
Incoming\Leftarrow\{Name(Node)\}, New\Leftarrow\{\phi\},Old\Leftarrow\emptyset,Next\Leftarrow\emptyset$],$\{Node\}\cup Nodes\_Set$)\\
-Select and Remove $\eta$ from $New(Node)$\\
-Add $\eta$ to $Old$\\
-If $\eta$ is F or if its negation in NNF belongs to $Current$\\
-- return $Nodes\_Set$\\
-If $\eta$ is atomic\\
-- return \textsc{expand}($Node,Nodes\_Set$)\\
-If $\eta$ is $\phi\land\psi$\\
-- add $\phi$ and $\psi$ to $New(Node)$
-- return \textsc{expand}($Node,Nodes\_Set$)\\
-If $\eta$ is $\phi_{1}\lor\phi_{2}$\\
-- create $Node_{i}$, a copy of $Node$, with $Node$ as father, adding $\phi_{i}$ in New if it does not belong to $Old(Node)$.\\
-If $\eta$ is $\phi\mathcal U\psi$\\
-- create $Node_{1}$, a copy of $Node$, with $Node$ as father, adding $\psi$ in New if it does not belong to $Old(Node)$.\\
-- create $Node_{2}$, a copy of $Node$, with $Node$ as father, adding $\phi$ in New if it does not belong to $Old(Node)$, and $\phi\mathcal U\psi$ to Next.
-If $\eta$ is $\phi\mathcal V\psi$\\
-- create $Node_{1}$, a copy of $Node$, with $Node$ as father, adding $\psi$ and $\phi$ in New if they does not belong to $Old(Node)$.\\
-- create $Node_{2}$, a copy of $Node$, with $Node$ as father, adding $\psi$ in New if it does not belong to $Old(Node)$, and $\phi\mathcal V\psi$ to Next.\\
- return \textsc{expand}($Node_{1}$,\textsc{expand}($Node_{2}$,$Nodes\_Set$))\\ [/latex]
Section: 3
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Effect: The graph node of the automaton accepting the language of \(\phi\)
Variables: \(\phi\) a MTL formula

Name: The transition function of its LGBA
Definition: \((p,q)\) if \(p\in Incoming(q)\)
Page: 7
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Section: 3.3
Variables: \(\mathcal P\) a set of propositions
\(\phi\) an LTL formula over \(\mathcal P\)

Question: The transition function of its LGBA
Answer: The function associating to a node \(q\) the set of subsets of \(\mathcal P\) compatible with \(Old(q)\)
Page: 7
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Section: 3.3
Variables: \(\mathcal P\) a set of propositions
\(\phi\) an LTL formula over \(\mathcal P\)

Question: The set of initial states of its LGBA
Answer: The set of states containing Init in its Incoming field
Page: 7
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Section: 3.3
Variables: \(\mathcal P\) a set of propositions
\(\phi\) an LTL formula over \(\mathcal P\)

Question: The set of accepting states of its LGBA
Answer: A set \(F_{\mu\mathcal U\psi}\) of states, for each subformula \(\mu\mathcal U\psi\).
Page: 7
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Section: 3.3
Variables: \(\mathcal P\) a set of propositions
Let \(\phi\) an LTL formula over \(\mathcal P\)

Page: 9
Variables: \(\langle Q,Q_0,\delta,\{F_1,\dots,F_{n}\},D,\mathcal L\rangle\) a LGBA,
Chapter: Simple on-the-fly automatic verification of linear temporal logic
Transitions: transitions: \(\delta'((q,i))\) being \(\delta(q)\times\{i\}\) if \(q\not\in F_i\) and \(\delta(q)\times\{i+1\}\) if \(q\in F_i\)
States: States: \(Q\times\{1,\dots,n\}\)
Initial: Initial states: \(Q_0\times\{0\}\)
Name: Its equivalent LBA
Alphabet: alphabet: \(D\)
Typ: The LBA with
Labels: labels \(\mathcal L\)

Definition: A set which contains each state \(q\) such that either \(\mu\mathcal U\psi\not\in Old(q)\), or such that \(\psi\in Old(q)\).
Page: 7
Chapter: Simple On-the-fly Automatic Verification of Linear Temporal Logic
Section: 3.3
Variables: \(\mathcal P\) a set of propositions
Let \(\phi\) an LTL formula over \(\mathcal P\)
\(\mu\mathcal U\psi\) a subformula of \(\phi\)
Notation: \(F_{\mu\mathcal U\psi}\)