概要：　形式的モデル化の理論と応用　−複雑なシステムを理解する−

本研究室では，複雑な実世界の対象をどのように数学的に取り扱える形でモデル化するかについての研究を行っています． 特に，イベントの発生により状態遷移が発生する離散事象システム，微分方程式で記述される連続システムがイベントの発生により 切り替わるハイブリッドシステムを主な研究対象としています．さらに，これかのモデル化手法を情報システム，サービスシステム， 制御システム，システムズバイオロジーなど様々な領域の問題に提要しています．
（overview.pdf）．


システムの形式的モデル化でできること

１．高信頼化
実際に動作させる前に，設計されたシステムが正しい動作を行うことを理論的に検証できます．また，正しくない場合には修正すべき箇所に関する情報を提供してくれます．シミュレーションやテストと異なり，すべての場合を網羅的に検査できます．

２．高性能化
システムの性能に影響を与えるさまざまなパラメータを最適なものにチューニングすることができます．また，確率的に与えられた入力に対するシステムの性能を評価することができます．

３．設計自動化
与えられた動作仕様を満たすようなシステムを自動的に合成することができます．さらに，動作仕様が実現不可能である場合には，実現可能な仕様の候補を提示してくれます．

４．システム推定
詳細が未知のシステムを観測データから推定することができます．

関連分野
本研究室で行う研究は，様々な分野の境界領域に位置しています．過去に発表した論文の分野は，理論計算機科学，ソフトウェア科学，論理学，システム科学，制御工学，人工知能，オペレーションズリサーチ，意思決定支援，研究技術開発マネージメントなど多岐に渡っています．

修了者の主な就職先
三菱自動車，アイシン精機，デンソー，YKK,　日立アプライアンス，島精機，三菱電機，日野自動車，オリンパス，住友電工情報システム，三洋電機，沖ソフトウェア，NEC, 日本IBM

最近の研究から

１．フォーマルアプローチによるシステムの設計，検証，制御

形式検証技術を既存の制御理論と組み合わせることで，論理的制御仕様を満たし，かつ，評価関数を最適化するような 制御入力を求めることができます．図は２台の車の走行の様子を表したもので，たとえば，論理的制御仕様として 「少なくとも３秒毎に0.5m以内に接近する」が与えられたとき，消費するエネルギーを最小にする制御入力を求めるこ とが目的となります．この問題は，双模倣関係に基づく離散抽象化とモデル予測制御の手法により解くことができます．

1) 実時間／ハイブリッドシステムのモデルベース開発に対する形式手法の適用
　　　　（sice208ws.pdf）

2) 離散ダイナミクスに着目したハイブリッドシステム制御論の構築
　　　　（ACA2008.pdf）

3) 連続ダイナミクスの流体化による安全性検証
　　　　（ATPN08.pdf）

4) ハイブリッドシステムのBox Abstraction
　　　　（sig_des2010.pdf）

２．サービス現場におけるスタッフのふるまいのモデル化

「音声つぶやきシステム」と呼ばれる特殊なコミュニケーションデバイスを用いて看護・介護業務をサポートする 研究開発プロジェクトに参加しています．その中で，デバイスにより収集された作業スタッフの位置情報から 各スタッフのふるまいモデルを学習し，スタッフ間の行動の差異や，要注意行動の検出などを行っています． また，人間の行動やデバイスの効果に関する様々な仮説を検証するために，実際の現場を模した環境上で， 特定の状況設定において繰り返し実験を行う仮想フィールド実験を実施しています．(URL:http://www.jaist.ac.jp/ks/mot/JSTservice/)

1) 行動型サービスにおける行動モデリング
　　　　（cogsima2014.pdf）

2) スタッフの要注意行動の検出
　　　　（wodes2014.pdf）

3) 離散事象シミュレーション
　　　　（simulation.avi）

4) 時空間状況認識
　　　　（SMC2019.pdf）

３．データサイエンスアプローチによる離散事象システムの故障診断

離散事象システムの故障診断は，従来はシステムの正確なモデルを必要とするモデルベース故障診断が主流であった． これに対し本研究では，モデル自体をシステムの動作履歴から学習し，正常時のモデルと異常時のモデルの差異を 数値化することにより故障診断を行う，データサイエンスのアプローチを提案している．

　　　（danms2013.pdf）

4．航空オープンデータを用いた空域交通流のモデル化

国土交通省航空局は日本上空における民間航空機位置の時系列データ（CARATSオープンデータ）を公開している．本研究ではこのデータを用いることにより，(1) 空域における交通流のダイナミクスを表現する数理モデルの構築を行う．空域は航空管制の単位であるセクターという領域に分割されており，セクター内の航空機数を容量以下に抑えることが航空管制において求められる．数理モデルを用いることで，(2) 近い将来（数分〜数十分後）における空域交通量の予測方法を開発し，さらに，(3) 航空管制官による指示，具体的には離陸時刻の遅延や巡航速度の制限，を用いたセクター内航空機数の制御方式を開発する

　　　（CARATS.pdf） （CARATSposter.pdf）

5．その他の応用領域

1) クラウドシステムの運用管理
Shinji Kikuchi, Kunihiko Hiraishi: Improving Reliability in Management of Cloud Computing Infrastructure by Formal Methods, IEEE/IFIP Network Operations and Management Symposium(NOMS) 2014, (2014/5/5-9, Krakow, Poland)

2) ビジネスプロセスの検証
Kenji Watahiki, Fuyuki Ishikawa, Kunihiko Hiraishi: Formal Verification of Business Processes with Temporal and Resource Constraints, 2011 IEEE International Conference on Systems, Man, and Cybernetics, pp.1173-1180 (2011/10/9-12, Anchorage, Alaska)

3) コンピューテーショナルバイオロジー
Koichi Kobayashi and Kunihiko Hiraishi: ILP/SMT-Based Method for Design of Boolean Networks Based on Singleton Attractors, IEEE/ACM Transactions on Computational Biology and Bioinformatics, Issue No.6, pp.1253-1259 (2014)

4) 空港面モデリングとシミュレーション
Kenji Uehara, Kunihiko Hiraishi and Koichi Kobayashi: Modeling of Traffic Congestion on Airport Surface using Petri Net, IEICE Technical Report, MSS2014-54, pp.17-22 (2014)