Brainscape's Knowledge GenomeTM

Browse over 1 million classes created by top students, professors, publishers, and experts.


See full index

CS4052 Logic and Software Verification > Exam: Question 1 > Flashcards

Exam: Question 1 Flashcards

TSes, LTL, PGs, composition, expressing LTL conditions

1
Q

How do you convert a pseudocode process into a program graph?

A
  • think of locations as ~ states of the system that you move between
  • think of actions that can be performed in a state to go to other states (or same state)
  • define the variables in the PG that are operated on
  • define the effect functions for each action: how vars change
  • define the initial location/s
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

How do you convert a program graph into a transition system?

A
  • combine locations and evaluations (variable value combos) into states
  • copy the actions across
  • check evals hold on transitions from the PG eval before it
  • initial states are from locations in Loc0 whose eval entails g0
  • make APs in each state from current variable eval
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

How do you convert a pseudocode process into a transition system?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

What does the || operator mean?

A

parallel composition

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

How do you construct the parallel composition of 2 TSes?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

How do you check whether a TS satisfies mutual exclusion?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

How do you check whether a TS ensures no individual is ever starved (starvation freedom)?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

What is a safety property?

A

Safety properties are about “nothing bad should happen”.

Example: the mutual exclusion property - always at most one process is in its critical section. The bad thing (having two or more processes in their critical section simultaneously) never occurs.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

What is a liveness property?

A

Liveness properties are about “something good will eventually happen”.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

What is the difference between a safety and liveness property?

A

Safety properties are about “nothing bad should happen”. Liveness properties are about “something good will eventually happen”.

Safety properties refer to all states in the system. Liveness properties need to be checked for all possible system runs/executions.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

How do you define a safety property for a TS in LTL?

A

say always not ( bad thing ), i.e. ! [] (bad condition)

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

How do you implement mutual exclusion as an LTL property?

A

☐(¬crit1 ∨ ¬crit2)

never true that both processes are in their critical sections

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

How do you implement starvation freedom as a LTL property?

A

(☐◇wait1→ ☐◇crit1) ⋀ (☐◇wait2→ ☐◇crit2)

every waiting process will eventually enter its critical section, i.e. starvation freedom

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

What kind of property does mutual exclusion represent?

A

safety

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

How do you find a LTL formula that is or is not satisfied by a path in a given TS?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

How do you find the reachable part of a TS?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
17
Q

How do you find the reachable part of a TS that is the result of a composition operation on two program graphs?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
18
Q

How do you find and describe an execution that proves that an entire TS is infinite?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
19
Q

How do you find whether an algorithm satisfies mutual exclusion?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
20
Q

How do you find whether two processes ever enter deadlock?

A

!

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
21
Q

How do you find whether two processes ever begin to mutually wait on each other?

A

!

22
Q

How do you find whether a process that wants to enter its critical section has to wait forever?

A

!

23
Q

How do you formally define a TS?

A

!

24
Q

How do you formally define a TS to model a real-world system?

A

!

25
Q

How do you find the number of reachabke states in a TS?

A

!

26
Q

What is invalid behaviour in a TS?

A

!

27
Q

How do you find whether a TS defines invalid behaviour over all possible executions?

A

!

28
Q

What is the handshaking composition operator?

A

!

29
Q

How does the handshaking composition operator work?

A

!

30
Q

Prove that the handshaking composition operator is not associative.

A

!

31
Q

What kind of property does a LTL formula ensuring mutual exclusion represent?

A

!

32
Q

What kind of property does a LTL formula ensuring starvation freedom represent?

A

!

33
Q

How do you find a path in a given TS satisfying a given LTL formula?

A

!

34
Q

How do you compose formally defined TSes?

A

!

35
Q

How do you find the number of reachable states from a formally defined TS?

A

!

36
Q

How do you find whether a process ever enters individual starvation?

A

!

37
Q

What does starvation freedom mean?

A

each waiting process will eventually enter its critical section

38
Q

What does mutual exclusion mean?

A

!

39
Q

How do you formally define a TS?

A

!

40
Q

How do you find all the paths in a given TS satisfying a given LTL formula?

A

!

41
Q

What does “a state in which both processes are mutually waiting for each other” mean?

A

!

42
Q

What does “a process that wants to enter the critical section has to wait ad infinitum” mean?

A

!

43
Q

How can you formalise the following operator with an LTL formula? ”At next” φ N ψ: at the next time where ψ holds, φ also holds

A

!

44
Q

How can you formalise the following operator with an LTL formula? ”Before” φ B ψ: if ψ holds sometime, φ does so before.

A

!

45
Q

How do you define new operators in LTL?

A

!

46
Q

How do you define a TS that represents an arbiter that interacts with a given system using chosen transitions?

A

!

47
Q

How can an arbiter that interacts with a given system using chosen transitions limit the number of processes simultaneously in their critical section?

A

!

48
Q

How do you perform parallel composition with an arbiter?

A

!

49
Q

How do you perform parallel composition with a handshake with an arbiter?

A

!

50
Q

How do you formally define a given pictoral TS?

A

!

CS4052 Logic and Software Verification (17 decks)

Brainscape helps you reach your goals faster, through stronger study habits.
© 2024 Bold Learning Solutions. Terms and Conditions