Lectures 10 and 11: 5th November 2019 Flashcards
LTL fairness, CTL, async comms, timed automata
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?
!
How do you formulate a mutual exclusion property in CTL?
!
What are the equivalence laws of CTL?
!
When does a state satisfy a CTL state formula?
!
When does a path satisfy a CTL path formula?
!
What is the satisfaction set of a CTL state formula?
!
When are two CTL formulae equivalent?
!
Give the basic model checking algorithm for CTL formulae.
!
What are synchronous and asynchronous communications?
!
What are channel systems?
!
How do channel systems work in PROMELA?
!
What are communication actions in PROMELA?
!
How are communiation actions formatted in PROMELA?
!
What is the capacity of a channel?
!
How does handshaking work in PROMELA?
!
How do you find the capacity of a channel in PROMELA?
!
When can processes send and get messages into or from a channel?
!
What are channel systems?
!
What are channel systems used for in PROMELA?
!
What is alternating bit protocol?
!
How does ABP implement reliable comms over unreliable channels?
!
How does ABP work?
!
What are concurrent systems?
!
What are the differences between different concurrent systems?
!
What are timed automata?
!
How do timed automata work?
!
What is UPPAAL?
!
How does UPPAAL work?
!
What is TCTL?
!
How does TCTL work?
!
What are untimed models?
!
What are untimed actions?
!
How do untimed models work?
!
What are real-time constraints?
!
How can you implement timed models with and without using timed automata?
!
Is it easier to implement timed models with or without timed automata? Why?
!
Why is using a set of clocks acting as stopwatches a poor solution for implementing timed automata?
!
How do timed automata work, in detail?
!
What are clock constraints?
!
How do you mathematically define a timed automaton?
!
How are transitions in timed automata formatted?
!
What are location invariants in timed automata?
!
How do you implement location invariants in timed automata?
!
What is the difference between guards and location invariants in timed automata?
!
How do clocks work in timed automata?
!
How are clocks implemented in timed automata?
!
