式を用いた性質検査およびハンズオンを行う。命題論理の拡張となっており、各論理式の真偽が状態に依存する。通常の意味で使用可能である。おいて、それぞれの意味は以下の通り。ここで不等号は状態遷移による時間的な前後関係を表す。式の頻出パターンも参照のこと。プロセスローカル変数の値を取得できる。用いて変数名を付けておく必要がある。ちなみにその際、変数名には何故か小文字しか使用できない。積オートマトンを検査する。オプションを与えればよい。オプションを指定すればよい。通知をモデル化することを考える。呼ばれる識別子で区別される。