>>504
どんな性質を証明したいかによると思われ。
例えばTCPソケットの状態遷移に関しての到達可能性などならCTLを使えるし、
マルチスレッドでのデッドロックを検証したければpetri-netとreachability graphだろうし。