Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{ / 02 - Concurrent Systems;
Tags: fromMath mathToDef hasSeenConjDef FromInstruction algoToProg computer_to_instruction hasNotNewEffectReturnsMeaning some_instruction mathToSee fromImplication omitted toBinaryFunction

Question: Any verification using model-based techniques is only as good as
Answer: the model of the system.
Page: 8
Chapter: 1

Name: Property specification
Definition: Stating what the system should do.
Page: 9
Chapter: 1

Name: Model description
Definition: Addressing how the system behaves.
Page: 9
Chapter: 1
Context: concurrent system

Smaller0: a state is encountered that violates the property under consideration
Greater0: a counterexample that indicates how the model could reach the undesired state
Page: 9
Chapter: 1
Hide middle: yes
Prefix Greater: the model checker provides

Name: Model checking
Definition: An automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) that model.
Page: 11
Chapter: 1
Section: 2

Name: The phases of model checking
Definition: Modeling phase
Page: 11
Chapter: 1
Section: 2
Definition2: Running phase
Conjdef: In this order
Definition3: Analysis phase.

Q: –[...];
–[...];
–[...].
A: Model the system under consideration using the model description language of the model checker at hand; perform some simulations: a first sanity check and quick assessment of the model; Formalize the property to be checked using the property specification language
Page: 11
Chapter: 1
Section: 2
Name: Modeling phase

Name: Running phase
Definition: Run the model checker to check the validity of the property in the system model.
Page: 11
Chapter: 1
Section: 2

Q: – property satisfied? → [...];
– property violated? →
[...].
– out of memory? → [...].
A: check next property (if any); 1. analyze generated counterexample by simulation;
2. refine the model, design, or property;
3. repeat the entire procedure; try to reduce the model and try again
Page: 11
Chapter: 1
Section: 2
Name: Analysis phase

Name: A model of \(S\)
Definition: A description of the behavior of systems in an accurate and unambiguous way.
Page: 12
Chapter: 1
Section: 2
Variables: \(S\) a system

Name: Verification in model checking
Definition: Check that the design satisfies the requirements that have been identified.
Page: 13
Chapter: 1
Section: 2

Name: Validation in model checking
Definition: Check that the formal model is consistent with the informal conception of the design.
Page: 13
Chapter: 1
Section: 2

Name: Modelling error
Definition: The model does not reflect the design of the system.
Page: 13
Chapter: 1
Section: 2

Name: Property error
Definition: The property does not reflect the informal requirement that had to be validated.
Page: 13
Chapter: 1
Section: 2

Question: Which kind of application is concerned by model-checking ?
Answer: Control-intensive, as opposed to data-intensive.
Page: 15
Chapter: 1
Section: 2.2

Name: Action names
Definition: A description of a communication mechanisms between processes.
Page: 20
Chapter: 2
Section: 1
Notation: Letters at the beginning of the Greek alphabet

Name: Atomic propositions
Definition: Expression of simple known facts about the states of the system under consideration.
Page: 20
Chapter: 2
Section: 1
Context: Model checking
Denoted by: Letters from the beginning of the latin alphabet

Name: A transition system
Definition: \((S,Act,\to,I,AP,L)\) with:
-\(S\) a set of states,
-\(Act\) a set of actions,
-\(\to\subseteq S\times Act\times S\),
-\(I\subseteq S\) a set of initial states,
-\(AP\) a set of atomic propositions and
-\(L:S\to 2^{AP}\) a labeling function.
Page: 20
Chapter: 2
Section: 1
Kind: Def
Abbreviation: TS

Name: A finite transition system
Definition: A TS \((S,Act,\to,I,AP,L)\) with \(S\), \(Act\) and \(AP\) finite.
Page: 20
Chapter: 2
Section: 1

Definition: \((s,\alpha,s')\in\to\).
Page: 20
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s,s'\in S\),
\(\alpha\in Act\)
Notation: \(s\xrightarrow{\alpha}s'\)

Name: The set of \(\alpha\)-successors of \(s\)
Definition: \(\left\{s'\in S\mid s\xrightarrow{\alpha}{s'}\right\}\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s\in S\),
\(\alpha\in Act\)
Notation: \(Post(s,\alpha)\)
Index: 3
Kind: Def

Name: The set of \(\alpha\)-predecessors of \(s\)
Definition: \(\left\{s'\in S\mid s'\xrightarrow{\alpha}{s}\right\}\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s\in S\),
\(\alpha\in Act\)
Notation: \(Pre(s,\alpha)\)
Index: 3
Kind: Def

Definition: \(\bigcup_{\alpha\in Act}Pre(s,\alpha)\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s\in S\)
Notation: \(Pre(s)\)
Index: 3
Kind: Def

Name: A direct \(\alpha\)-successor of \(s\)
Definition: An element of \(Post(s,\alpha)\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s\in S\),
\(\alpha\in Act\)
Index: 3
Kind: Def

Name: A direct successor of \(s\)
Definition: An element of \(Post(s)\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s\in S\)
Index: 3
Kind: Def

Definition: \(\bigcup_{s\in C}Post(s,\alpha)\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(C\subseteq S\),
\(\alpha\in Act\)
Notation: \(Post(C,\alpha)\)
Index: 3
Kind: Def

Definition: \(\bigcup_{s\in C}Pre(s)\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(C\subseteq S\),
\(\alpha\in Act\)
Notation: \(Pre(C)\)
Index: 3
Kind: Def

Definition: A state \(s\) such that \(Post(s)=\emptyset\).
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Notation: A terminal state
Index: 4
Kind: Def

Name: An action-deterministic TS
Definition: \(|I|\le 1\)
Page: 24
Chapter: 2
Section: 1
Index: 5
Kind: Def
Definition2: \(|Post(s,\alpha)|\le 1\) for all states \(s\) and actions \(\alpha\).
Conjdef: A TS \((S,Act,\to,I,AP,L)\) such that

Name: An AP-deterministic TS
Definition: \(|I|\le 1\)
Page: 24
Chapter: 2
Section: 1
Index: 5
Kind: Def
Definition2: \(|\{s'\in Post(s) \mid L(s')=A\}|\le 1\) for all states \(s\) and \(A\subseteq AP\).
Conjdef: A TS \((S,Act,\to,I,AP,L)\) such that
Extra: Initially: \(|Post(s)\cap\{s'\in S\mid L(s')=A\}|\) ?

Name: A finite execution fragment
Definition: An alternating sequences of states and actions, ending with a state:
\(s_0\alpha_1\dots\alpha _n s_n\) such that \(s_i\xrightarrow{\alpha_{i+1} }s_{i+1}\) for all \(0\le i<n\).
Page: 24
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 6
Kind: Def

Name: The length of the execution fragment
Definition: \(n\).
Page: 24
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
\[s_0\alpha_1\dots\alpha _n s_n\] a finite execution fragment
Index: 6
Kind: Def

Name: An execution fragment
Definition: A finite or infinite execution fragment.
Page: 25
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 6
Kind: Def

Name: A maximal execution fragment
Definition: An execution fragment which can not be prolonged.
Page: 25
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 6
Kind: Def

Name: An initial execution fragment
Definition: An execution fragment which starts in \(I\).
Page: 25
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 7
Kind: Def

Name: An execution of the TS
Definition: An initial, maximal execution fragment.
Page: 25
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 9
Kind: Def

Name: A reachable state
Definition: A state \(s\) such that there exists an initial, finite execution fragment ending in \(s\).
Page: 26
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 10
Kind: Def

Name: A sequential hardware circuit
Definition: \((n,k,m,c_{0,1},\dots,c_{0,k},\delta_{r_1}\dots,\delta_{r_k},\lambda_{y_1},\dots,\lambda_{y_m})\) with \(n\) the number of inputs, \(k\) the number of registers \(m\) the number of output bits, and the \(\delta_{r_i}\) and \(\lambda_{y_i}\) being boolean functions whose inputs belongs to \(\{x_i\mid 1\le i\le n\}\cup\{r_i\mid 1\le i\le k\}\).
Page: 28
Chapter: 2
Section: 1.2

Name: Its evaluation
Definition: Given an infinite sequence \((a_{i,1},\dots,a_{i,n})_{i\in\mathbb N}\), let \(c_{i,j}\) (resp, \(y_{i,j}\)) be \(f_j\) (resp, \(f'_j\)), with \(r_{j'}\) interpreted as \(c_{i-1,j'}\) and \(x_{j'}\) as \(a_{i,j}\).
Page: 28
Chapter: 2
Section: 1.2
Variables: \(S=(n,k,m,c_{0,1},\dots,c_{0,k},\delta_{r_1}\dots,\delta_{r_k},\lambda_{y_1},\dots,\lambda_{y_m})\) a sequential hardware circuit

Name: \(Eval(S)\)
Definition: The set of evaluations of those variables.
Page: 28
Chapter: 2
Section: 1.2
Variables: \(S\) a set of variables

Name: The set of Boolean conditions over \(S\)
Page: 30
Chapter: 2
Section: 1.2
Variables: \(S\) a set of typed variables
Notation: \(Cond(S)\)

Name: The domain of \(x\)
Definition: The set of possible values for \(x\)
Page: 30
Chapter: 2
Section: 1.2
Variables: \(x\) a variable
Abbreviation: \(dom(x)\)

Name: A program graph over \(S\)
Definition: \((Loc,Act,Effect,\hookrightarrow,Loc_0,g_0)\) with:
-\(Loc\) a set of locations,
-\(Act\) a set of actions,
-\(\hookrightarrow\subseteq Loc\times Cond(Var)\times Act\times Loc\) the conditional transition relation,
-\(Loc_0\subseteq Loc\) a set of initial locations,
-\(g_0\in Cond(Var)\) a set of initial condition.
Page: 32
Chapter: 2
Section: 1.2
Variables: \(S\) a set of typed variables

Name: A location
Definition: A node of this graph
Page: 32
Chapter: 2
Section: 1.2
Variables: \(S\) a set of typed variables,
\(P\) a program graph over \(S\)

Definition: \((l,g,\alpha,l')\in\hookrightarrow\)
Page: 33
Chapter: 2
Section: 1.2
Notation: [$]l\xhookrightarrow{g:\alpha} l'[/$]

Q: \(\frac{ [...] }{ [...] }\).
A: premise; conclusion
Page: 34
Chapter: 2
Section: 1.2
Name: Inference rule
Name2: rule

Name: Their interleaving
Definition: \(S_1\times S_2\)
Page: 38
Chapter: 2
Section: 2.1
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) transition systems
Notation: \(TS_1|||TS_2\)
Index: 18
Kind: Def
Definition2: \(Act_1\cup Act_2\)
Conjdef: The TS
Definition3: \(\to\) contains \(\{(s_1,s_2),(s_1',s_2)\mid s_1\to_1 s'_1\}\) and \(\{(s_1,s_2),(s_1,s'_2)\mid s_2\to_2 s'_2\}\)
Definition4: \(I_1\times I_2\)
Definition5: \(AP_1\cup AP_2\)
Definition6: \(L(s_1,s_2)=L_1(s_1)\cap L_2(s_2)\)

Name: The shared-variable program of \(PG_1\) and \(PG_2\)
Definition: \(Loc_1\times Loc_2\)
Page: 40
Chapter: 2
Section: 2.2
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow_i{},Loc_{0,i},g_{0,i})\) program graphs
Notation: \(PG_1|||PG_2\)
Index: 21
Kind: Def
Definition2: \(Act_1\uplus Act_2\)
Conjdef: The PG
Definition3: \(Effect(\alpha,\eta)=Effect_i(\alpha,\eta)\) for \(\alpha\in Act_i\)
Definition4: [$](l_i,l_{3-i})\xhookrightarrow{g:\alpha}(l'_i,l_{3-i})[/$] for [$] l_i\xhookrightarrow{g:\alpha}_i l'_i[/$]
Definition5: \(Loc_{0,1}\times Loc_{0,2}\)
Definition6: \(g_{0,1}\land g_{0,2}\)

Name: Their shared variables
Definition: \(\bigcap_i Var_i\)
Page: 40
Chapter: 2
Section: 2.2
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow,Loc_{0,i},g_{0,i})\) program graphs over \(Var_i\)
Index: 21
Kind: Def

Name: The local variables of \(PG_i\)
Definition: \(Var_i\setminus\bigcup_{j\ne i}Var_j\)
Page: 40
Chapter: 2
Section: 2.2
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow,Loc_{0,i},g_{0,i})\) program graphs over \(Var_i\)
Index: 21
Kind: Def

Name: A critical action
Definition: An action which access shared variables
Page: 42
Chapter: 2
Section: 2.2
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow,Loc_{0,i},g_{0,i})\) program graphs over \(Var_i\)

Name: The three kinds of non-determinism of \(TS(PG_1|||PG_2)\)
Definition: non-determinism in one of the \(PG_i\)
Page: 42
Chapter: 2
Section: 2.2
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow,Loc_{0,i},g_{0,i})\) program graphs over \(Var_i\)
Definition2: interleaving of noncritical actions of \(PG_1\) and \(PG _2\)
Conjdef: All
Definition3: the resolution of a contention between critical actions of PG 1 and PG 2 (concurrency).

Name: Atomic operations
Definition: A sequence of actions which must not be interlocked with other concurrent processes
Page: 42, 43
Chapter: 2
Section: 2.2
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow,Loc_{0,i},g_{0,i})\)
Index: 23
Kind: Rem
Denoted by: Being on the same arrow of the graph representations, or between brackets

Definition: \(\Pi S_i\)
Page: 48
Chapter: 2
Section: 2.3
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) transition systems for \(1\le i\le n\)
\(H_{i,j}\subseteq Act_i\cap Act_j\) for \(i<j\)
\(\tau\not\in H\)
Notation: \(TS_1||\dots||TS_n\)
Index: 26
Kind: Def
Definition2: \(\bigcup _i Act_i\)
Conjdef: The TS
Definition3: \((s_1,\dots, s_{i},\dots,s_n )\xrightarrow{\alpha}(s_1,\dots,s'_i,\dots,s_n)\) for \(s_i\xrightarrow\alpha s'_i,\alpha\not\in H\) and \((s_1,\dots,s_i,\dots,s_j,\dots,s_{n})\xrightarrow{\alpha}(s_1,\dots,s'_i,\dots,s'_j,\dots s_{n})\) for \(s_i\xrightarrow\alpha s'_i, s_j\xrightarrow\alpha s'_j, \alpha\in H_{i,j}\)
Definition4: \(\bigcup I_i,\bigcup I_i\)
Definition5: \(\bigcup AP_i\bigcup AP_i\)
Definition6: \(L(\vec s)\mapsto \bigcup {L_i(s_i)}\)

Smaller0: \(H=\emptyset\)
Greater0: \(TS_1||_HTS_2 = TS_1|||_HTS_2\)
Page: 49
Chapter: 2
Section: 2.3
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) transition systems,
\(H\subseteq Act_1\cap Act_2\)
Index: 27
Kind: Rem

Page: 48
Section: 2.3
Notation: \(TS_1\parallel_H TS_2\)
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) transition systems,
\(H\subseteq Act_1\cap Act_2\)
\(\tau\not\in H\)
Chapter: 2
Definition: \(S_1\times S_2\)
Kind: Def
Index: 26
Associative: Associative, for \(H\) fixed
Definition2: \(Act_1\cup Act_2\)
ConjDef: A TS
Definition3: -\((s_i,s_{3-i})\xrightarrow{\alpha}(s'_i,s_{3-i})\) for \(s_i\xrightarrow\alpha s'_i,\alpha\not\in H\),
-\((s_1,s_{2})\xrightarrow{\alpha}(s'_1,s_{2})\) for \(s_i\xrightarrow\alpha s'_i, \alpha\in H\)
Definition4: \(I_1\cup I_2\)
Definition5: \(AP_1\cup AP_2\)

Name: Mutual Exclusion by Means of an Arbiter
Definition: \((TS_1|||TS_2)||A\) where \(A\) mimic the \(TS_i\)'s, ensuring by its actions that no two of them are in critical state together
Page: 50
Chapter: 2
Section: 2.3
Variables: \(TS_i=(\{crit_i,noncrit_i\},\{request_i,rel_i\},\to_i,I_i,AP_i,L_i)\)
Index: 28
Kind: Ex

Name: A program graph over \((Var,Chan)\)
Definition: A tuple \((Loc,Act,Effect,\hookrightarrow, Loc_0,g_0)\) as in program graph, with \(\hookrightarrow\subseteq Loc\times Cond(Var)\times (Act\cup Comm)\times Loc\)
Page: 55
Chapter: 2
Section: 2.4
Variables: \(Var\) a set of variable,
\(Chan\) a set of channels
Index: 31
Kind: Def
Extra: parenthèse implicite ?

Name: A channel system over \((Var,Chan)\)
Definition: A sequence of program graphs \(PG_i\) over \((Var_i,Chan)\), with \(Var=\bigcup_i Var_i\)
Page: 55
Chapter: 2
Section: 2.4
Variables: \(Var\) a set of variable,
\(Chan\) a set of channels
Notation: \([PG_1\mid \dots\mid PG_n]\)
Index: 31
Kind: Def
Denoted by: \(CS\)

Name: A channel
Definition: A named element, with a capacity in \(\mathbb N\cup\{\infty\}\) and a domain
Page: 55
Chapter: 2
Section: 2.4
Index: 31
Kind: Def

Name: The domain of the channel \(c\)
Definition: The set of elements which can be transmitted over the channel
Page: 55
Chapter: 2
Section: 2.4
Variables: \(c\) a channel
Notation: \(dom(c)\)

Name: The capacity of \(c\)
Definition: The number of elements which can be stocked in the channel
Page: 55
Chapter: 2
Section: 2.4
Variables: \(c\) a channel
Abbreviation: \(cap(c)\)

Name: Alternating bit protocol
Definition: Emmitter sends a message with a bit. The receiver sends the bit back.
If Emmiter does not receive the bit back, after some time, it sends the message again.
When he receives the bit, it sends the following message with the negatiof of the bit.
Page: 57
Chapter: 2
Section: 2.4
Abbreviation: ABP

Name: The transition system of \(CS\)
Definition: \(S=(\Pi_i Loc_i)\times Eval(Var)\times Eval(Chan)\),
-\(Act=\biguplus Act_i\uplus \{\tau\}\),
Page: 60
Chapter: 2
Section: 2.4
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow_i,Loc_{0,i},g_{0,i})\)Let \(CS=[PG_1\mid\dots\mid PG_n]\) a channel system over \((Chan,Var)\)
Notation: \(TS(CS)\)
Definition2: \(\to\) contains interleaving, asynchronous message passing and synchronous message passing,
Conjdef: The TS
Definition3: \(I=\left\{\langle\ell_1,\dots,\ell_n,\eta,\xi_0\rangle\mid \forall i. (\ell_i\in Loc_{0,i}\land \eta\models g_{0,i}))\right\}\),
Definition4: \(AP=\biguplus Loc_i\uplus Cond(Var)\),
Definition5: \(L(\langle\ell_1,\dots,\ell_n,\eta,\xi_0\rangle)=\{\ell_i\mid i\}\cup\{g\in Cond(Var)\mid \eta\models g\}\)

Name: An interleaving transition
Definition: \(\langle\ell_1,\dots,\ell_n,\eta,\xi\rangle\xrightarrow\alpha\langle\ell_1,\dots,\ell_i',\dots,\ell_n,Effect(\alpha,\eta),\xi\rangle\) for [$]\ell_i\xhookrightarrow{g:\alpha}\ell'_i[/$] and \(\eta\models g\)
Page: 61
Chapter: 2
Section: 2.4
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow_i,Loc_{0,i},g_{0,i})\)Let \(CS=[PG_1\mid\dots\mid PG_n]\) a channel system over \((Chan,Var)\)

Name: Asynchronous message receiving for \(c\)
Definition: [$]\ell_i\xhookrightarrow{g:c?x}\ell'_i[/$]
Page: 61
Chapter: 2
Section: 2.4
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow_i,Loc_{0,i},g_{0,i})\)Let \(CS=[PG_1\mid\dots\mid PG_n]\) a channel system over \((Chan,Var)\),
\(c\in Chan\)
Definition2: \(\eta\models g\),
Conjdef: \(\langle\ell_1,\dots,\ell_n,\eta,\xi_0\rangle\xrightarrow\tau\langle\ell_1,\dots,\ell_i',\dots,\ell_n,\eta[x:=v_1],\xi[c:=v_2\dots v_k]\rangle\) for
Definition3: \(\xi(c)=v_1\dots v_k\) non empty
Assuming: \(cap(c)>0\)

Name: Asynchronous message sending for \(c\)
Definition: [$]\ell_i\xhookrightarrow{g:c!v}\ell'_i[/$],
Page: 61
Chapter: 2
Section: 2.4
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow_i,Loc_{0,i},g_{0,i})\)
\(CS=[PG_1\mid\dots\mid PG_n]\) a channel system over \((Chan,Var)\),
\(c\in Chan\)
Definition2: \(\xi(c)=v_1\dots v_k\) of length less than \(cap(c)\)
Conjdef: \(\langle\ell_1,\dots,\ell_n,\eta,\xi_0\rangle\xrightarrow\tau\langle\ell_1,\dots,\ell_i',\dots,\ell_n,\eta,\xi[c:=v_1\dots v_k v]\rangle\) for
Assuming: \(cap(c)>0\)

Name: Synchronous message passing for \(c\)
Definition: \(\langle\ell_1,\dots,\ell_n,\eta,\xi_0\rangle\xrightarrow\tau\langle\ell_1,\dots,\ell_i',\dots,\ell_j',\dots,\ell_n,\eta[x:=v],\xi\rangle\) for:
-[$]\ell_i\xhookrightarrow{g:c?v}\ell'_i[/$],
-[$]\ell_j\xhookrightarrow{g:c!v}\ell'_j[/$],
-\(\eta\models g_1\land g_2\).
Page: 61
Chapter: 2
Section: 2.4
Variables: \(PG_i=(Loc_i,Act_i,Effect_i,\hookrightarrow_i,Loc_{0,i},g_{0,i})\)Let \(CS=[PG_1\mid\dots\mid PG_n]\) a channel system over \((Chan,Var)\),
\(c\in Chan\)
Assuming: \(cap(c)=0\)

Name: A formal semantic
Definition: Rendering the intuitive meaning of the language commands in an unambiguous manner.
Page: 63
Chapter: 2
Section: 2.4

Name: Process Metalanguage
Page: 63
Chapter: 2
Section: 2.4
Abbreviation: Promela

Name: A Promela program
Definition: A finite number of processes to be executed concurently
Page: 63
Chapter: 2
Section: 2.5
Denoted by: \(\overline{\mathcal P}\)

Name: A process can read a value over \(c\)
Definition: the capacity of \(c\) is 0 and another process can send a value.
Page: 56
Chapter: 2
Section: 2.4
Variables: \(c\) a channel
Definition2: the capacity of \(c\) is >0 and the channel is not empty
Conjdef: Either

Name: A process can transmits a value over \(c\)
Definition: Either its capacity is 0 and another process can receive a value.
Or capacity is >0 and the channel is not yet full
Page: 56
Chapter: 2
Section: 2.4
Variables: \(c\) a channel
Context: concurrent system

Question: Substatements of skip
Answer: skip and exit
Page: 69
Chapter: 2
Section: 2.5
Index: 38
Kind: Prop

Question: Substatements of x:=expr
Answer: x:=expr and exit
Page: 69
Chapter: 2
Section: 2.5
Index: 38
Kind: Prop

Question: Substatements of c?x
Answer: c?x and exit
Page: 69
Chapter: 2
Section: 2.5
Index: 38
Kind: Prop

Question: Substatements of c!expr
Answer: c!expr and exit
Page: 69
Chapter: 2
Section: 2.5
Index: 38
Kind: Prop

Question: Substatements of stmt1;stmt2
Answer: stmt';stmt2 with stmt' being a substatement of stmt1 distinct from exit, and
the substatements of stmt2
Page: 69
Chapter: 2
Section: 2.5
Index: 38
Kind: Prop

Question: Substatements of cond_cmd
Answer: The substatements of stmti and
if
::g1=>stmt1
...
::gn=>stmtn
fi
Page: 69
Chapter: 2
Section: 2.5
Variables: cond_cmd be
if
::g1=>stmt1
...
::gn=>stmtn
fi
Index: 38
Kind: Prop

Question: Substatements of
do
::g1=>stmt1
...
::gn=>stmtn
od
abbreviated as loop
Answer: stmt';loop with stmt' a substatement of some stmti
exit
loop
Page: 69
Chapter: 2
Section: 2.5
Index: 38
Kind: Prop

Name: Substatements of stmt
Page: 69
Chapter: 2
Section: 2.5
Variables: stmt a statement in ProMela
Notation: \(sub(stmt)\)
Index: 38
Kind: Prop

Name: The set of substatements of stmt
Page: 69
Chapter: 2
Section: 2.5
Variables: stmt a statement in ProMela
Index: 38
Kind: Not
Abbreviation: \(sub(stmt)\)

Question: Semantic of skip
Answer: [$]\texttt{skip}\xhookrightarrow{\text{true}:id}exit[/$]
Page: 71
Chapter: 2
Section: 2.5

Question: Semantic of \(x:=\texttt{expr}\)
Answer: [$]x:=\texttt{expr}\xhookrightarrow{\text{true}:\text{assign}(x,\texttt{expr})}exit[/$]
Page: 71
Chapter: 2
Section: 2.5

Question: Semantic of \(c!\texttt{expr}\)
Answer: [$]c!\texttt{expr}\xhookrightarrow{c!\texttt{expr}}exit[/$]
Page: 71
Chapter: 2
Section: 2.5

Question: Semantic of \(c?x\)
Answer: [$]c?x\xhookrightarrow{c?x}exit[/$]
Page: 71
Chapter: 2
Section: 2.5

Question: Semantic of \(\texttt{atomic}(x_1:=\text{expr}_1;\dots;x_n:=\text{expr}_n)\)
Answer: [$]\texttt{atomic}(x_1:=\text{expr}_1;\dots;x_n:=\text{expr}_n)\xhookrightarrow{\text{true}:Effect(assign(x_n:=expr_n),\dots,Effect(x_1:=expr_1,Id)\dots)}exit[/$]
Page: 71
Chapter: 2
Section: 2.5

Question: Semantic of \(stmt_1;stmt2\)
Answer: [$]\frac{stmt_1\xhookrightarrow{g:\alpha}exit}{stmt_1;stmt_2\xhookrightarrow{g:\alpha}stmt_2}[/$]
Page: 71
Chapter: 2
Section: 2.5
Answer2: [$]\frac{stmt_1\xhookrightarrow{g:\alpha}stmt_1'\ne exit}{stmt_1;stmt_2\xhookrightarrow{g:\alpha}stmt1',stmt_2}[/$]

Question: Two-step semantic of cond_cmd
Answer: [$]\overline{cond\_cmd\xhookrightarrow{g_i:id}stmt'_i}[/$] where id is an action symbol for an action that does not affect the variables.
Page: 72
Chapter: 2
Section: 2.5
Variables: cond_cmd be
if
::g1=>stmt_1
...
::gn=>stmt_n
fi
Index: 39
Kind: Rem

Question: Test-and-set semantic loop
Answer: [$]\frac{stmt_1\xhookrightarrow{h:\alpha}stmt'_i\ne exit}{loop\xhookrightarrow{g_i\land h:\alpha}stmt'_i;loop}[/$]
Page: 72
Chapter: 2
Section: 2.5
Variables: loop
do
::g1=>stmt1
...
::gn=>stmtn
od
Answer2: [$]\frac{stmt_1\xhookrightarrow{h:\alpha}exit\land loop\xhookrightarrow{\bigwedge\neg g_i}exit}{loop\xhookrightarrow{g_i\land h:\alpha}loop}[/$]

Question: Test-and-set semantic of cond_cmd
Answer: [$]\frac{cond\_cmd\xhookrightarrow{g_i\land h:\alpha}stmt'_i}{stmt_1\xhookrightarrow{h:\alpha}stmt'_i}[/$]
Page: 71
Chapter: 2
Section: 2.5
Variables: cond_cmd be if
::g1=>stmt1
...
::gn=>stmtn
fi

Question: Two step semantic of
do
::g1=>stmt1
...
::gn=>stmtn
od
designed as loop
Answer: [$]loop\xhookrightarrow{g_i}stmt_i;loop[/$] and
[$]loop\xhookrightarrow{\bigwedge\neg g_i}exit[/$]
Page: 71
Chapter: 2
Section: 2.5

Name: The synchronous product of the \(TS_i\)
Definition: Set of states \(\Pi S_i\)
Page: 75
Chapter: 2
Section: 2.6
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) transition systems
Notation: \(TS_1\otimes TS_2\)
Index: 42
Kind: Def
Definition2: \(\prod Act_i\)
Conjdef: The TS
Definition3: \[\frac{s_1\xrightarrow\alpha_1s'_1\land s_2\xrightarrow \beta_2s'_2}{\langle s_1,s_2\rangle\xrightarrow{\alpha*\beta}\langle s'_1,s'_2\rangle}\]
Definition4: Initial locations: \(\prod_i I_i\)
Definition5: \(\bigcup_i AP_i\)
Definition6: \(L(\langle s_i\rangle_i)=\bigcup_i L_i(s_i)\)

Definition: The synchronous execution of actions \(\alpha_1\) and \(\alpha_2\)
Page: 75
Chapter: 2
Section: 2.6
Variables: \(TS_i=(S_i,Act_i,\to_i,I_i,AP_i,L_i)\) transition systems,
\(\alpha_i\in Act_i\)
Notation: \(\alpha_1*\alpha_2\)
Index: 42
Kind: Def

Question: (size explosion problem omitted)
Answer: fini
Page: 81

Name: The \(TS\) of \(S\)
Definition: -The set of states is \(Eval(x_1,\dots,x_n,r_1,\dots,r_k)\)
-The set of actions is a singleton \(\{\tau\}\),
-The transition function is \((a_1,\dots,a_n,\ c_1,\dots,c_k)\to (a'_1,\dots,a'_n,\delta_{r_1}(a_1,\dots,a n,c_1,\dots,c_k),\dots,\delta_{r_k}(a_1,\dots,a n,c_1,\dots,c_k))\)
-The set of initial states is \(\left\{(a_1,\dots,a_n,c_{0,1},\dots,c_{0,k}\mid a_1,\dots,a_n\in\{0,1\}\right\}\)
-The set of atomic predicate is \(\{x_1,\dots,x_n,y_1,\dots,y_m,r_1,\dots,r_k\}\)
-The set \(L\) is \((a_1,\dots,a_n,c_1,\dots,c_k)\mapsto\{x_i\mid a_i=1\}\cup \{r_j\mid c_j=1\}\cup\{y_i\mid s\models \lambda_{y_i}(a_1,\dots,a_n,c_1,\dots,c_k)=1\}\).
Page: 28
Chapter: 2
Section: 1.2
Variables: \(S=(n,k,m,c_{0,1},\dots,c_{0,k},\delta_{r_1}\dots,\delta_{r_k},\lambda_{y_1},\dots,\lambda_{y_m})\) a sequential hardware circuit

Name: The TS semantic of \(PG\)
Definition: \(S=Loc\times Eval(Var)\)
Page: 34
Chapter: 2
Section: 1.2
Variables: \(PG=(Loc,Act,Effect,\hookrightarrow,Loc_0,g_0)\) a program graph over set \(Var\)
Notation: \(TS(PG)\)
Index: 15
Kind: Def
Definition2: [$] \frac{l\xhookrightarrow{g:\alpha}l'\land \eta\models g} {\langle l,\eta\rangle\xrightarrow{\alpha}\langle l',Effect(\alpha,\eta)\rangle}[/$],
Conjdef: The TS with
Definition3: \(I=\{\langle l,\eta\rangle\mid l\in Loc_0,\eta\models g_0\}\)
Definition4: \(AP=Loc\cup Cond(Var)\),
Definition5: \(L(\langle l,\eta\rangle)=\{l\}\cup \{g\in Cond(Var)\mid \eta\models g\}\).

Definition: \(\bigcup_{s\in C}Post(s)\)
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(C\subseteq S\),
\(\alpha\in Act\)
Notation: \(Post(C)\)
Index: 3
Kind: Def

Definition: \(\bigcup_{\alpha\in Act}Post(s,\alpha)\)
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS,
\(s\in S\)
Notation: \(Post(s)\)
Index: 3
Kind: Def

Question: Nondeterminism represents
Answer: several options for the possible behaviors by nondeterminism.
Page: 23
Chapter: 2
Section: 1
Variables: \((S,Act,\to,I,AP,L)\) a TS

Name: An infinite execution fragment
Definition: An alternating sequences of states and actions:
\[s_0\alpha_1\dots\] such that \(s_i\xrightarrow{\alpha_{i+1} }s_{i+1}\) for all \(i\in\mathbb N\).
Page: 24
Chapter: 2
Section: 1.1
Variables: \((S,Act,\to,I,AP,L)\) a TS
Index: 6
Kind: Def

Instruction: x:=expr
Page: prog
65
Effect: Affect the value of expr to x
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog

Instruction: c?x
Page: prog
65
Effect: Read a value on c assign it to x
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog

Instruction: c!expr
Page: prog
65
Effect: Sends the value of expr on the canal c
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog

Instruction: expr1;expr2
Page: prog
65
Effect: Execute expr1 followed by expr2
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog

Instruction: skip
Page: prog
65
Effect: doing nothing, during a single step
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog

Instruction: do
::g1=>stmt1
...
::gn=>stmtn
od
Page: prog
65
Effect: While some gi holds, execute, nondeterministically, a stmti such that the guard gi holds. Halts if no gi is satisfied.
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog

Instruction: if
::g_1=>stmt_1
...
::g_n=>stmt_n
::else=>stmt'
fi
Page: prog
73
Effect: execute, nondeterministically, a stmt_i such that the guard g_i holds.
Execute stmt' if no guard holds
Context: Promela
Chapter: 2
Section: 2.5
Extra: prog
Index: 40
Kind: Rem

Name: The set of reachable state of \(TS\).
Page: 26
Chapter: 2
Section: 1.1
Variables: \(TS=(S,Act,\to,I,AP,L)\) a TS
Index: 10
Kind: Def
Abbreviation: \(Reach(TS)\)