Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 05 - LTL
Tags: fromImplication hasSeenConjDef toBinaryRelation
On every note of this deck, unless a note says otherwise:
Chapter: 5

Name: Eventually operator
Definition: \(\top\cup\)
Page: 230, 232
Section: 1, 1.1
Context: LTL
Notation: \(\lozenge\)
Name2: Finally
Notation2: \(F\)

Name: LTL's syntax
Definition: \(\phi::=\text{true}\mid a\mid \phi_1\land\phi_2\mid\neg\phi\mid\bigcirc \phi\mid\phi_1\cup\phi_2\) with \(a\in AP\)
Page: 231
Section: 1
Variables: AP a set of atomic proposition

Definition: \(\phi\cup(\psi\cup\xi) \)
Page: 231
Section: 1
Notation: \(\phi\cup\psi\cup\xi \)

Name: until
Page: 231
Section: 1
Notation: \(\cup\)

Name: next operator
Page: 231
Section: 1
Notation: \(\circ\)
Extra: eXtra
Notation2: \(X\)

Name: The length of \(\phi\)
Definition: The number of operator of \(\phi\)
Page: 235
Section: 1.1
Variables: \(\phi\) a formula
Notation: \(|\phi|\)
Kind: Rem

Definition: \(\left\{\sigma\in(2^{AP})^\omega\mid \sigma\models\phi\right\}\)
Page: 235
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\phi\) a formula
Notation: \(Words(\phi)\)
Index: 6
Kind: Def

Definition: \(A_jA_{j+1}\dots\)
Page: 235
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(j\in\mathbb N\)
Notation: \(\sigma[j\dots]\)
Index: 6
Kind: Def

Definition: always true
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(a\in AP\)
Notation: \(\sigma\models\text{true}\)
Index: 2
Kind: Fig

Definition: \(a\in A_0\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(a\in AP\)
Notation: \(\sigma\models a\)
Index: 2
Kind: Fig

Definition: \(\sigma\models\phi_1\) and \(\sigma\models\phi_2\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi_1,\phi_2\) formulas
Notation: \(\sigma\models \phi_1\land\phi_2\)
Index: 2
Kind: Fig

Definition: \(\sigma\models \neg\phi\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi\) a formula
Notation: \(\sigma\not\models\phi\)
Index: 2
Kind: Fig

Definition: \(\sigma[1\dots]\models\phi\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi\) a formulas
Notation: \(\sigma\models \bigcirc\phi\)
Index: 2
Kind: Fig

Definition: \(\exists j\in\mathbb N.\sigma[j\dots]\models\phi_2\) and \(\sigma[i\dots]\models\phi_1\) for all \(0\le i<j\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi_1,\phi_2\) formulas
Notation: \(\sigma\models\phi_1\mathcal U\phi_2\)
Index: 2
Kind: Fig

Definition: \(\exists j\in\mathbb N.\sigma[j\dots]\models\phi\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi\) a formula
Notation: \(\sigma\models \lozenge\phi\)
Index: 2
Kind: Fig

Definition: \(\forall j\in\mathbb N.\sigma[j\dots]\models\phi\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi\) a formula
Notation: \(\sigma\models \square\phi\)
Index: 2
Kind: Fig

Definition: \(\stackrel\infty\exists j\in\mathbb N.\sigma[j\dots]\models\phi\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi\) a formula
Notation: \(\sigma\models \square\lozenge\phi\)

Definition: \(\stackrel\infty\forall j\in\mathbb N.\sigma[j\dots]\models\phi\)
Page: 236
Section: 1.2
Variables: \(AP\) a set of atomic propositions,
\(\sigma=A_0A_1\dots\in (2^{AP})^\omega\),
\(\phi\) a formula
Notation: \(\sigma\models \lozenge\square\phi\)

Definition: for almost all
Page: 236
Section: 1.2
Notation: \(\stackrel\infty\forall\)

Definition: for infinitely many
Page: 236
Section: 1.2
Notation: \(\stackrel\infty\exists\)

Definition: \(trace(\pi)\models \phi\)
Page: 237
Section: 1.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS without terminal states,
\(\phi\) a LTL-formula over AP,
\(\pi\) an infinite path fragment
Notation: \(\pi\models\phi\)

Definition: For each path \(\pi\) starting at \(s\), \(\pi\models \phi\)
Page: 237
Section: 1.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS without terminal states,
\(\phi\) a LTL-formula over AP,
\(s\in S\) a state
Notation: \(s\models\phi\)
Index: 7
Kind: Def

Definition: \(Traces(TS)\subseteq Words(\phi)\)
Page: 237
Section: 1.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS without terminal states,
\(\phi\) a LTL-formula over AP,
Notation: \(TS\models\phi\)
Index: 7
Kind: Def

Smaller0: \(TS\models\neg\phi\)
Greater0: \(TS\not\models\phi\)
Page: 238
Chapter: 5
Section: 1.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS without terminal states,
\(\phi\) a LTL-formula over AP,
Index: 9
Kind: Rem

Name: weak until operator
Definition: \((\phi\mathcal U\psi)\lor\square\phi\)
Page: 252
Section: 1.5
Variables: \(\phi,\psi\) formulas
Notation: \(\phi\mathcal W\psi\)

Name: Always \(\phi\) in the past
Page: 247
Section: 1.3
Variables: \(\phi\) an LTL formulla
Notation: \(\square^{-1}\phi\)
Index: 16
Kind: Rem

Name: Sometime in the past \(\phi\)
Page: 247
Section: 1.3
Variables: \(\phi\) an LTL formulla
Notation: \(\lozenge^{-1}\phi\)
Index: 16
Kind: Rem

Name: \(\phi\) in the previous state
Page: 247
Section: 1.3
Variables: \(\phi\) an LTL formulla
Notation: \(\circ^{-1}\phi\)
Index: 16
Kind: Rem

Page: 248
Definition: Formulae whose image by \(Words\) are equal
Chapter: 5
Section: 1.4
Notation: \(\equiv\)
Name: Equivalent LTL formulae
Context: LTL

Name: Duality law for LTL
Definition: \(\neg\bigcirc\phi\equiv\bigcirc\neg\phi\),
Page: 248
Section: 1.4
Definition2: \(\neg\lozenge\phi\equiv\square\neg\phi\)
Conjdef: All of
Definition3: \(\neg\square\phi\equiv\lozenge\neg\phi\)

Name: Idempotency law for LTL
Definition: \(\lozenge\lozenge\phi\equiv\lozenge\phi\),
Page: 248
Section: 1.4
Definition2: \(\square\square\phi\equiv\square\phi\),
Conjdef: All of
Definition3: \(\phi\mathcal U(\phi\mathcal U\psi)\equiv \phi\mathcal U \psi\),
Definition4: \((\phi\mathcal U\psi)\mathcal U\psi\equiv \phi\mathcal U \psi\)

Name: expansion law for LTL
Definition: \(\lozenge\phi\equiv\phi\lor\bigcirc\lozenge\phi\)
Page: 248, 253
Section: 1.4
Definition2: \(\phi\mathcal W\psi\equiv\psi\lor(\phi\land \bigcirc(\phi\mathcal W\psi))\)
Conjdef: All of
Definition3: \(\phi\mathcal U\psi\equiv\psi\lor(\phi\land \bigcirc(\phi\mathcal U\psi))\)
Definition4: \(\square\phi\equiv\phi\land\bigcirc\square\phi\)

Name: Distributive law for LTL
Definition: \(\circ(\phi\mathcal U\psi)\equiv(\circ\phi)\mathcal U(\circ \psi)\),
\(\square(\phi\mathcal U\psi)\equiv(\square\phi)\mathcal U(\square \psi)\),
\(\lozenge(\phi\mathcal U\psi)\equiv(\lozenge\phi)\mathcal U(\lozenge \psi)\)
Page: 248
Section: 1.4

Smaller0: \(\lozenge (A\land B)\)
Greater0: \(\lozenge A\land \lozenge B\)
Page: 248
Chapter: 5
Section: 1.4
Variables: \(A,B\) atomic propositions
Counterexample: \((AB)^\omega\)

Name: A formula in positive normal form for LTL
Definition: A formula whose negations occurs only on atoms
Page: 255
Section: 1.5
Index: 20
Kind: Def
Abbreviation: PNF

Name: Weak until
Definition: \((\phi\mathcal U\psi)\lor\square\phi\),
Page: 252
Section: 1.5
Variables: \(\phi,\psi\) LTL formulae
Notation: \(\phi\mathcal W\psi\)
Name2: Unless
Intuition: \(\phi\) can stop holding when \(\psi\) holds, if it ever occurs

Question: The normal form of \(\neg(\phi\mathcal U\psi)\)
Answer: is \((\phi\land\neg\psi)\mathcal W(\neg\phi\land\neg\psi)\)
Page: 252
Chapter: 5
Section: 1.5
Variables: \(\phi,\psi\) LTL formulae

Name: Release
Page: 256
Section: 1.5
Variables: \(\phi,\psi\) LTL formulae
Context: LTL
Notation: \(\mathcal R\)

Definition: \(\neg(\neg\phi \mathcal U\neg\psi)\)
Page: 256
Section: 1.5
Variables: \(\phi,\psi\) LTL formulae
Notation: \(\phi\mathcal R\psi\)
Intuition: \(\psi\) must holds at least until \(\phi\) occurs

Name: A Weak-Until PNF
Definition: A formula in PNF with potentially some weak-until
Page: 255
Section: 1.5
Index: 20
Kind: Def

Name: A release PNF
Definition: A formula in PNF with potentially some release
Page: 257
Section: 1.5
Index: 20
Kind: Def

Question: Difference between \(\phi\mathcal R\psi\) and \(\psi\mathcal W\phi\).
Answer: In \(\phi\mathcal R\psi\), \(\psi\) must still holds when \(\phi\) first hold, while in \(\psi\mathcal W\phi\) it is possible that \(\phi\) never holds simultaneously with \(\psi\)
Page: 257
Chapter: 5
Section: 1.5
Variables: \(\phi,\psi\) LTL formulae
Extra: (not stated in the text)

Question: The size of its equivalent release PNF formulae ?
Answer: \(\mathcal O(|\phi|)\)
Page: 257
Chapter: 5
Section: 1.5
Variables: \(\phi\) LTL formulae

Name: An unconditional LTL fairness constraint
Definition: A formula of the form \(\square\lozenge\Psi\)
Page: 258
Section: 1.6
Variables: \(\phi\) LTL formulae
Index: 25
Kind: Def
Denoted by: \(ufair\)

Name: A strong LTL fairness constraint
Definition: A formula of the form \(\square\lozenge\Phi\implies\square\lozenge\Psi\)
Page: 258
Section: 1.6
Variables: \(\phi\) LTL formulae
Index: 25.2
Kind: Def
Denoted by: \(sfair\)

Name: A weak LTL fairness constraint
Definition: A formula of the form \(\lozenge\square\Phi\implies\square\lozenge\Psi\)
Page: 258
Section: 1.6
Variables: \(\phi\) LTL formulae
Index: 25.3
Kind: Def
Denoted by: \(wfair\)

Name: An LTL fairness assumption
Definition: A conjunction of LTL fairness constraints of any arbitrary type
Page: 258
Section: 1.6
Variables: \(\phi\) LTL formulae
Index: 25.3
Kind: Def

Name: \(\phi\) Weak until \(\psi\)
Definition: \((\phi\land\neg\psi)\mathcal U(\neg\phi\land\neg\psi)\)
Page: 252
Section: 1.5
Variables: \(\phi,\psi\) LTL formulae
Notation: \(\neg(\phi\mathcal W\psi)\)

Name: Linear temporal logic
Page: 230
Section: 1
Abbreviation: LTL

Name: Always
Definition: \(\neg\lozenge\neg\)
Page: 230, 232
Section: 1, 1.1
Context: LTL
Notation: \(\square\)
Name2: Globally
Abbreviation2: \(G\)