Help
Options
Didn't know it?
click below
click below
Knew it?
click below
click below
Don't Know
Remaining cards (0)
Know
retry
shuffle
restart
0:00
Embed Code - If you would like this activity on your web page, copy the script below and paste it into your web page.
Normal Size Small Size show me how
Normal Size Small Size show me how
jefe
| Question | Answer |
|---|---|
| LTL (Linear Temporal Logic) | A logic used to describe how a system behaves over time using infinite executions |
| Infinite Execution | An execution that never terminates and continues forever |
| Atomic Proposition | A boolean condition representing a system event (e.g. request, grant) |
| X φ (Next) | φ holds in the next state |
| F φ (Eventually) | φ will hold at some point in the future |
| G φ (Globally) | φ holds forever |
| φ U ψ (Until) | φ holds until ψ becomes true |
| Safety Property | A property stating that something bad never happens |
| Safety Violation | A violation that can be detected in finite time |
| Liveness Property | A property stating that something good will eventually happen |
| Liveness Violation | A violation that can only be detected in infinite time |
| Fairness | A condition ensuring that enabled processes are eventually executed |
| Starvation | When a process is continuously ignored despite being enabled |
| Weak Fairness | A fairness assumption where a continuously enabled process must eventually execute |
| Büchi Automaton | An automaton that operates on infinite executions |
| Accepting State | A state that must be visited infinitely often for acceptance |
| Büchi Acceptance Condition | An execution is accepted if an accepting state is visited infinitely often |
| Relationship between LTL and Büchi Automata | Every LTL formula can be translated into a Büchi automaton that accepts exactly the executions satisfying it |
| GF p | p occurs infinitely often |
| Meaning of GF p | p may be false sometimes but must occur again and again forever |
| FG p | Eventually p holds forever |
| Meaning of FG p | From some point onward p is always true and never becomes false |
| Difference between GF p and FG p | GF allows p to be false between occurrences, FG does not |
| Never Claim | A Promela construct representing the negation of an LTL property |
| Purpose of Never Claim | Used by SPIN to search for counterexamples |
| Accepting Cycle in Never Claim | Indicates a liveness violation |
| Synchronous Channel | A channel with zero buffer requiring send and receive to occur simultaneously |
| Syntax of Synchronous Channel | chan c = [0] of { ... } |
| Asynchronous Channel | A channel with a buffer allowing send and receive at different times |
| Syntax of Asynchronous Channel | chan c = [N] of { ... } where N > 0 |
| Deadlock | A situation where processes block forever waiting for each other |
| Synchronous Channels and Deadlock | Deadlocks occur easily if send and receive do not match |
| Asynchronous Channels and Deadlock | Fewer deadlocks due to buffering |
| Buffer | Waiting space in an asynchronous channel |
| Rendezvous | Simultaneous send and receive in synchronous channels |
| Liveness and Fairness Relationship | Liveness properties assume fairness |
| Unfair Execution | Execution where a process is continuously ignored by the scheduler |
Created by:
user-2021565