[English]
アリやハチの群れや人間社会の営みを観察していると，各々が自分の意思で勝手に行動しているにも関わらず，全体として秩序や均衡が生み出される様子に驚かされます。このように，自ら状況を判断し意思決定する複数の主体（エージェント）が，互いに影響を及ぼし合いながら全体としてある目的を達成するシステムをマルチエージェントシステムと呼びます。工学的観点からは，中央集中制御によらない自律分散型のシステムもまたマルチエージェントシステムの一種と考えることができます。
当研究室では，広い意味でのマルチエージェントシステムを対象に，個々のエージェントの振る舞いから秩序や均衡が創発されるメカニズムの解明と，その工学的応用について研究しています。とりわけ，数理論理学（形式手法），ゲーム理論，分散アルゴリズム，進化計算などの様々な理論や手法をもとにした分野横断的な研究に特色があります。現在取り組んでいる主なテーマとしては，以下のものが挙げられます。
1970年代初めにゴシップ問題と呼ばれる問題が議論されました。これは，集団において各人が持つ秘密の情報を電話で（一対一のコミュニケーションで）交換するとき，全員が全員の秘密を知っている状態になるには何回の通話が必要かという問題です。この問題はその後，電話番号を知らないと通話ができないと仮定した上で，通話の際に秘密だけでなく既知の電話番号の情報も交換するダイナミックゴシップや，各人の知識状態によって通話の相手を決める認識論的ゴシップなどが提起されました。
このような状況において，もしも嘘つき（敵対的エージェント）がいて，ある人に対しては「自分の秘密は0である」と言う一方で別の人には「自分の秘密は1である」と言っているとします。このとき，他の正直な人たちは自分が聞いた情報だけから誰が嘘つきかを特定することができるでしょうか。あるいは，この嘘つきに気づかれないようにして正直な人たちだけで互いの情報を集めることにより，誰が嘘つきであるのかを共有知識とすることができるでしょうか。
こうした問題は，ゴシップ問題に限らず，集団におけるデマの拡散や分散システムにおけるビザンチン故障をしたノードの特定など，多くの場面に共通して現れる問題です。私たちは，認識論理（Epistemic Logic）を用いてこの問題を定式化し分析する方法について研究しています。
近年，特徴的なプレイスタイルによってビデオゲームやボードゲームをプレイするエージェントの研究開発が行われています。これらの研究の多くは，あらかじめ特定のプレイスタイルを想定した上で，それに合わせて定義された報酬関数を用いてエージェントに学習させるという方法が採用されてきました。しかしながら，このような方法では未知のプレイスタイルを発見することが困難です。 私たちは，進化計算を基に，事前に想定することなく同時に複数のプレイスタイルを自動生成するためのフレームワークの構築を目指して研究しています。具体的には，ゲームをプレイする際の特徴的な行動を遺伝子によって表現し，エージェント同士を互いに戦わせて生き残ったもの同士を交配させることにより世代交代を繰り返します。これによって得られた適応度の高いエージェントの特徴をクラスタリングを用いて抽出することにより，最終的に，ゲームに適応したプレイスタイルを特定することができます。
以上の枠組みを用いて，私たちは複雑な戦略が求められる多人数ゲームを対象に，生成された多様なプレイスタイルがゲームの進行に与える影響やプレイスタイル間の相性などを分析しています。さらに，以上で得られた成果の応用として，集団の多様性がパレート最適性などの全体の効用に与える影響を明らかにすることを目指して研究を行っています。
この他にも，私たちは様々なボードゲームやカードゲームを対象に，強化学習やゲーム理論，論理推論などをもとに上手にゲームをプレイするエージェントの研究開発に取り組んでいます。
社会の人々が持つ意見の推移を数理モデルにより分析する世論形成の研究がこれまで数多く行なわれてきました。先行研究の多くは，各人（エージェント）があるトピックに対して持つ賛成・反対の意見を数値で表し，世論の形成を近隣のエージェント同士の意見の同調の過程によってモデル化しています。しかしながら，現実には我々は周囲からの意見の表明だけを頼りに自らの意見を決めるのではなく，周囲や環境から得た知識をもとに意見を決めていると考えられます。こうした知識の果たす役割を捉えるために，私たちは数理論理学によるエージェントの知識表現を取り入れた世論形成モデルの構築を目的に研究を行っています。これにより，知識と意見が相互に影響を及ぼし合いながら世論を形成する過程を明らかにすることを目指しています。特に，誤った情報の伝播と世論形成との関係に焦点を当て，陰謀論者による極端な政治的主張の出現やエコーチェンバーによる世論の分断といった，近年SNSにおいて観察される現象の解明を試みています。
論理学の応用の一分野に，形式手法（formal methods，数理的技法）があります。これは，ソフトウェアの仕様がプログラマの意図した通りに書かれているかどうかを，数学的に厳密な方法で検証するための方法です。形式手法には，大きく分けて証明論的なアプローチによるもの（定理証明）と意味論的なアプローチによるもの（モデル検査）の2つがあります。
当研究室では，定理証明やモデル検査をもとに，ネットワークシステムや自律型の交通システムなど，さまざまなシステムの安全性やセキュリティの検証法について研究しています。また，形式手法を応用したシステムのスケジューリング手法についても研究しています。
また，形式手法による検証以外にも，自律分散システムに関するさまざまな研究を行っています。その主なものとしては，ゲーム理論を用いた省電力ストレージや耐障害性を持つ分散制約最適化アルゴリズムなどの研究開発が挙げられます。