>>505
> どんな性質を証明したいかによると思われ。

「うまく動かない」ということをなんとかして確認したいのですが...(^^;
具体的には想定外の入力が起きる条件を確定したいのです。
ほぼ動いているようにみえるのですがたまに通信で想定外の入力がきて
不具合がおきてしまう。でもなかなか状況を再現できないから、
いっそのこと全部形式的に書き下して条件を見つけてしまえればなぁ、と。
動機が不純ですかね (W

> 例えばTCPソケットの状態遷移に関しての到達可能性などならCTLを使えるし、

なるへそ、これはこれでおもしろそうです。TCPにCTLが使えるというのは何か
参考になる論文とかありますでしょうか?

> マルチスレッドでのデッドロックを検証したければpetri-netと
> reachability graphだろうし。

マルチスレッドのモデルってペトリネットが定番なんでしょうか?
普通のプロセス計算ではちょっと合わないと思ったので。

reachability graphとわ何でしょうか?

くれくれ君でスマソ。