Flashcards in Exam: Question 1 Deck (50)
How do you convert a pseudocode process into a program graph?
- 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 do you convert a program graph into a transition system?
- 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 do you convert a pseudocode process into a transition system?
What does the || operator mean?
How do you construct the parallel composition of 2 TSes?
How do you check whether a TS satisfies mutual exclusion?
How do you check whether a TS ensures no individual is ever starved (starvation freedom)?
What is a safety property?
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.
What is a liveness property?
Liveness properties are about "something good will eventually happen".
What is the difference between a safety and liveness property?
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 do you define a safety property for a TS in LTL?
say always not ( bad thing ), i.e. !  (bad condition)
How do you implement mutual exclusion as an LTL property?
☐(¬crit1 ∨ ¬crit2)
never true that both processes are in their critical sections
How do you implement starvation freedom as a LTL property?
(☐◇wait1→ ☐◇crit1) ⋀ (☐◇wait2→ ☐◇crit2)
every waiting process will eventually enter its critical section, i.e. starvation freedom
What kind of property does mutual exclusion represent?
How do you find a LTL formula that is or is not satisfied by a path in a given TS?
How do you find the reachable part of a TS?
How do you find the reachable part of a TS that is the result of a composition operation on two program graphs?
How do you find and describe an execution that proves that an entire TS is infinite?
How do you find whether an algorithm satisfies mutual exclusion?
How do you find whether two processes ever enter deadlock?
How do you find whether two processes ever begin to mutually wait on each other?
How do you find whether a process that wants to enter its critical section has to wait forever?
How do you formally define a TS?
How do you formally define a TS to model a real-world system?
How do you find the number of reachabke states in a TS?
What is invalid behaviour in a TS?
How do you find whether a TS defines invalid behaviour over all possible executions?
What is the handshaking composition operator?
How does the handshaking composition operator work?