ωオートマトン(ω-automata)とは、簡単に言うと無限の状態遷移を扱うオートマトンです。Spinを勉強する上で、必要になることがありますので、簡単にまとめておきます。