Lectures 7 and 8: 15th October 2019 Flashcards Preview

CS4052 Logic and Software Verification > Lectures 7 and 8: 15th October 2019 > Flashcards

Flashcards in Lectures 7 and 8: 15th October 2019 Deck (50)
Loading flashcards...
1

What does Spin use as its underlying model?

Labelled Transition Systems

2

How can TSes be modelled as graphs?

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

3

What are action names?

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

4

What are atomic propositions?

A statement or assertion that must be true or false.

5

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

6

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.

7

What are direct-α successors?

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

8

What are α-predecessors?

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

9

What is a terminal state in a TS?

A state which has no successors for any action.

10

When is nondeterminism useful?

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

11

What is action-based determinism?

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

12

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 (∅).

13

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

14

What are infinite execution fragments?

An execution fragment which loops infinitely, without ever terminating.

15

What are maximal execution fragments?

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

16

What are initial execution fragments?

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

17

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.

18

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.

19

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.

20

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

21

What is conditional branching?

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

22

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.

23

How do you notate conditional transactions?

g:α, where g is a Boolean condition (guard) and α is an
action possible provided g holds.

24

What are action effects?

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

25

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.

26

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.

27

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

28

What is Eval(Var)?

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

29

What is Cond(Var)?

Cond(Var) = set of boolean conditions over Var
Var is a set of typed state variables

30

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