表題番号：2007B-127 日付：2008/04/11
研究課題ハイブリッド制約モデリング言語の高信頼実装技術
研究者所属（当時） 資格 氏名
（代表者） 理工学術院 教授 上田　和紀
（連携研究者） 理工学術院 助手 石井　大輔
研究成果概要
ハイブリッド制約モデリング言語とは，時間の経過に伴って状態が連続変化し
たり，状態や方程式系自体が離散変化したりするハイブリッドシステムを，制
約 (constraints) 概念に基づいて記述・シミュレーション・検証するための
高水準言語である．1990年代に先駆となる言語 Hybrid CC が提案実装されて
いたが，言語機能と実行結果の信頼性の両面で研究の進展が待たれていた．

本研究は，新たなハイブリッド制約モデリング言語 Hydra の確立に向けて，
その設計論と，計算結果の正しさを保証する高信頼実装の要素技術を開拓する
ことを目標に実施した．本年度の成果は以下のようにまとめることができる．

1. 既存のハイブリッド制約言語である Hybrid CC の記述実験および検討を通
じて，Hydra が備えるべき機能，特に記号的離散状態の表現について踏み
込んだ検討を行った．

2. 高信頼実装のためには，求解過程において離散的に切り替わる方程式系の
区間演算技術が必須となる．区間演算においては，離散変化条件の成否が
一般に非決定的となるため，成否が決定的になるような小区間への分割を
行いつつ区間演算を進めるアルゴリズムを提案し，その有効性を確認した．

3. ハイブリッドシステムにおける重要かつ厄介な性質として，有限時間内に
無限回の離散的状態変化を起こす Zeno 挙動がある．そこで，与えられた
システムがZeno 挙動をもつかどうかの自動検証手法を開発した．Zeno 挙
動に関する推論は数値計算では困難であり，数式処理と限定記号除去によ
る解析方式を提案してその有効性を確認した．

4. ハイブリッドシステムの検証に伝統的に使われてきたハイブリッドオート
マトンとハイブリッド制約モデリング言語との関係づけのために、ハイブ
リッド制約プログラムからハイブリッドオートマトンへの自動変換技法を
開発して実装した．

5. 既存の制約ソルバ，区間演算，多倍長演算ライブラリを高信頼実装の部品
として活用するための調査・実験・準備を行った．区間演算を用いた常微
分方程式ソルバVNODE-LPに多倍長演算を組込み，求解精度向上における有
効性を多数の例題で調査するとともに，非線形制約求解系Elisaを用いた幾
何モデリングにおける制約不足の問題に対処するためのパターン分割手法
を提案・実験した．