Definition 1.2.9: for state s of an _ -NTS, _-closure(s) is a set of states defined inductively:
(i) s_ _-closure(s),
(ii) if t_ _-closure(s) and u___(t, _), then u_ _-closure(s),
(iii) nothing belongs to the _-closure(s) unless it follows from finitely many applications of (i) and (ii).
Also, for a set of states T, _-closure(T) = _s__T _-closure(s).
The behavior produced by multiple consecutive _-moves of an _ -NTS is the first thing we capture in our analysis.
| Previous slide | Next slide | Back to first slide | View graphic version |