Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 03 - LT proprerties
Tags: fromImplication effectNew examplesSwitchExample1 fromAlgorithm hasNotNewEffectReturnsMeaning hasSeenConjDef instructionToImplementation récupéré some_instruction

Name: deadlock
Definition: An undesirable terminal state
Page: 89
Chapter: 3
Section: 1

Name: Dining philosoher
Definition: 5 philosophers around a bowl of rice. A chopstic between each philosopher. Each can eat when they have both chopstic and think when they have known. Each must think and eat infinitely often.
Page: 90, 91
Chapter: 3
Section: 1

Definition: The set of states accessible from \(s\)
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
\(s\in S\)
Notation: \(Post^*(s)\)

Definition: The set of states from which \(s\) is accessible
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
\(s\in S\)
Notation: \(pre^*(s)\)

Definition: \(\bigcup_{s\in C}pre^*(s)\)
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
\(C\subseteq S\)
Notation: \(pre^*(C)\)

Definition: \(\bigcup_{s\in C}post^*(s)\)
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
\(C\subseteq S\)
Notation: \(post^*(C)\)

Definition: \(Post^*(I)\)
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
Notation: \(Reach(TS)\)

Name: A finite path fragment of TS
Definition: A finite state sequence \((s_i)_{0\le i\le n}\) such that \(s_i\in Post(s_{i-1})\) for all \(0<i\le n\) where \(n\ge 0\).
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
Denoted by: \(\hat \pi\)

Name: An infinite path fragment of TS
Definition: An infinite state sequence \((s_i)_{i\in\mathbb N}\) such that \(s_i\in Post(s_{i-1})\) for all \(0<i\).
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
Denoted by: \(\pi\)

Definition: \(s_0\).
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=(s_i)\) a path in \(TS\)
Notation: \(first(\pi)\)

Definition: \(s_j\).
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=(s_i)\) a path in \(TS\)
Notation: \(\pi[j]\)

Definition: \((s_i)_{i\ge j}\).
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=(s_i)\) a path in \(TS\)
Notation: \(\pi[j ...]\)

Definition: \((s_i)_{i\le j}\).
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=(s_i)\) a path in \(TS\)
Notation: \(\pi[\dots j]\)

Definition: The last element of \(\pi\) if the path is finite, \(\bot\) otherwise
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=(s_i)\) a path in \(TS\)
Notation: \(last(\pi)\)

Definition: The number of elements of \(\pi\) if it is finite, \(\infty\) otherwise
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=(s_i)\) a path in \(TS\)
Notation: \(len(\pi)\)

Name: A maximal path fragment
Definition: A finite path fragment that ends in a terminal state or an infinite path fragment
Page: 96
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
Index: 5
Kind: Def

Name: An initial path fragment
Definition: A path fragment whose itinial state belongs to \(I\)
Page: 96
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
Index: 5
Kind: Def

Definition: The set of maximal path fragments starting at \(s\)
Page: 96
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Notation: \(Paths(s)\)
Index: 5
Kind: Def

Name: A path in \(TS\)
Definition: An initial maximal path fragments in \(TS\)
Page: 96
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Index: 6
Kind: Def

Definition: The set of all paths in \(TS\)
Page: 96
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Notation: Paths(TS)
Index: 6
Kind: Def

Definition: The set of all initial finite path fragments of \(TS\)
Page: 96
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Notation: Paths_fin(TS)
Index: 6
Kind: Def
Extra: «path fragments» is in the text

Name: The trace of \(\pi\)
Definition: The sequence \(L(s_0)L(s_1)\dots\)
Page: 98
Chapter: 3
Section: 2.2
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\pi=s_0\xrightarrow{\alpha_0}s_1\xrightarrow{\alpha_1}\dots\) a path fragment
Notation: \(trace(\pi)\)
Index: 8
Kind: Def
Typ: A word over the alphabet \(2^{AP}\)

Definition: \(\{trace(\pi)\mid \pi\in\Pi\}\)
Page: 98
Chapter: 3
Section: 2.2
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(\Pi\) a set of pathes
Notation: \(trace(\Pi)\)
Index: 8
Kind: Def

Name: A (finite) trace of \(s\)
Definition: A trace of a (finite) path fragments whose first state is \(s\)
Page: 98
Chapter: 3
Section: 2.2
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Index: 8
Kind: Def

Definition: \(trace(Paths_{fin}(s))\), \(trace(Paths(s))\)
Page: 98
Chapter: 3
Section: 2.2
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Notation: \(Traces(s)\), \(Traces_{fin}(s)\)
Index: 8
Kind: Def

Definition: \(\bigcup_{s\in I}trace(s)\), \(\bigcup_{s\in I}trace_{fin}(s)\)
Page: 98
Chapter: 3
Section: 2.2
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
Notation: \(Traces(TS)\), \(Traces_{fin}(TS)\)
Index: 8
Kind: Def

Name: A LT property
Definition: A subset of \((2^{AP})^\omega\)
Page: 100
Chapter: 3
Section: 2.3
Variables: \(AP\) a set of property
Index: 10
Kind: Def

Name: \(TS\) satisfies \(P\)
Definition: \(Traces(TS)\subseteq P\)
Page: 100
Chapter: 3
Section: 2.3
Variables: \(AP\) a set of property,
\(P\) an LT property,
\(TS=(S,act,\to,I,AP, L)\) a TS,
Notation: \(TS\models P\)
Index: 11
Kind: Def

Name: \(s\) satisfies \(P\)
Definition: \(Traces(s)\subseteq P\)
Page: 100
Chapter: 3
Section: 2.3
Variables: \(AP\) a set of property,
\(P\) an LT property,
\(TS=(S,act,\to,I,AP, L)\) a TS,
\(s\in S\)
Notation: \(s\models P\)
Index: 11
Kind: Def

Definition: Restricting the trace to the elements of \(AP'\)
Page: 102
Chapter: 3
Section: 2.3
Variables: \(AP\) a set of property,
\(TS=(S,act,\to,I,AP, L)\) a TS,
\(AP'\subseteq AP\)
Example: The mutual exclusion property can be expressed considering only the critical states of each processes
Denoted by: subscript \(AP'\) on trace

Name: Starvation Freedom
Definition: The statement that a process wanting access to a critical section will eventually have access to the critical section
Page: 103
Chapter: 3
Section: 2.3
Index: 14
Kind: Ex

Name: \(TS\) is a correct implementation of \(TS'\)
Definition: \(Traces(TS)\subseteq Traces(TS')\)
Page: 104
Chapter: 3
Section: 2.4
Variables: \(TS,TS'\) TS

Smaller0: (\(TS'\models P\) implies \(TS\models P\) for each LT property \(P\))
Greater0: \(Traces(TS)\subseteq Traces(TS')\)
Page: 104
Chapter: 3
Section: 2.4
Variables: \(TS,TS'\) TS without terminal set, over the same set \(AP\)
Index: 15
Kind: Theo
Smaller to greater: iff

Name: Trace equivalent TS
Definition: TS with the same trace
Page: 104
Chapter: 3
Section: 2.4
Index: 17
Kind: Def

Smaller0: \(TS\) and \(TS'\) satisfy the same LT properties
Greater0: \(Traces(TS)=Traces(TS')\)
Page: 106
Chapter: 3
Section: 2.4
Variables: \(TS,TS'\) TS
Index: 18
Kind: Cor
Smaller to greater: iff

Name: An invariant over \(AP\)
Definition: A set of the form \(\left\{A_0 A_1\dots\in \left( 2^{AP}\right)^\omega\mid \forall j\ge0.\ A_j\models\Phi\right\}\)
Page: 107
Chapter: 3
Section: 3.1
Variables: \(AP\) a set,
Index: 20
Kind: Def
Denoted by: \(P_{inv}\)

Name: An invariant condition of \(P_{\text{inv}}\)
Definition: A formula \(\Phi\) such that \(P_{\text{inv}}=\left\{A_0 A_1\dots\in \left( 2^{AP}\right)^\omega\mid \forall j\ge0.\ A_j\models\Phi\right\}\)
Page: 107
Chapter: 3
Section: 3.1
Variables: \(AP\) a set,
\(P_{inv}\) an invariant over \(AP\)
Index: 20
Kind: Def
Name2: A state condition of \(P_{\text{inv}}\)

Definition: An LT Property \(P\) such that for all words \(\sigma\in\left(2^{AP}\right)^\omega\setminus P\), there exists a bad prefix of \(\sigma\)
Page: 112
Chapter: 3
Section: 3.1
Variables: \(AP\) a set
Index: 22
Kind: Def
Denoted by: \(P_{safe}\)

Name: A bad prefix for \(P_{safe}\)
Definition: A finite word \(\hat \sigma\in\left(2^{AP}\right)^*\) such that there exists no \(\hat\sigma\sigma'\in P\).
Page: 112
Chapter: 3
Section: 3.1
Variables: \(AP\) a set,
\(P_{safe}\subseteq \left(2^{AP}\right)^\omega\)
Index: 22
Kind: Def

Name: A minimal bad prefix for \(P_{safe}\)
Definition: A bad prefix, minimal for the prefix relation
Page: 112
Chapter: 3
Section: 3.1
Variables: \(AP\) a set,
\(P_{safe}\subseteq \left(2^{AP}\right)^\omega\)
Index: 22
Kind: Def

Name: The set of bad prefix for \(P_{safe}\)
Page: 112
Chapter: 3
Section: 3.1
Variables: \(AP\) a set,
\(P_{safe}\subseteq \left(2^{AP}\right)^\omega\)
Index: 22
Kind: Def
Abbreviation: \(BadPref(P_{safe})\)

Name: The set of minimal bad prefix for \(P_{safe}\)
Page: 112
Chapter: 3
Section: 3.1
Variables: \(AP\) a set,
\(P_{safe}\subseteq \left(2^{AP}\right)^\omega\)
Index: 22
Kind: Def
Abbreviation: \(MinBadPref(P_{safe})\)

Smaller0: \(P\) is an invariant
Greater0: \(P\) is a regular safety property
Page: 112, 159
Chapter: 3, 4
Section: 3.1, 2.1
Variables: \(AP\) a set,
\(P\subseteq \left(2^{AP}\right)^\omega\)
Index: 22
Kind: Def
Context: Infinite words

Smaller0: \(TS\models P_{safe}\)
Greater0: \(Traces_{fin}(TS)\) is disjoint from \(BadPref(P_{safe})\)
Page: 114
Variables: \(TS\) a TS,
\(P_{safe}\) a safety property
Index: 25
Kind: Lem
Smaller to greater: iff
Assuming: \(TS\) does not have terminal state

Definition: The set of finite prefixes of \(\sigma\)
Page: 114
Variables: \(\sigma\in \Sigma^{\omega}\)
Notation: \(pref(\sigma)\)
Index: 26
Kind: Def

Definition: \(\bigcup_{\sigma\in P} pref(\sigma)\)
Page: 114
Variables: \(P\subseteq \Sigma^{\omega}\)
Notation: \(pref(P)\)
Index: 26
Kind: Def

Name: The closure of \(P\)
Definition: The set of \(\sigma\in\Sigma^\omega\) such that \(pref(\sigma)\subseteq pref(P)\)
Page: 115
Variables: \(P\subseteq \Sigma^{\omega}\)
Notation: \(closure(P)\)
Index: 26
Kind: Def

Smaller0: \(closure(P)=P\)
Greater0: \(P\) is a safety property
Page: 115
Chapter: 3
Section: 3.1
Variables: \(P\subseteq \Sigma^\omega\)
Index: 27
Kind: Lem
Smaller to greater: iff

Smaller0: for any safety property \(P_{safe}\), \(TS'\models P_{safe}\) implies \(TS\models P_{safe}\)
Greater0: \(Traces_{fin}(TS)\subseteq Traces_{fin}(TS')\)
Page: 116
Chapter: 3
Section: 3.3
Variables: \(TS,TS'\) some TS
Index: 28
Kind: Theo
Smaller to greater: iff

Smaller0: (for any safety property \(P_{safe}\), \(TS'\models P_{safe}\) iff \(TS\models P_{safe}\))
Greater0: (\(Traces_{fin}(TS)= Traces_{fin}(TS')\))
Page: 117
Chapter: 3
Section: 3.3
Variables: \(TS,TS'\) some TS
Index: 29
Kind: Cor
Smaller to greater: iff

Smaller0: \(Traces(TS)\subseteq Traces(TS')\)
Greater0: \(Traces_{fin}(TS)\subseteq Traces_{fin}(TS')\)
Page: 117, 119
Chapter: 3
Section: 3.3
Variables: \(TS,TS'\) some TS
Index: 30
Kind: Theo
Smaller to greater: iff
Assuming: \(TS\) without terminal state, \(TS'\) \(AP\) image-finite

Smaller0: \(Traces_{fin}(TS)\)
Greater0: \(pref(Traces(TS))\)
Page: 117
Chapter: 3
Section: 3.3
Variables: \(TS\) some TS
Index: 30
Kind: Theo
Smaller to greater: =
Assuming: \(TS\) without terminal state

Name: An \(AP\) image-finite TS
Definition: for all \(A\subseteq AP\), the set \(\{s_0\in I\mid L(s_0)=A\}\) is finite and
Page: 119
Chapter: 3
Section: 3.3
Definition2: for all states \(s\in TS'\), and all \(A\subseteq AP\), \(\{s'\in Post(s)\mid L(s')=A\}\) is finite
Conjdef: A TS \((S,Act,\to,I,Ap,l)\) such that
Name2: An image-finite TS
Extra: Recall that the set of states may be infinite

Smaller0: \(TS\) is finite
Greater0: \(TS\) is image-finite
Page: 119
Chapter: 3
Section: 3.3
Variables: \(TS\) A TS

Smaller0: \(TS\) does not have terminal state
Greater0: \(Traces(TS)\subseteq Traces(TS')\)
Page: 117, 119, 120
Chapter: 3
Section: 3.3
Variables: \(TS,TS'\) some TS
Index: 30, 31
Kind: Theo, Rem
Smaller1: \(TS'\) is \(AP\) image-finite
Greater1: \(Traces_{fin}(TS)\subseteq Traces_{fin}(TS')\)
Connect Greater0: iff

Name: A liveness property
Definition: A property \(P\) such that \(pref(P)=(2^{AP})^*\)
Page: 121, 125
Chapter: 3
Section: 4.1
Variables: \(AP\) a set of atomic propositions
Index: 33, 39
Kind: Def, Rem
Definition2: A property which is dense
Example: Eventually
Example2: repeated eventually
Intuition: No finite word ensure rejection
Denoted by: \(P_{live}\)
Example3: starvation freedom

Name: Eventually property
Definition: each process will eventually enter its critical section;
Page: 121
Chapter: 3
Section: 4.1
Index: 33
Kind: Def

Name: Repeated Eventually property
Definition: Each process will enter its critical section infinitely often
Page: 121
Chapter: 3
Section: 4.1
Index: 33
Kind: Def

Name: Starvation freedom
Definition: each waiting process will eventually enter its critical section.
Page: 121
Chapter: 3
Section: 4.1
Index: 33
Kind: Def

Question: A safety and liveness property
Answer: is equivalent to True
Page: 123
Chapter: 3
Section: 4.1
Index: 35
Kind: Lem

Smaller0: \(closure(P)\cup closure(P')\)
Greater0: \(closure(P\cup P')\)
Page: 123
Chapter: 3
Section: 4.1
Variables: \(P,P'\subseteq (2^{AP})^\omega\)
Index: 36
Kind: Lem
Smaller to greater: =

Question: \(P\) is decomposed as
Answer: the intersection of the safety property \(closure(P)\) and of the liveness property \(\left(P\cup\left((2^{AP})^\omega\setminus closure(P)\right)\right)\)
Page: 124
Chapter: 3
Section: 4.1
Variables: \(P\subseteq (2^{AP})^\omega\)
Index: 36
Kind: Theo
Name: Decomposition theorem

Definition: \(2^{-n}\) with \(n\) the length of the longest common prefix of \(\sigma\) and \(\sigma'\)
Page: 125
Chapter: 3
Section: 4.1
Variables: \(\sigma,\sigma'\in (2^{AP})^\omega\)
Notation: \(d(\sigma,\sigma')\)
Index: 39
Kind: Rem
DefType: The distance

Smaller0: \(P\) is a safety property
Greater0: closed
Page: 125
Chapter: 3
Section: 4.1
Variables: \(P\subseteq \Sigma^{\omega}\)
Index: 39
Kind: Rem
Smaller to greater: iff
Prefix Greater: topologically, \(P\) is

Smaller0: \(closure(P)\)
Greater0: closure of \(P\)
Page: 125
Chapter: 3
Section: 4.1
Variables: \(P\subseteq \Sigma^{\omega}\)
Index: 39
Kind: Rem
Smaller to greater: =
Prefix Greater: the topological

Name: An execution fragment which is unconditional \(A\)-fair
Definition: An execution fragment \(\rho=s_0\xrightarrow{\alpha_i}s_1\xrightarrow{\alpha_1}\dots\) such that \(\exists^\infty j.\alpha_j\in A\)
Page: 129, 130
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
\(A\subseteq Act\),
Name2: Impartiality condition

Name: Strong fairness
Definition: An execution fragment \(\rho=s_0\xrightarrow{\alpha_i}s_1\xrightarrow{\alpha_1}\dots\) such that:
\(\left(\exists^\infty Act(s_j)\cap A\ne\emptyset\right)\implies{\left(\exists^\infty j.\alpha_j\in A\right)}\)
Page: 129
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
\(A\subseteq Act\),
Name2: Compassion property

Name: Weak fairness
Definition: An execution fragment \(\rho=s_0\xrightarrow{\alpha_i}s_1\xrightarrow{\alpha_1}\dots\) such that:
\(\left(\forall^\infty Act(s_j)\cap A\ne\emptyset\right)\implies{\left(\exists^\infty j.\alpha_j\in A\right)}\)
Page: 129
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
\(A\subseteq Act\),
Name2: Justice property

Smaller0: \(TS\) is strongly \(A\)-fair
Greater0: \(TS\) is weakly \(A\)-fair
Page: 131
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
\(A\subseteq Act\),
Smallest: \(TS\) is unconditionally \(A\)-fair

Name: A fairness assumption
Definition: \((\mathcal F_{ucond},\mathcal F_{strong},\mathcal F_{weak})\) with \(\mathcal F_{ucond},\mathcal F_{strong},\mathcal F_{weak}\subseteq 2^{Act}\)
Page: 133
Chapter: 3
Section: 5.1
Variables: \(ACT\) a set of action
Index: 46
Kind: Def
Denoted by: \(\mathcal F\)

Name: A \(\mathcal F\)-fair execution
Definition: An execution which is:
-unconditionally \(A\)-fair for all \(A\in\mathcal F_{ucond}\),
-strongly \(A\)-fair for all \(A\in\mathcal F_{strong}\) and
-weakly \(A\)-fair for all \(A\in\mathcal F_{weak}\)
Page: 133
Chapter: 3
Section: 5.1
Variables: \(ACT\) a set of action,
\(\mathcal F=(\mathcal F_{ucond},\mathcal F_{strong},\mathcal F_{weak})\) a fairness assumption
Index: 46
Kind: Def
Name2: A fair execution (if \(\mathcal F\) is clear)

Definition: The set of \(\mathcal F\)-fair pathes starting at \(s\)
Page: 134
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
\(\mathcal F=(\mathcal F_{ucond},\mathcal F_{strong},\mathcal F_{weak})\) a fairness assumption,
\(s\in S\)
Notation: \(FairPaths_{\mathcal F}(s)\)
Index: 46
Kind: Def

Definition: The set of \(\mathcal F\)-fair pathes starting in an initial state of \(TS\)
Page: 134
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
Let \(\mathcal F=(\mathcal F_{ucond},\mathcal F_{strong},\mathcal F_{weak})\) a fairness assumption,
Notation: \(FairPaths_{\mathcal F}(TS)\)
Index: 46
Kind: Def

Definition: \(FairPaths_{\mathcal F}(TS)\subseteq P\)
Page: 135
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
Let \(\mathcal F=(\mathcal F_{ucond},\mathcal F_{strong},\mathcal F_{weak})\) a fairness assumption,
\(P\) an LT property over \(AP\)
Notation: \(TS_{\mathcal F}P\)
Index: 48
Kind: Def

Smaller0: \(TS_{(\emptyset,\mathcal F,\emptyset)}P\)
Greater0: \(TS_{(\mathcal F,\emptyset,\emptyset)}P\)
Page: 135
Chapter: 3
Section: 5.1
Variables: \(TS=(S,Act,\to,I,Ap,L)\) a TS without terminal states,
Let \(\mathcal F\subseteq 2^{AP}\) a fairness assumption,
\(P\) an LT property over \(AP\)
Index: 48
Kind: Def
Smallest: \(TS_{(\emptyset,\emptyset,\mathcal F)}P\)

Page: 111
Implementation: Uses a DFS. For each state found, add a predecessor. For each found state, check whether \(\Phi\) holds. If it is not the case, return it and its list of ancestors.
Otherwise return true
Section: 3.1
Chapter: 3
Effect: Invariant checking, or find the path to a counter-example
Variables: \(TS\) a TS
\(\phi\) a propositional formula
Time complexity: \(O(|S|(1+|\Phi|)+\sum_{s\in S}|Post(s)|)\) with \(S\) is the set of reachable state
Index: 21
Kind: Theo