Problem 3 A labeled transition system (LTS) M is a triple (S, A, where S is a set (finite or infinite) of states, A is a finite set of actions, and is a ternary relation over S x A x S. If the argument of is (si, a, 8 e S x A x S, we write "si si" instead of (si, a, s i) We assume that the states in S are indexed with a set I of natural numbers, i.e., S si i E I t. If S is finite with S n, then I is the initial segment 10, 1 nt of N; if S is infinite, then I N. If we write s si, we mean that the LTS M can make a transition from state si to state si when action a is applied. The set of next states from si with action a is defined by: next si, a 81 ESI si 8 If next(si, a) then M cannot make a transition from state si with action a. We write next (si) to denote UaeA next(si, a), which is the set of all next states from 8 Caution: The relation in M, which is called the transition relation of M, is unrelated to logical implication The symbol is overloaded (sorry!)