Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 06 - CTL
Tags: fromImplication fromMath hasSeenConjDef toBinaryRelation

Question: Exemple of CTL statement not expressible in LTL
Answer: from each state accessed, the initial state is accessible
Page: 314
Chapter: 6
Section: 1

Name: A Computation Tree Logic state formulae
Definition: \(true\)
Page: 317
Chapter: 6
Section: 2.1
Variables: \(AP\) a set
Notation: CTL state formulae
Index: 1
Kind: Def
Definition2: \(a\) with \(a\in AP\)
Conjdef: Either
Definition3: \(\land\) or \(\neg\) of this kind of formula
Definition4: Closed under existential and universal quantification of the other kind of CTL formulae
Denoted by: Upper case Greek letters

Name: A Computation Tree Logic path formulae
Definition: \(\bigcirc\) followed by the other kind of formula,
Page: 317
Chapter: 6
Section: 2.1
Variables: \(AP\) a set
Index: 1
Kind: Def
Definition2: \(\Phi\bigcup\Phi\) with \(\Phi\) the other kind of formula
Conjdef: Either
Abbreviation: CTL path formulae
Denoted by: Lower case Greek letters

Name: For some path, \(\phi\) holds
Page: 317
Chapter: 6
Section: 2.1
Variables: \(\phi\) a CTL state formula
Notation: \(\exists\phi\)
Index: 1
Kind: Def

Name: For all paths, \(\phi\) holds
Page: 317
Chapter: 6
Section: 2.1
Variables: \(\phi\) a CTL state formula
Notation: \(\forall\phi\)
Index: 1
Kind: Def

Name: \(\Phi\) holds potentially
Page: 318
Chapter: 6
Section: 2.1
Variables: \(\Phi\) a CTL path formula
Notation: \(\exists\lozenge\Phi\)

Name: \(\Phi\) is inevitable
Page: 318
Chapter: 6
Section: 2.1
Variables: \(\Phi\) a CTL path formula
Notation: \(\forall\lozenge\Phi\)

Name: Potentially always \(\Phi\)
Page: 318
Chapter: 6
Section: 2.1
Variables: \(\Phi\) a CTL path formula
Notation: \(\exists\square\Phi\)

Name: Invariantly \(\Phi\)
Page: 318
Chapter: 6
Section: 2.1
Variables: \(\Phi\) a CTL path formula
Notation: \(\forall\square\Phi\)

Name: For all paths next \(\Phi\)
Page: 318
Chapter: 6
Section: 2.1
Variables: \(\Phi\) a CTL path formula
Notation: \(\forall\bigcirc \Phi\)

Definition: \(\Phi\) is infinitely often true on all paths
Page: 319
Chapter: 6
Section: 2.1
Variables: \(\Phi\) a CTL path formula
Notation: \(\forall\square\forall \lozenge \Phi\)
Index: 3
Kind: Ex

Definition: \(\pi\models\phi\) for some \(\pi\in Paths(s)\)
Page: 319
Chapter: 6
Section: 2.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(s\in S\),
\(\phi\) a CTL path formula
Notation: \(s\models \exists\phi\)
Index: 4
Kind: Def

Definition: \(\pi\models\phi\) for all \(\pi\in Paths(s)\)
Page: 319
Chapter: 6
Section: 2.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(s\in S\),
\(\phi\) a CTL path formula
Notation: \(s\models \forall\phi\)
Index: 4
Kind: Def

Definition: The set of states \(s\in S\) such that \(s\models \Phi\).
Page: 321
Chapter: 6
Section: 2.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\Phi\) a CTL state formula
Notation: \(Sat(\Phi)\)
Index: 5
Kind: Def
Notation2: \(Sat_{TS}(\Phi)\)

Name: \(TS\) satisfies \(\Phi\)
Definition: \(I\subseteq Sat(\Phi)\)
Page: 321
Chapter: 6
Section: 2.2
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS,
\(\Phi\) a CTL state formula
Notation: \(TS\models\Phi\)
Index: 5
Kind: Def
Definition2: \(\forall s_0\in I. s_0\models\Phi\)

Name: Equivalent CTL formulae
Definition: CTL - formulae which satisfy exactly the same states
Page: 329
Chapter: 6
Section: 2.3
Index: 12
Kind: Def

Name: Existential normal form
Definition: A formula without universal quantifier
Page: 332
Chapter: 6
Section: 2.4
Context: CTL
Index: 13
Kind: Def
Abbreviation: ENF

Name: CTL formula in positive normal form
Definition: A formula whose negations applies only to atoms
Page: 333
Chapter: 6
Section: 2.4
Context: CTL
Index: 15
Kind: Def
Abbreviation: PNF

Page: 334
Definition: For any transition system \(TS\) over \(AP\): \(TS\models\Phi\) iff \(TS\models\phi\)
Chapter: 6
Section: 3
Variables: \(AP\) a set of atomic propositions,
\(\Phi\) a CTL formula
\(\phi\) an LTL formula
Notation: \(\phi\equiv\Phi\)
Name: \(\Phi\) and \(\phi\) are equivalent
Kind: Def
Index: 17

Question: How to obtain an LTL formula equivalent to \(\Phi\) ?
Answer: If there exists such a formula, \(\Phi\) without its quantifier is equivalent
Page: 335
Chapter: 6
Section: 3
Variables: \(AP\) a set of atomic propositions,
\(\Phi\) a CTL formula
Index: 18
Kind: Theo

Smaller0: there exists an LTL formula equivalent to \(\Phi\)
Greater0: \(\Phi\) without quantifiers is (an LTL formula) equivalent to \(\Phi\)
Page: 335, 336
Chapter: 6
Section: 3
Variables: \(AP\) a set of atomic propositions,
\(\Phi\) a CTL formula
Index: 18, 19
Kind: Theo, Lem
Smaller to greater: iff
Counterexample: \(s_0\models\lozenge\square a\) but \(s_0\not\models\forall \lozenge\forall\square a\)

Name: LTL formula without equivalent CTL formulae
Page: 335
Chapter: 6
Section: 3
Index: 21
Kind: Theo
Example: \(\lozenge\square A\)
Example2: \(\lozenge(a\land\circ a)\)