Lectures 7 and 8: 15th October 2019 Flashcards
Transition Systems
What does Spin use as its underlying model?
Labelled Transition Systems
How can TSes be modelled as graphs?
Nodes represent the states and the edges represent the program’s transitions between them.
What are action names?
The identifiers sent from one process to another to perform certain functionality. Used in inter-process comms.
What are atomic propositions?
A statement or assertion that must be true or false.
How do you formally define a transition system?
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
Why is the labelling function in a TS equal to 2 ** AP?
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.
What are direct-α successors?
All the states that can be transitioned to from a current state given the action α.
What are α-predecessors?
All the states that can transition to a current state given the action α.
What is a terminal state in a TS?
A state which has no successors for any action.
When is nondeterminism useful?
It can be useful for abstraction and underspecification and modelling stochastic environments and parallelism.
What is action-based determinism?
Systems are action-based deterministic iff there is ⩽ 1 transition from a state for each action.
What is state-based determinism?
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 (∅).
What are execution fragments?
Possible alternating sequences of states and actions that represent a trace of execution. For example, ϱ = s0 α1 s1 α2 s2 … αn sn
What are infinite execution fragments?
An execution fragment which loops infinitely, without ever terminating.
What are maximal execution fragments?
An execution fragment which is infinite or terminates in a terminal state - goes to the end of the execution.
What are initial execution fragments?
An execution fragment starts in an initial state - goes from the start of the execution.
What are reachable states?
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.
How can you tell if a state is reachable from execution fragments?
All reachable states have initial and finite execution fragments which terminate on them.
When can states with connections (transactions going to them) still be unreachable?
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.
How do you label states, APs, and actions on TS diagrams?
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
What is conditional branching?
A programming instruction that directs the computer to different parts of the program based on the results of a comparison.
Can TSes represent conditional branching? If so, how?
Could have child states for all possible variable states, but with already present state explosion doing this is bad. Use conditional transitions instead.
How do you notate conditional transactions?
g:α, where g is a Boolean condition (guard) and α is an
action possible provided g holds.
What are action effects?
How the performance of an action alters state (global) variables.
How can you obtain a TS from a graph containing conditional transitions?
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.
What is a program graph?
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.
How do you formally define program graphs?
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
What is Eval(Var)?
Eval(Var) = η = set of variable evaluations over Var
Var is a set of typed state variables
What is Cond(Var)?
Cond(Var) = set of boolean conditions over Var
Var is a set of typed state variables
How do you formalise the effect of actions?
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
What is the difference between location and state?
location = a possible situation in a program’s execution that models a representation of past events and outcomes
state = location + variable values
How do you notate states from locations and conditions?
state = ⟨l,η⟩, where l = location, and η = state variable evaluation
How do you define the transition system for a program graph?
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(α,η)⟩
What does T⊆S×Act×S represent within transition systems?
The transitions, from a current state, taking an action and giving a resultant state.
What does the || operator mean?
parallel composition; it is usually commutative and associative but depends on the kind of communication supported.
What does the ||| operator mean?
complete interleaving (with total independence)
Why does complete interleaving with a shared variable to a depth of 2 give a diamond shape?
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.
What is the output of a complete interleaving operation on TSes?
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
How do you prevent interference of variables with the same names in two completely interleaved TSes?
Need to resolve variables at a higher level with joined system and variable names in the program graph.
How are transitions from complete interleaving operations constrained?
⟨s1, s2⟩ –α–> ⟨s’1, s2⟩
and
⟨s1, s2⟩ –β–> ⟨s1, s’2⟩
How do you interleave program graphs?
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
What are critical actions?
Functionality performed by a program which access global variables and cannot be executed simultaneously
What composes states in interleaved TSes?
tuples of the current variable values (evaluation) and location of each interleaved TS
How do you notate the local variables of a program graph, PG1, that is completely interleaved with another program graph, PG2?
x1 ∈ Var1 ∖ Var2
How do you notate the global variables of completely interleaved program graphs PG1 and PG2?
x ∈ Var1 ∩ Var2
Are actions that are indivisible in program graphs indivisible in the model?
Yes
Which actions do TSes express the effects of? What are the consequences of this?
TS only expresses the effects of actions that are completely executed.
What is an execution of a transition system?
an initial and maximal execution fragment
What is parallel composition?
( 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.
What is complete interleaving?
When two LTSes (programs) execute simultaneously and take turns nondeterministically. They often interfere with each other when using shared variables.
