|
Infinity Sets
Infinity Sets
- Number of states is finite, so an infinite trace visits some states infinitely often.
- These states are called the infinity set of a trace:
1. a, b, a, b, a, b, ... {a, b}2. a, b, a, c, c, c, c, ... {c}3. a, b, a, c, a, c, a, c ... {a, c}
- Fairness constraints are conditions on the infinity set.
- Finf {a, b} : “Infinitely often {a,b}” means some state in {a, b} must be in the infinity set.Satisfied by 1 and 3, but not 2.
d
c
|