Lectures 7 and 8: 15th October 2019

Question 1

What does Spin use as its underlying model?

Answer 1

Labelled Transition Systems

Question 2

How can TSes be modelled as graphs?

Answer 2

Nodes represent the states and the edges represent the program’s transitions between them.

Question 3

What are action names?

Answer 3

The identifiers sent from one process to another to perform certain functionality. Used in inter-process comms.

Question 4

What are atomic propositions?

Answer 4

A statement or assertion that must be true or false.

Question 5

How do you formally define a transition system?

Answer 5

Transition Systems are defined as (S, Act, T, I, AP, L)

where

S = finite set of states
Act = finite set of actions: ~ inputs
T = set of transitions, in form T ⊆ (S x Act x S): which state to go to from a current state for a given action
I = set of initial states
AP = set of atomic propositions
L:S→2 ^ AP = labelling function: determines which APs hold in which states

Question 6

Why is the labelling function in a TS equal to 2 ** AP?

Answer 6

The number of labels for each state will be equal to 2 ^ |AP| since each AP is binary - each possible combo of true/false satisfaction.

Question 7

What are direct-α successors?

Answer 7

All the states that can be transitioned to from a current state given the action α.

Question 8

What are α-predecessors?

Answer 8

All the states that can transition to a current state given the action α.

Question 9

What is a terminal state in a TS?

Answer 9

A state which has no successors for any action.

Question 10

When is nondeterminism useful?

Answer 10

It can be useful for abstraction and underspecification and modelling stochastic environments and parallelism.

Question 11

What is action-based determinism?

Answer 11

Systems are action-based deterministic iff there is ⩽ 1 transition from a state for each action.

Question 12

What is state-based determinism?

Answer 12

Systems are state-based deterministic iff there is ⩽ 1 direct successor for each state whose list of holding APs is exactly the same, except for none holding (∅).

Question 13

What are execution fragments?

Answer 13

Possible alternating sequences of states and actions that represent a trace of execution. For example, ϱ = s0 α1 s1 α2 s2 … αn sn

Question 14

What are infinite execution fragments?

Answer 14

An execution fragment which loops infinitely, without ever terminating.

Question 15

What are maximal execution fragments?

Answer 15

An execution fragment which is infinite or terminates in a terminal state - goes to the end of the execution.

Question 16

What are initial execution fragments?

Answer 16

An execution fragment starts in an initial state - goes from the start of the execution.

Question 17

What are reachable states?

Answer 17

States that can be transitioned to in a path from an initial state. They will have initial and finite execution fragments which terminate on them. Unreachable states have no predecessors.

Question 18

How can you tell if a state is reachable from execution fragments?

Answer 18

All reachable states have initial and finite execution fragments which terminate on them.

Question 19

When can states with connections (transactions going to them) still be unreachable?

Answer 19

The actions and conditions triggering the transitions to the state are impossible, or if all the states that would lead to it are themselves unreachable.

Question 20

How do you label states, APs, and actions on TS diagrams?

Answer 20

states as name inside of a circle

APs as a comma-separated list (of those holding) above a state, within a {} wrapper: {AP1, AP2}

actions as name over an arrow (associated transition) between states

Question 21

What is conditional branching?

Answer 21

A programming instruction that directs the computer to different parts of the program based on the results of a comparison.

Question 22

Can TSes represent conditional branching? If so, how?

Answer 22

Could have child states for all possible variable states, but with already present state explosion doing this is bad. Use conditional transitions instead.

Question 23

How do you notate conditional transactions?

Answer 23

g:α, where g is a Boolean condition (guard) and α is an

action possible provided g holds.

Question 24

What are action effects?

Answer 24

How the performance of an action alters state (global) variables.

Question 25

How can you obtain a TS from a graph containing conditional transitions?

Answer 25

A graph containing conditional transitions as edges is
not a transition system. We can obtain one by unfolding the graph: merge transitions with the same effects but different conditions and add states and make them represent the changes instead by adding information to the state on the variables that dictated the conditional transitions. Instead of conditional transitions being impossible, there will simply not be a transition between two states if their global (state) variables prevent this.

Question 26

What is a program graph?

Answer 26

Program graphs are a graphical representation of a program’s source code. For Spin models, the nodes of the program graph represent the states and the edges represent the program’s transitions between them. States will have code fragments to execute.

Question 27

How do you formally define program graphs?

Answer 27

A PG over set Var of typed variables is a tuple
PG = (Loc, Act, Effect, Ct, Loc0, g0) where

Loc is a set of locations and Act is a set of actions
Effect: Act × Eval(Var)→Eval(Var) is the effect function
Ct ⊆ Loc × Cond(Var) × Act × Loc is the conditional transition relation
Loc0 ⊆ Loc set of initial locations l1 –g:α–> l2
g0 ∈ Cond(Var) is the initial condition

every location in initial locations, Loc0, satisfies the initial condition, g0

Eval(Var) = η = set of variable evaluations over Var
Cond(Var) = set of boolean conditions over Var
Var is a set of typed state variables

Question 28

What is Eval(Var)?

Answer 28

Eval(Var) = η = set of variable evaluations over Var

Var is a set of typed state variables

Question 29

What is Cond(Var)?

Answer 29

Cond(Var) = set of boolean conditions over Var

Var is a set of typed state variables

Question 30

How do you formalise the effect of actions?

Answer 30

Effect: Act × Eval(Var)→Eval(Var)

Eval(Var) = η = set of variable evaluations over Var
Var is a set of typed state variables
Act is an action

Question 31

What is the difference between location and state?

Answer 31

location = a possible situation in a program’s execution that models a representation of past events and outcomes

state = location + variable values

Question 32

How do you notate states from locations and conditions?

Answer 32

state = ⟨l,η⟩, where l = location, and η = state variable evaluation

Question 33

How do you define the transition system for a program graph?

Answer 33

The TS(PG) of a PG = (Loc, Act, Effect, Ct, Loc0, g0) over Var is the tuple (S, Act, T, I, AP, L) where

S = Loc × Eval(Var)
T ⊆ S × Act × S
I = {⟨l,η⟩ | l ∈ Loc0 and η ⊨ g0}
AP = Loc ∪ Cond(Var)
L (⟨l,η⟩) = {l} ∪ {g ∈ Cond(Var) | η ⊨ g}

T ⊆ S × Act × S defined by the rule:
if premise holds, then conclusion holds; formally,

l1 –g:α–> l2 ⋀ η ⊨ g
—————————— (horizontal line like division)
⟨l1, η⟩→⟨l2, Effect(α,η)⟩

Question 34

What does T⊆S×Act×S represent within transition systems?

Answer 34

The transitions, from a current state, taking an action and giving a resultant state.

Question 35

What does the || operator mean?

Answer 35

parallel composition; it is usually commutative and associative but depends on the kind of communication supported.

Question 36

What does the ||| operator mean?

Answer 36

complete interleaving (with total independence)

Question 37

Why does complete interleaving with a shared variable to a depth of 2 give a diamond shape?

Answer 37

Effects of both LTSes will have the same effect as they are independent, so will combine to the same outcome regardless of which comes first. So single outcome (bottom state), with two paths there - via each of the two LTSes going first.

Question 38

What is the output of a complete interleaving operation on TSes?

Answer 38

Let TSi = (Si, Acti, Ti, Ii, APi, Li) be two interleaved transition systems.

TSi = TS1 ||| TS2 = (S1 × S2, Act1 ∪ Act2, T, I1 × I2, AP1 ∪ AP2, L)

where T is such that:

⟨s1, s2⟩ –α–> ⟨s’1, s2⟩

and

⟨s1, s2⟩ –β–> ⟨s1, s’2⟩

and L(⟨s1, s2⟩) = L1(s1) ∪ L2(s2)
for α ∈ Act1, β ∈ Act2

Question 39

How do you prevent interference of variables with the same names in two completely interleaved TSes?

Answer 39

Need to resolve variables at a higher level with joined system and variable names in the program graph.

Question 40

How are transitions from complete interleaving operations constrained?

Answer 40

⟨s1, s2⟩ –α–> ⟨s’1, s2⟩

and

⟨s1, s2⟩ –β–> ⟨s1, s’2⟩

Question 41

How do you interleave program graphs?

Answer 41

Let PGi = (Loci, Acti, Effecti, C(t,i), Loc(0,i), g(0,i)) be two program graphs over variables

PGi = PG1 ||| PG2 over Var1 ∪ Var2 = (Loc1 × Loc2, Act1 ⊎ Act2, Effect, Ct, Loc(0,1) × Loc(0,2), g(0,1) ⋀ g(0,2))

⊎ = disjoint union
⋀ = conjuction (‘and’ operator)

⟨l1, l2⟩ –g:α–> ⟨l’1, l2⟩

and

⟨l1, l2⟩ –g:β–> ⟨l1, l’2⟩

and Effect(α, η)(v) = Effecti(α, η)(v) if α ∈ Acti, v ∈ Vari

Question 42

What are critical actions?

Answer 42

Functionality performed by a program which access global variables and cannot be executed simultaneously

Question 43

What composes states in interleaved TSes?

Answer 43

tuples of the current variable values (evaluation) and location of each interleaved TS

Question 44

How do you notate the local variables of a program graph, PG1, that is completely interleaved with another program graph, PG2?

Answer 44

x1 ∈ Var1 ∖ Var2

Question 45

How do you notate the global variables of completely interleaved program graphs PG1 and PG2?

Answer 45

x ∈ Var1 ∩ Var2

Question 46

Are actions that are indivisible in program graphs indivisible in the model?

Answer 46

Yes

Question 47

Which actions do TSes express the effects of? What are the consequences of this?

Answer 47

TS only expresses the effects of actions that are completely executed.

Question 48

What is an execution of a transition system?

Answer 48

an initial and maximal execution fragment

Question 49

What is parallel composition?

Answer 49

( P || Q) expresses the parallel composition of the processes P and Q. It constructs an LTS which allows all the possible interleavings of the actions of the two processes. Actions, which occur in the alphabets of both P and Q, constrain the interleaving since these actions must be carried out by both of the processes at the same time. These shared actions synchronise the execution of the two processes. If the processes contain no shared actions then the composite state machine will describe all interleavings.

The parallel composition operator can be used to put processes in parallel. The behaviour of p ∥ q is the arbitrary interleaving of actions of the processes p and q, assuming for the moment that there is no communication between p and q. For example, the process a ∥ b behaves like a · b + b · a.

Question 50

What is complete interleaving?

Answer 50

When two LTSes (programs) execute simultaneously and take turns nondeterministically. They often interfere with each other when using shared variables.