Title: Theory / Unimportant / CS / Fundamental / Model Checking / LTL / Sort
Tags: récupéré MissingMedia

Smaller0: \(A\) is realizable
Greater0: \(A\) is realizable as a tbU\(2n(n^{2n+2}+1)\)CW
Page: 7
Section: 3
Variables: \(\Sigma_I,\Sigma_O\) input and output alphabet,
\(A\) a tbUCW
Smaller to greater: iff
Extra: check deck

Name: A game arena
Definition: \(S_i,S_O\), the set of player states, are disjoint sets
Page: 8
Section: 3
Definition2: \(s_0\in S_O\) the initial state
Conjdef: with
Definition3: \(T\subseteq (S_O\times S_I)\cup (S_i\times S_O)\) the transition relation
Extra: check deck
Denoted by: \(G\)
DefType: A tuple

Name: A play on \(G\)
Definition: A sequence \((\pi_i)_i\), finite or not, such that \(\pi_0=s_0\) and \(\pi_{i}T\pi_{i+1}\) for each \(i\) such that those terms are defined.
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena
Extra: check deck
Denoted by: \(\pi\)

Name: A winning condition
Definition: A subset of \((S_OS_I)^\omega\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena
Extra: check deck
Denoted by: \(W\)

Name: A play won by \(O\)
Definition: A play belonging to \(W\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(W\) a winning condition
Extra: check deck

Name: A play won by \(I\)
Definition: A play not belonging to \(W\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(W\) a winning condition
Extra: check deck

Name: A strategy for player \(i\)
Definition: a mapping that maps any finite play whose last state \(s\) is in \(S_i\) to a state \(s'\) such that \((s,s')\in T\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(i\in\{O,I\}\)
Extra: check deck
Denoted by: \(\lambda_i\)

Name: The outcome of \(\lambda_i\)
Definition: The set of infinite play \(\pi=(\pi_i)\) such that for all \(j\ge0\), if \(\pi_j\in S_i\) then \(\pi_{j+1}=\lambda_i(\pi_0,\dots,\pi_j)\).
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(i\in\{O,I\}\),
\(\lambda_i\) a strategy for \(i\)
Abbreviation: \(\textbf{Outcome}_G(\lambda_i)\)
Extra: check deck

Name: A safety condition
Typ: A subset of \(S_O\cup S_I\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena
Denoted by: \(\textbf{safe}\)
Extra: check deck

Name: The associated winning condition
Definition: \(\textbf{safe}^\omega\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(\textbf{safe}\) a safety condition
Extra: check deck

Definition: The pair denoting \(G\) and \(W\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(W\) a winning condition
Notation: \((S_0,S_I,s_0,T,W)\)
Extra: check deck

Definition: A state \(s\) such that \(\lambda_I\) is winning in \((S_O,S_I,s,T)\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(i\in\{O,I\}\),
\(\lambda_i\) a strategy for player \(I\)
\(W\) a winning condition
Notation: A state winning for \(\lambda_i\)
Extra: check deck

Name: A strategy for player \(i\) which wins at state \(s\)
Definition: A strategy \(\lambda_i\) which is winning in \((S_O,S_I,s,T)\)
Page: 8
Section: 3
Variables: \(G=(S_O,S_I,s_0,T)\) a game arena,
\(i\in\{O,I\}\),
\(s\in{S_O\cup S_i}\),
\(W\) a winning condition
Extra: check deck

Definition: \(A\Box(p\to q)\)
Page: 10
Section: 3.1
Variables: \(p,q\) CTL*-state
Context: CTL*
Notation: \(p\implies q\)

Definition: \(\neg p\lor q\)
Page: 10
Section: 3.1
Variables: \(p,q\) CTL*-state
Notation: \(p\to q\)

Definition: The formula \(\psi\) where each variables \(x\) are replaced by \(x'\)
Page: 10
Section: 3.1
Variables: \(V\) a set of variable,
\(\psi\) a CTL* formula over \(V\)
Context: CTL*
Notation: \(\psi'\)

Definition: The restriction of CTL* in which each temporal operator is immediately preceded by a path quantifier
Page: 10
Section: 3.1
Context: CTL*
Notation: CTL

Name: A basic CTL formula
Definition: A formula \(\mathcal{QT}\) with \(\mathcal Q\) a path quantifier, and \(\mathcal T\) a temporal operator which does not contain any additional temporal operators or path quantifiers
Page: 10
Section: 3.1
Context: CTL*

Name: An LTL formula
Definition: A CTL* formula without path quantifiers
Page: 10
Section: 3.1
Context: CTL*

Name: A temporal tester of \(\phi\)
Definition: An FDS with a distinguished Boolean variable \(x_\phi\) such that \(x_\phi=1\) at all positions in a \(T[\phi]\)-computation in which \(\phi\) is true.
Page: 11
Section: 4
Variables: \(\phi\) a path formula
Context: CTL*
Notation: \(T[\phi]\)

Definition: The output variable of \(T[\phi]\)
Page: 11
Section: 4
Variables: \(\phi\) a path formula,
\(T[\phi]\) its temporal tester
Context: CTL*
Notation: \(x_\phi\)

Definition: The variables are \(x_\circ\) and the variables of \(p\)
Page: 11
Section: 4.1
Variables: \(\circ p\) a basic path formula
Notation: \(T[\circ p]\)
Definition2: Initial state is T
Conjdef: The FDS
Definition3: Transition relation is \(x_\circ=p'\)
Definition4: \(\mathcal J=\mathcal C=\emptyset\)

Definition: The variables are \(x_{\mathcal U}\) and the variables of \(p\) and \(q\)
Page: 11
Section: 4.1
Variables: \(p\mathcal U q\) a basic path formula
Notation: \(T[p\mathcal U q]\)
Definition2: the initial condition is T
Conjdef: The FDS
Definition3: The transition condition is \(x_\mathcal U=q\lor (p\land x'_{\mathcal U})\)
Definition4: \(\mathcal J=\{\neg x_{\mathcal U}\lor q\}\)
Definition5: \(\mathcal C=\emptyset\)

Definition: The variables are \(x_{\mathcal W}\) and the variables of \(p\) and \(q\)
Page: 11
Section: 4.1
Variables: \(p\mathcal W q\) a basic path formula
Notation: \(T[p\mathcal W q]\)
Definition2: the initial condition is T
Conjdef: The FDS
Definition3: The transition condition is \(x_\mathcal W=q\lor (p\land x'_{\mathcal W})\)
Definition4: \(\mathcal J=\{ x_{\mathcal W}\lor (\neg p\land\neg q)\}\)
Definition5: \(\mathcal C=\emptyset\)

Definition: The variables are \(x_\ominus\) and the variables of \(p\)
Page: 11
Section: 4.1
Variables: \(\ominus p\) a basic path formula
Notation: \(T[\ominus p]\)
Definition2: Initial state is \(x_\ominus=F\)
Conjdef: The FDS
Definition3: Transition relation is \(x'_\ominus=p\)
Definition4: \(\mathcal J=\mathcal C=\emptyset\)

Definition: The variables are \(x_\ominus\) and the variables of \(p\)
Page: 11
Section: 4.1
Variables: \(p\) a basic path formula
Notation: \(T[\ominus p]\)
Definition2: Initial state is \(x_\ominus=T\)
Conjdef: The FDS
Definition3: Transition relation is \(x'_\ominus=p\)
Definition4: \(\mathcal J=\mathcal C=\emptyset\)

Definition: The variables are \(x_{\mathcal B}\) and the variables of \(p\) and \(q\)
Page: 12
Section: 4.1
Variables: \(p\mathcal B q\) a basic path formula
Notation: \(T[p\mathcal B q]\)
Definition2: the initial condition is \(x_{\mathcal B}=q\lor q\)
Conjdef: The FDS
Definition3: The transition condition is \(x'_{\mathcal S}=q'\lor (p'\land x'_{\mathcal B})\)
Definition4: \(\mathcal J=\emptyset\)
Definition5: \(\mathcal C=\emptyset\)

Definition: The variables are \(x_{\mathcal S}\) and the variables of \(p\) and \(q\)
Page: 11
Section: 4.1
Variables: \(p\mathcal S q\) a basic path formula
Notation: \(T[p\mathcal S q]\)
Definition2: the initial condition is \(x_{\mathcal S=q}\)
Conjdef: The FDS
Definition3: The transition condition is \(x'_\mathcal S=q'\lor (p'\land x'_{\mathcal S})\)
Definition4: \(\mathcal J=\emptyset\)
Definition5: \(\mathcal C=\emptyset\)

Definition: \(T[f(x_\phi)]\parallel|T[\phi]\)
Page: 12
Section: 4.1
Variables: \(f(\phi)\) a principally temporal path formula containing one or more occurrences of the basic path formula \(\phi\)
Notation: \(T[f]\)
Conjdef: The FDS

Name: The redux of \(\psi\)
Definition: The formula \(\psi\) where each temporal formula \(\phi\) is replaced by a variable \(x_\phi\)
Page: 13
Section: 4.1
Variables: \(f(\phi)\) a principally temporal path formula containing one or more occurrences of the basic path formula \(\phi\)
Abbreviation: \(redux(\psi)\)