Exam: Question 4 Flashcards Preview

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

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

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.


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



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.


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



What are partial semantics?



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



What is a correctness condition?



What is the syntax of correctness conditions?



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



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



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


How do you perform handshaking composition on two TSes?



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



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



What are the differences between TSes and petri nets?



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



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



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



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



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



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



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



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



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



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



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



How do you model a given algorithm with petri nets?



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



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



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