次世代デジタル社会基盤研究領域の青木利晃教授とRIVIERE Peter Bernard特任助教が、12th International Conference on Rigorous State Based Methods（ABZ 2026）において、Best Paper Awardを受賞しました。

　ABZ 2026は、ASM、Alloy、B、TLA、VDM、Zなどの形式手法に関する主要な国際会議の一つであり、令和8年5月18日～20日にかけて東京で開催されました。
　同会議は、The 27th International Symposium on Formal Methods（FM 2026）と併催され、形式仕様、検証、モデリング、安全性保証などに関する最新の研究成果が発表されたほか、異なる形式手法を扱う研究コミュニティ間で知識や経験の活発な交流が行われました。
　Best Paper Awardは、ABZ 2026に投稿された論文の中から、独創性、技術的貢献、新規性、将来性などの観点で特に優れた研究に対して授与される賞です。

※参考：ABZ 2026

■受賞年月日
　令和8年5月20日

■研究題目、論文タイトル等
Encoding BDI Syntax with Theories in Event-B

■研究者、著者
Mengwei Xu (University of Newcastle), Peter Riviere, Toshiaki Aoki, Marie Farrell (The University of Manchester), Yamine Ait Ameur (IRIT/INPT-ENSEEIHT), Neeraj Singh (INPT-ENSEEIHT/IRIT, University of Toulouse, France), Guillaume Dupont (INPT-ENSEEIHT)

■受賞対象となった研究の内容
　本研究では、自律システムの設計で広く用いられているBDI（Belief-Desire-Intention）エージェントについて、その構造を形式手法Event-B上で忠実に表現する手法を提案した。Event-Bは、数学的、特に、集合論に基づいてシステムをモデル化し、安全性や正当性を検証するための形式手法である。
　従来、BDIエージェントの検証では、モデル検査器や定理証明器ごとに個別の実装や表現方法が必要であり、再利用や保守が難しいという課題があった。本研究では、Event-BのTheory機構を活用することで、BDIエージェントを本来の意味に沿ってコンパクトかつ再利用可能な形で表現できることを示した。さらに、完全な動作意味を与える前の段階でも、エージェントが持つ知識の整合性確認や、belief（信念）に基づく安全性検証が可能であることを示した。これにより、自律ロボットや自動運転システムに対する、形式手法を用いたAIシステム検証技術への応用可能性を示した。

■受賞にあたって一言
【青木教授】
　本研究は、日本、イギリス、フランスの研究者による国際共同研究として実施されたものであり、形式手法とAI・自律システムを橋渡しする基盤技術として国際的に評価されたことを大変嬉しく思います。本研究を通して得られた知見は、我々が推進しているJST CRESTプロジェクトの研究をさらに発展・加速していく上でも重要な成果になると考えています。今後も、自動運転システムや自律ロボットなど、実システムの高信頼化・高安全化に貢献できる研究を推進していきたいと考えています。

【RIVIERE特任助教】
In this context of international work with UK, France, and Japan. It is a pleasure to receive this award, and it will provide an excellent opportunity to strengthen the connection between the autonomous agents community and formal methods. We will use this award as an important result for the JST CREST and as an inspiration to improve verification capabilities and contribute to the development of a new generation of safe and verified complex systems for society.

令和8年7月2日