Flashcards in Lectures 10 and 11: 5th November 2019 Deck (74)
What is a TS?
What is a PG?
What is an arbtier?
How can you implement mutual exclusion with an arbiter?
What is a semaphore?
How can you implement mutual exclusion with a semaphore?
How do you compose multiple PGs together?
How do you interleave multiple PGs together?
How do you find the reachable part of a TS?
When does a state satisfy a property?
When does a TS satisfy a property?
What is the difference between unconditional, strong, and weak fairness?
Unconditional = Every process gets its turn infinitely often.”
Strong = “Every process that is enabled infinitely often gets its turn infinitely often.”
Weak = “Every process that is continuously enabled from a certain time instant onwards gets its turn infinitely often.”
How can you formulate unconditional, strong, and weak fairness in LTL?
Unconditional = ufair = ☐◇criti
Strong = sfair = ☐◇waiti → ☐◇criti
Weak = wfair = ◇☐waiti → ☐◇criti
How can you formulate strong fairness in a TS of two composed PGs implementing mutual exclusion?
What is a linear logic?
What are the implications of LTL being a linear logic?
What types of formulae are easy, hard, and impossible to express in LTL?
What are branching logics?
What are branching time logics?
What are the unfoldings of a model?
What is CTL?
What are the two types of CTL formulae?
What are CTL state formulae?
What are CTL path formulae?
What is the format of CTL state formulae?
What is the format of CTL path formulae?
How can you convert between state and path formulae/
How must temporal operators be formatted to be legal in a state formula?
What do ∃ and ∀ mean in state formulae?