理論情報科学領域【平石研究室】
■ 研究概要
本研究室では，複雑な現実の対象をどのように数学的に取り扱える形でモデル化するかについての研究を行っています。特に，複数の構成要素が同時進行的に動作するコンカレントシステム，および，微分方程式で記述される連続システムがイベントの発生により離散的に切り替わるハイブリッドシステムの研究を行っています。
■ システムの形式的モデル化でできること
１．高信頼化
実際に動作させる前に，設計されたシステムが正しい動作を行うことを理論的に検証できます。また，正しくない場合にはどこを直せばよいのかを発見してくれます。シミュレーションやテストと異なり，すべての場合を網羅的に検査できます。
２．高性能化
システムの性能に影響を与えるさまざまなパラメータを最適なものにチューニングすることができます。また，確率的に与えられた入力に対するシステムの性能を評価することができます。
３．設計自動化
与えられた動作仕様を満たすようなシステムを自動的に合成することができます。さらに，動作仕様が実現不可能である場合には，実現可能な仕様の候補を提示してくれます。
４．システム推定
詳細が未知のシステムを観測データから推定することができます。
■ 関連分野
本研究室で行う研究は，様々な分野の境界領域に位置しています。過去に発表した論文の分野は，理論計算機科学，ソフトウェア科学，論理学，システム科学，制御工学，人工知能，オペレーションズリサーチ，意思決定支援，研究技術開発マネージメントなど多岐に渡っています。
■ 最近の研究から
１．記号的計算によるハイブリッドシステムの解析
ハイブリッドオートマトンは微分方程式がイベントの発生によりどのように切り替わっていくかをオートマトンの形で表現したものです。図はタンクの水面レベルを制御するシステムをハイブリッドオートマトンで表現したものです。その解析には，連続状態の集合を数式の形で扱える記号的計算が有効です。
ハイブリッドオートマトン |
２．遺伝子依存関係の推定とシミュレーション
生物細胞内での反応は遺伝子の発現によるたんぱく質の合成が基本となっています。ある遺伝子の発現が別の遺伝子の発現を制御するという連鎖が存在し，それにより細胞内の状態は動的に変化していきます。これをハイブリッドシステムとしてモデル化し，遺伝子制御領域における配列の類似性，および，DNAマイクロアレイ技術を用いた発現に関する実験データを用いてシステムの推定を行っています。また，それに基づきシミュレーションを行います。
遺伝子依存関係 |
■代表的な著書・論文
- Sunseong Choe, Kunihiko Hiraishi : Application of Quantifier
Elimination to Optimal Control Problems of Hybrid Systems,
Proc. 7th Asian Symposium on Computer Mathematics, 62-65, 2005
- Kunihiko Hiraishi, Sunseong Choe : Coputational Tools for
Designing Hybrid Systems Based on Constraint Satisfaction,
Proc. Workshop on Control of Hybrid and Discrete Event Systems,
Satellite workshop of ATPN2005, 41-60, 2005
- Kunihiko Hiraishi : Deriving Discrete Behavior of Hybrid
Systems under Incomplete Knowledge, IEICE Trans. Fundamentals,
Vol. E87-A. No.11, 2913-2918, 2004
