アリやハチなどの社会性昆虫の営みや人々の経済活動などを観察していると，各々が自身の意思で勝手に行動しているように見えながらも，全体としてある秩序や均衡が生み出される様子に驚かされます．このように，自律的に意思決定する複数の主体（エージェント）が互いに影響を及ぼし合いながら全体としてある目的を達成するシステムは，しばしばマルチエージェントシステムと呼ばれます．工学的観点からは，中央集中制御によらない自律分散システムもまたマルチエージェントシステムの一種と考えることができます．
当研究室では，広い意味でのマルチエージェントシステム（または自律分散システム）を対象に，エージェントの振る舞いとそこから創発される全体性との関係の解明を，数理論理学やゲーム理論，マルチエージェントスケジューリング，強化学習などを用いて行います．また，それによって得られた知見をもとに，自律分散型のコンピュータシステムの研究開発を行います．現在取り組んでいる主なテーマとしては，以下のものが挙げられます．
今日のSNSをはじめとする大規模なインターネットサービスを実現するために，その基盤システムには高いスケーラビリティや運用コストの削減，高信頼性などが求められます．このような要求を満たすシステムを構築する際，中央集中型の制御では，しばしば中央コントローラがボトルネックや単一障害点となることがあります．こうした問題を解決するためのアプローチの一つが，自律分散型の制御です．
当研究室で研究開発を進めている自律分散システムに，ゲーム理論を用いた大規模分散省電力ストレージがあります．これは，システム全体の負荷に応じてディスク間でデータを移動させることにより，一部のディスクに負荷を集約して残りのディスクを省電力モードに移行させるというものです．このデータの移動の制御は，「利己的に振る舞う自律的なディスク間でのゲーム」として定式化することで実現されます．またこの他にも，自己安定アルゴリズムを用いたインターネットサービスの可用性向上などをテーマとした研究も行っています．
論理学の応用の一分野に，形式手法（formal methods，数理的技法）と呼ばれるものがあります．これは，ソフトウェアの仕様がプログラマの意図した通りに書かれているかどうかを，数学的に厳密な方法で検証するための方法です．形式手法には，大きく分けて証明論的なアプローチによるもの（しばしば定理証明と呼ばれるもの）と意味論的なアプローチによるもの（しばしばモデル検査と呼ばれるもの）の2つがあります．
当研究室では，定理証明やモデル検査をもとに，交通システムの運行スケジュールにおけるデッドロック検出やセキュリティプロトコルの安全性検証など，さまざまなシステムを対象とした検証法について研究しています．
複数の車両を協調動作させて旅客や荷物を配送するシステムを対象としたスケジューリングに関する研究を行っています．具体的には，自動車を非接触型インターフェースにより隊列走行可能とした新しい公共交通システムを対象に，旅客の待ち時間や走行コストの観点からの運行スケジュールの最適化手法の開発に取り組んでいます．
また，多数のドローンを用いた配送システムを対象に，衝突の危険を回避しつつ最も効率の良い配送経路を決定する手法の開発を，モデル検査をもとに行っています．
ゲーム理論における均衡概念を，数理論理学により分析する手法について研究しています．ゲーム理論は，プレイヤーと呼ばれる複数の主体が，それぞれの行動が影響し合う状況（ゲーム）の中で，自らの利益に基づき相手の行動を予測して意思決定を行うための理論です．この研究分野での中心的な課題は，すべてのプレイヤーが最適な行動を選択する状態（すなわち均衡状態）がどのようにして実現されるのかを解明することです．
当研究室では，数理論理学の分野で確立された認識論理（Epistemic logic）を用いて，各プレイヤーがゲーム論的状況においてどのような知識を獲得し，またその知識をもとにどのような推論を行うことによって最適な行動を選択するのかを分析する手法について研究しています．