变迁系统 transition system
transition system本质上就是带有标记的有向图。
Formally, a transition system is a pair (S, →) where S is a set of states and → is a relation of state transitions (i.e., a subset of S × S). A transition from state p to state q, i.e. (p, q) ∈ →, is written as p → q.
标记可以在节点、边上，或两者皆有。
A labelled transition system is a tuple (S, Λ, →) where S is a set of states, Λ is a set of labels and → is a relation of labelled transitions (i.e., a subset of S × Λ × S).
标记在节点上的transition system也就是 Kripke Structure。FA和 ω-automata 也可以认为是标记在边上的transition system，但是表达能力更高的自动机并不单纯是一张标记图。
有时，transition system也有初始状态集I。而所谓终止状态集F，即那些没有转移的状态（对任意label）的集合。