Discrete Time PA

MSCからProcess代数へのマッピングがしっくりこなくてAlureのイベント依存関係経由でPAにもってゆこうとしていたがどうもすっきりしない。
そこでdiscrete Timed PAなるものを読んでみることにした

http://citeseer.ist.psu.edu/341551.html

というのをみるとなるものがあるらしい、これは使えそうということで、大森ドトールで検討すると、たしかに大丈夫そうだ。うまく時間と時間の省略を関連づけられて、ごちゃごちゃするから以降の議論では、時間は無視することにするということができそう。

そうおもっていると、discrete timed PAにもいろいろ種類があって、前論文の著者VereijkenのD論では、なるものを使っている、こっちが最新かあ、まいった。

それにしてもVereijkenのD論のPrefaceは面白い。Beatenの指導で、discrete timed PAをやってみると、結構できて（前述paper）、つぎにハイブリッドPAに手を出したらそこでは、沈没し消沈し、また再びdiscrete timed PAに戻って、ある定理の証明を100ページもかかって、間違っていることを証明しそれがD論になったということだった。

まあ山あり谷ありということですね。