Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 04 - Regular Properties
Tags: hasSeenConjDef fromImplication autSingle defToAut equivalentHand examplesSwitchExample1 fromAlgorithm fromImplementation fromMath hasNotNewEffectReturnsMeaning
On every note of this deck, unless a note says otherwise:
Chapter: 4

Name: Nondeterministic finite automaton
Definition: \(Q\) the set of states
Page: 151
Section: 1
Definition2: \(\Sigma\) the alphabet
Conjdef: A tuple
Definition3: \(\delta:Q\times\Sigma\to 2^Q\) the transition function
Abbreviation: NFA
Definition4: \(Q_0\subseteq Q\) the set of initial states
Denoted by: \(\mathcal A\)
Definition5: \(F\subseteq Q\) the set of accepting states

Name: The set of states
Page: 151
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Notation: \(Q\)

Name: The alphabet
Page: 151
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Notation: \(\Sigma\)

Name: The transition function
Page: 151
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Notation: \(\delta\)

Name: The set of initial states
Page: 151
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Context: NFA
Notation: \(Q_0\)

Name: The size of \(\mathcal A\)
Definition: \(|Q|+\sum_{q\ Q}\sum_{A\in \Sigma}|\delta(q,A)|\)
Page: 151
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Notation: \(|\mathcal A|\)

Definition: \(q'\in \delta(q,A)\)
Page: 152
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Notation: \(q\xrightarrow Aq'\)

Name: A run for \(w\)
Definition: A sequence of states \(q_0\dots q_n\) such that \(q_0\in Q_0\) and \(q_i\xrightarrow{A_{i+1} }q_{i+1}\) for all \(0\le i<n\)
Page: 153
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA,
\(w=A_1\dots,A_n\in \Sigma^*\)
Index: 3
Kind: Def

Name: An accepting run
Definition: A run whose last state belongs to \(F\)
Page: 153
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA
Index: 3
Kind: Def

Name: A word accepted by \(\mathcal A\)
Definition: A word \(w\) such that there exists an accepting run for \(w\)
Page: 154
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA,
\(A_1\dots,A_n\in \Sigma^*\)
Index: 3
Kind: Def

Name: The accepted language of \(\mathcal A\)
Definition: The set of words accepted by \(\mathcal A\).
Page: 154
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA,
Notation: \(\mathcal L(\mathcal A)\)
Index: 3
Kind: Def

Definition: A function \(f:Q\times\Sigma^*\to 2^Q\) such that \(f(q,\epsilon)=\{q\}\) and \(f(q,A_1A_2\dots A_n)=\bigcup_{q'\in\delta(q,A_1)}f(q',A_2\dots A_n)\)
Page: 155
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA,
Notation: \(\delta^*\)

Name: Non-regular language
Page: 154
Section: 1
Example: \(A^nB^n\) for \(n\ge 0\)

Name: Equivalent automata
Definition: Automata accepting the same language.
Page: 155
Section: 1
Index: 6
Kind: Def

Name: The emptiness problem
Definition: Deciding whether the language accepted by an automaton is empty
Page: 155
Section: 1

Page: 155
Implementation: Running a fixed point algorithm, starting with the set of initial states, and inserting for each state the elements which are accessibles from it.
If a final state is added to the set, the algorithm accepts otherwise it rejects
Section: 1
Chapter: 4
Effect: Deciding whether the language accepted by an automaton is empty
Time complexity: \(O(|\mathcal A|)\)

Page: 156
Variables: \(\mathcal A_i=(Q_i,\Sigma,\delta_i,Q_{0,i},F_i)\) NFAs,
Section: 1
Chapter: 4
Transitions: \(\frac{q_1\xrightarrow A_1q'_1\land q_2\xrightarrow A_2q'_2}{(q_1,q_2)\xrightarrow A(q'_1,q'_2)}\)
States: \(Q_1\times Q_2\)
Initial: \(Q_{0,1}\times Q_{0,2}\)
Name: Their product automaton
Notation: \(\mathcal A_1\otimes\mathcal A_2\)
Final: \(F_1\times F_2\)
Alphabet: \(\Sigma\)
Kind: Def
Index: 8

Smaller0: \(\mathcal L(A_1\otimes A_2)\)
Greater0: \(\mathcal L(A_1)\cap\mathcal L(A_2)\)
Page: 156
Chapter: 4
Section: 1
Variables: \(\mathcal A_i=(Q_i,\Sigma,\delta_i,Q_{0,i},F_i)\) NFAs,
Index: 8
Smaller to greater: =

Name: A deterministic Finite Automaton
Definition: \(|Q_0|\le 1\),
Page: 157
Section: 1
Definition2: \(|\delta(q,a)|\le 1\) for each \(q\in Q\), \(A\in\Sigma\)
Conjdef: An NFA \((Q,\Sigma,\delta,G_0,F)\) such that
Abbreviation: DFA

Name: A total DFA
Definition: \(|Q_0|= 1\),
Page: 157
Section: 1
Definition2: \(|\delta(q,a)|=1\) for each \(q\in Q\), \(A\in\Sigma\)
Conjdef: An NFA \((Q,\Sigma,\delta,G_0,F)\) such that

Definition: \((Q,\Sigma,\delta,q_0,Q\setminus F)\)
Page: 157
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,q_0,F)\) a DFA
Notation: \(\overline{\mathcal A}\)
DefType: The DFA

Question: \(\mathcal L(\overline{\mathcal A})\)
Answer: equals \(\Sigma^*\setminus\mathcal L(\mathcal A)\)
Page: 157
Chapter: 4
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,q_0,F)\) a DFA
Assuming: \(\mathcal A\) total

Question: Its equivalent DFA
Answer: \((\mathcal P(Q),\Sigma, (Q',a)\mapsto \{\delta(q,a)\mid q\in q'\}, Q_0, \{Q'\mid Q'\cap F\ne \emptyset\})\)
Page: 157
Chapter: 4
Section: 1
Variables: \(\mathcal A=(Q,\Sigma,\delta,Q_0,F)\) a NFA

Name: A regular safety property
Definition: A safety property whose set of bad prefix (minimal or not) is regular
Page: 159, 161
Section: 2
Index: 11, 12
Kind: Def, lem

Name: The product of \(TS\) and \(\mathcal A\)
Definition: Set of states \(S\times Q\),
Page: 165
Section: 2.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\mathcal A=(Q,2^{AP},\delta,Q_0,F)\) a NFA
Notation: \(TS\otimes\mathcal A\)
Index: 16
Kind: Def
Definition2: Actions \(Act\)
Conjdef: The TS
Definition3: \(\{(s,q)\xrightarrow{\alpha}'(t,p)\mid s\xrightarrow{\alpha}t,q\xrightarrow{L(t)}p\}\) and
Definition4: \(I'=\{\langle s_0,q\rangle\mid s_0\in I\land\exists q_0\in Q_0,q_0\xrightarrow{L(s_0)}q\}\)
Assuming: \(Q_0\) is disjoint from \(F\)
Definition5: Labels \(Q\)
Definition6: Labelling function: \(L'((s,q))=\{q\}\)

Smaller0: \(TS\models P_{safe}\)
Greater0: \(TS\otimes\mathcal A\models P_{inv(\mathcal A)}\)
Page: 165
Chapter: 4
Section: 2.2
Variables: \(AP\) a set
\(TS=(S,Act,\to,I,AP,L)\) a TS,
\(P_{safe}\) over \(AP\), regular
\(\mathcal A=(Q,2^{AP},\delta,Q_0,F)\) a NFA accepting (minimal) bad prefixes of \(P_{safe}\)
Index: 19
Kind: Theo
Smaller to greater: iff
Connect Smaller0: ,
Smallest: \(Traces_{fin}(TS)\) is disjoint from \(\mathcal L(\mathcal A)\)

Name: The invariant over \(AP'=2^Q\) in \(TS\otimes\mathcal A\)
Definition: \(\bigwedge_{q\in F}\neg q\)
Page: 166
Section: 2.2
Variables: \(AP\) a set
\(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\mathcal A=(Q,2^{AP},\delta,Q_0,F)\)
Notation: \(P_{inv(\mathcal A)}\)
Index: 16
Kind: Def

Smaller0: \(q_1,\dots,q_n\not\in F\)
Greater0: \(trace(s_0\dots s_n)\in\mathcal L(\mathcal A)\)
Page: 168
Chapter: 4
Section: 2.2
Variables: \(AP\) a set
Let \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\mathcal A=(Q,2^{AP},\delta,Q_0,F)\)
\((\langle s_i,q_{i+1}\rangle)_{0\le i\le n}\) an initial path fragment of \(TS\otimes \mathcal A\)
Index: 20
Kind: Cor
Smaller1: \(q_{n+1}\in F\)