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