Exam: Question 4 Flashcards Preview

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

Flashcards in Exam: Question 4 Deck (52)
Loading flashcards...
1

What is a petri net?

A mathematical model of distributed systems made of tokens, places, and transitions, which can allow concurrency.

Places are similar to locations and are represented by circles.

Tokens are objects/resources, represented by dots inside locations.

Transitions are modelled as squares/rectangles and move tokens between locations.

2

How do you give petri nets that generate all words that are prefixes of a given language?

!

3

How do you make a petri net to model an example of mutual exclusion with 2 processes?

Have two competing processes and a mutex place. Both transitions to allow both access to their critical sections require both the mutex and waiting place for the process to have a token, and removes them from both, placing a token into the processes' critical section place. Then once done, the token is removed and the tokens in the waiting place and mutex place are restored.

4

How can you show a Petri net model satisfies mutual exclusion?

!

5

What are partial semantics?

!

6

How do you find the partial semantics for all given programs and states?

!

7

What is a correctness condition?

!

8

What is the syntax of correctness conditions?

!

9

How do you prove or disprove correctness conditions against a given program?

!

10

How do you form correctness conditions to describe the behavior of programs?

!

11

How do you perform a parallel composition of 2 TSes?

- draw the TSes out individually with their states, transitions, and APs
- find all possible unique pairs of states
- draw the transitions between the states based upon the changes that cause them in the original TSes
- eliminate unreachable states
- eliminate states where only 1 state changes but both would for the same action
- add APs to each state pair by appending those in states in each individual TS

12

How do you perform handshaking composition on two TSes?

!

13

How do you give the minimal petri net equivalent to a TS?

!

14

How do you find which parts of a petri net are equivalent to a TS which the petri net is equivalent to?

!

15

What are the differences between TSes and petri nets?

!

16

How can you find a safety property that holds in one composed TS but not another?

!

17

How do you define the satisfaction of LTL formulae [] p and <> p over Petri nets, where p is an atomic proposition? Illustrate your answer.

!

18

How do you make a petri net that produces a given language?

!

19

How do you find the reachable states in a pseudocode program with processes from a given start state and variable value?

!

20

How do you make a correctness condition to describe the behavior of a program with respect to a variable?

!

21

How do you find the reachability graph of a petri net?

!

22

How do you find the overlapping graph of a petri net?

!

23

How do you model a real-world system with a petri net?

!

24

How do you find which states are reachable from a given start state with given starting variable values for a program running given processes?

!

25

How do you show whether a TS holds a given LTL formula with a given fairness constraint?

!

26

How do you find a path for which a TS does not hold a given LTL formula?

!

27

How do you model a given algorithm with petri nets?

!

28

How can you show whether a petri net satisfies starvation freedom?

!

29

How do you define the semantics of LTL for petri nets to describe properties of state-based semantics?

!

30

How can you find a valid global execution fragment of a given TS?

!