Lectures 9 and 10: 29th October 2019

Question 1

What is Eval(Var)?

Answer 1

Eval(Var) = the set of variable evaluations over Var that are possible = {η1, η3, ηn}

Var is a set of typed state variables

Question 2

How are TSes defined?

Answer 2

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 = labelling function: determines which APs hold in which states

Question 3

How are PGs defiend?

Answer 3

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
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 4

What’s the difference between a TS and a PG?

Answer 4

PG has locations rather than states and its transitions are conditional, and effects of transitioning (=> action => changing Eval(Var)) are also defined. Interleaved PGs don’t interfere with global variables.

The program graph consisting of locations as nodes and conditional transitions as edges is not a transition system since the edges are provided with conditions.

However, each program graph can be interpreted as a transition system. The underlying transition system of a program graph results from unfolding: a state of the transition system is composed of a location l of the program graph and an evaluation η of the variables.

Question 5

What is parallel composition?

Answer 5

( 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 6

How does parallel composition work with TSes?

Answer 6

Doesn’t - may only be done with PGs

Question 7

What is interleaving?

Answer 7

Composing combinations of actions by different program processes, examining only their effects on their local variables (doesn’t handle globals).

Question 8

How does interleaving work with TSes?

Answer 8

The interleaving operator for transition systems simply
constructs the cartesian product of the individual state
spaces without considering potential conflicts from
shared variables.

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 9

What is the TS of a PG?

Answer 9

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

????????

Question 10

How does interleaving work with PGs?

Answer 10

The interleaving operator for transition systems simply
constructs the cartesian product of the individual state
spaces without considering potential conflicts from
shared variables. For programs with shared variables, we define interleaving directly on program graphs PG1 ||| PG2

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 11

When would you interleave PGs?

Answer 11

When interleaving programs with shared variables

Question 12

What is an effect function?

Answer 12

Tells you what the outcome of each transition/action is on Eval(Var), i.e. how variable values change. The function takes start evaluation and action and gives outcome evaluation.

Question 13

How do the possibility of transitions change after interleaving TSes? And PGs?

Answer 13

For both, any transitions that were possible in a component TS or PG prior to interleaving is still possible after interleaving without affecting other TSes/PGs.

Question 14

How is interleaving different for PGs and TSes?

Answer 14

Interleaved PGs can’t interfere with global variables but this is possible in interleaved TSes.

Question 15

Why can TS interleaving be described as the Cartesian product of states?

Answer 15

Interleaving TSes is just the Cartesian product of states to find all possible pairs.

Question 16

How are the local (to each component PG) and global variables of a composed program graph defined?

Answer 16

• Local variables of PG1 are x1 ∈ Var1∖Var2
• Local variables of PG2 are those in x2 ∈ Var2∖Var1
• Global variables are x ∈ Var1 ∩ Var2

Question 17

What are critical actions in composed PGs?

Answer 17

Actions that access global variables are critical. Critical actions cannot be executed simultaneously.

Question 18

What are composed PGs?

Answer 18

A PG resulting from the parallel composition of two other PGs

Question 19

What is the PG level? Why is it “higher”?

Answer 19

Modelling a program with a PG rather than a TS. It is a higher level because it doesn’t allow for global interference when interleaving and is another added conversion from a TS.

Question 20

How is interleaving different from parallel composition?

Answer 20

Parallel composition is complete interleaving. It can only be done with PGs whereas incomplete interleaving can also be done with TSes. Complete interleaving doesn’t allow for processes (PGs) to interfere with global variables but incomplete interleaving does.

Question 21

Why must composition with actions that affect global variables be carried out at the PG level?

Answer 21

PGs have an effect function that tells you the values of each variable after each action (transition), so in each state. They don’t interfere when being interleaved completely.

Question 22

What is a semaphore?

Answer 22

A variable or abstract data type used to control access to a common resource by multiple processes in a concurrent system such as a multitasking operating system.

Question 23

How can semaphores implement mutual exclusion?

Answer 23

Have a boolean of if in critical section or int above/below threshold value. Only allow in when false, set to true when in critical section or accessing a resource, then to false after to allow others in.

Question 24

How do you interleave two PGs to enforce mutual exclusion?

Answer 24

Have 1 PG to operate a semaphore and either be in locations of waiting, critical section, or waiting for access. Then carry out parallel composition by performing incomplete interleaving and then eliminating unreachable locations.

Question 25

How do you prove which states in a composed graph are reachable?

Answer 25

For all transitions, check the state of variables before them and after them for the process associated with the transition by building its variable states from the root/initial states. If the conditions of the transition would not allow them from the initial variable values then eliminate the transition.

Question 26

How does parallel composition work for PGs?

Answer 26

Make locations as the cartesian product: each possible combination group of states in each process. Make each transition according to each new location based on the process changing in them, and then eliminate unreachable states.

Question 27

What is handshaking?

Answer 27

When perfectly synchronised communications between interleaved processes lead to them performing actions simultaneously

Question 28

What does the handshaking operation do?

Answer 28

Perform interleaving on TSes or PGs and then consider actions for transitions. If their actions are independent then leave them, but otherwise if guard makes them dependent then if they both happen then ensure they both take effect simultaneously.

Question 29

How is the handshaking operation notated?

Answer 29

Let TSi=(Si, Acti,Ti, Ii, APi, Li), i=1,2 be transition systems and H⊆Act1∩Act2 with τ∉H. TS1 ||H TS2 is:

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

L(⟨s1, s2⟩) = L1(s1) ∪ L2(s2)

T is such that:

if an action, α, is in both and can be executed in a transition from the current states of both TSes (synchronisation):

s1 -α-> 1 s’1 ⋀ s2 -α->2 s’2
given that:
⟨s1,s2⟩ -α-> ⟨s’1,s’2⟩

i.e. that if you can transition from start locations from the interleaved TSes - with actions in both languages and from both start states - both transitions occur simultaneously

else then act as interleaving, i.e. perform the action with 1 TS without affecting the other/s:

s1 -α-> 1 s’1 given that ⟨s1, s2⟩ -α-> ⟨s’1, s2⟩
and
s2 -α-> 2 s’2 given that ⟨s1, s2⟩ -α-> ⟨s1, s’2⟩

Question 30

How are the conditions for interleaving and synchronisation different?

Answer 30

if an action, α, is in both and can be executed in a transition from the current states of both TSes with synchronisation (otherwise falling back to interleaving):

s1 -α-> 1 s’1 ⋀ s2 -α->2 s’2
given that:
⟨s1,s2⟩ -α-> ⟨s’1,s’2⟩

i.e. that if you can transition from start locations from the interleaved TSes - with actions in both languages and from both start states - both transitions occur simultaneously

with interleaving, i.e. perform the action with 1 TS without affecting the other/s:

s1 -α-> 1 s’1 given that ⟨s1, s2⟩ -α-> ⟨s’1, s2⟩
and
s2 -α-> 2 s’2 given that ⟨s1, s2⟩ -α-> ⟨s1, s’2⟩

Question 31

What is perfect synchronisation?

Answer 31

When two or more interleaved processes execute simultaneously as their actions are compatible

Question 32

What happens if 1 TS in a handshaking product disallows an action?

Answer 32

Just use interleaving as before

Question 33

What happens with a handshaking operation if there is no possible synchronisation of actions?

Answer 33

Just use interleaving as before

Question 34

How can multiway handshaking be modelled?

Answer 34

Use the parallel composition of transition systems TS1 through TSn where H ⊆ Act1 ∩ … ∩ Actn representing multiway handshaking (e.g., to model broadcasting)

Question 35

How can mutual exclusion be implemented with an arbiter and handshaking?

Answer 35

Model a binary semaphore that regulates access to the critical section by a separate process called “Arbiter” that interacts with other processes by means of handshaking

Question 36

How can you implement a mutual exclusion LTL given a binary semaphore and two processes?

Answer 36

☐(¬crit1 ∨ ¬crit2)

i.e. it’s always true that at least one is not in the critical section

Question 37

How can you implement an LTL to check that two processes will get access to critical sections infinitely often?

Answer 37

(☐◇crit1) ⋀ (☐◇crit2)

i.e. process 1 will get into its critical section infinitely often (always eventually) and so will process 2

Question 38

What is the difference between W and U?

Answer 38

W = weak until
U = strong until

In strong until the second operand must eventually become true. Weak until holds if the first is always true and the second never becomes true.

Question 39

What are the LTL properties to satisfy mutual exclusion?

Answer 39

☐(¬crit1 ∨ ¬crit2)
and (☐◇wait1→ ☐◇crit1) ⋀ (☐◇wait2→ ☐◇crit2)
and ☐ ((y=0) → crit1 ∨ crit2)

i.e. it’s always true that at least one is not in the critical section, every waiting process will eventually enter its critical section, and whenever the semaphore y has the value 0, one of the processes is in its critical section

Question 40

When does a state satisfy a property?

Answer 40

If and only if all paths starting in the state satisfy the property

Question 41

When does a TS satisfy a property?

Answer 41

If and only if all initial paths satisfy the property

i. e. if and only if all initial states satisfy the property
i. e.if and only if all paths starting in each initial state satisfy the property

Question 42

Is it true that a TS may not satisfy a property and also not satisfy its negation?

Answer 42

Yes. It means it doesn’t satisfy the property, nor its negation, though some execution paths do satisfy both - there are both possible

Question 43

How can you prove possibility: a property being true in at least one execution of a TS?

Answer 43

To prove a property is possible in a TS, prove that its negation does not hold

Question 44

What does it mean for a path to satisfy a property?

Answer 44

The property evaluates to true for that path

Question 45

How do you determine which parts of an interleaved TS are reachable?

Answer 45

Check if states have transitions going to them and if so the guard conditions on those transitions hold

Question 46

Can you assess LTL properties that contain variables not found in the model?

Answer 46

No

Question 47

Do implications whose first operand isn’t true hold?

Answer 47

Yes, trivially since after every time the first operand happens, the second doesn’t not happen.