今日も，たまにはまじめにお仕事の話．

今日からFM 2009の本会議．細かい話は書きませんが，さすがに面白い話ばかり．


夜はTuring Award 2007（コンピュータの世界のノーベル賞みたいな）のE. Allen Emerson氏の講演．もちろん1980年代の彼らのModel Checkingに関する取り組みを振り返って，という話．Temporal Logicの導入について．そしてLTLのモデル検査の，オートマトン積Non-Emptyness判定問題への還元について．数百名の参加者の誰もが当たり前のように知っている話．だからこそすごい．

Computer Scienceに関わっていない人でも，IntelプロセッサなりIEEEプロトコルなりを通して，何らかの恩恵は受けているのではないでしょうか．

Emerson氏はそれなりにご高齢なわけですが，「テキサスからはるばる来て，乗ったタクシーの運転手がオランダ語しか話せなかったショックで声が出なくなってしまった」そうです．確かに最初はガラガラ声でしたが，のってきたら全く問題ないように見えました．そういった方でも1.5Lペットボトルのコーラを持ち歩いてがぶがぶ飲んでいるのがアメリカらしいというか何というか．


続いては若手のやり手，Joost-Pieter Katoen氏によるモデル検査はどこにでも（ubiquitous），という話．エンザイムの化学反応系の確率計算や，「複数電池のどれをいつ充電するのが最もライフタイムを長くするか」という最適化を，モデル検査で解くという話．後者の話なんかは，自分のところの学生さんなんかも関係ある話ですが，複雑な電池の消費・充電モデルを扱い，そしてまさかのUPPAALによる解法．


やっぱりComputer Scienceは面白いなぁと実感．ちなみに自分はComputer Science出身ですが，もっとComputer Scienceをきちんとやってくればよかったという後悔というか引け目があります．もちろんこれからの方向性は考えていて，まぁそれは書いてみるよりも実行ですね．


ちなみにFM 2011は2011年6月（FMは1年半ごと）．アイルランド，つまりLEROです．今回はサブイベントで計3件発表ですが，次回はもっとインパクトのあることを持ってこなければですね．