微分制約論理式によるハイブリッドシステムのモデリングと検証
スポンサーリンク
概要
- 論文の詳細を見る
本研究ではハイブリッドシステムの到達可能性検証のための有界モデル検査法(bounded model checking)を提案する.提案手法では,非線形ハイブリッドオートマトンを常微分方程式およびガード制約を埋め込んだ論理式として,モデル中の危険領域を示す論理式とともに記述する.上記論理式の充足可能性をSAT求解系と数式処理系(Mathematica)を連携させた探索により示し,モデル中の不具合を発見することができる.
- 2009-01-22
著者
関連論文
- 特集「インタラクティブシステムとソフトウェア」の編集にあたって
- 並列計算機システムFOLON上へのPVMの移植と評価
- 階層グラフ書換え言語における並行プロセスの型推論
- 双対モデリングを用いた充足可能性問題のCNF encoding
- 微分制約論理式によるハイブリッドシステムのモデリングと検証
- なぜソフトウェア論文を書くのは難しい(と感じる)のか
- 特集「ソフトウェア論文」の編集にあたって
- 3A-1 大規模メモリ環境下におけるモデル検査ツールSpinのマルチコア検証機能の性能評価(高性能計算,一般セッション,アーキテクチャ)
- 3A-2 強連結成分ベースのグラフ分割による分散並列LTLモデル検査の高速化(高性能計算,一般セッション,アーキテクチャ)
- 6ZJ-9 階層グラフ書換え言語LMNtalによるモデル検査(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4K-2 分散検証環境DiVinEを用いた分散LTLモデル検査アルゴリズムの性能評価(情報爆発時代における分散処理とセキュリティ,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 6ZJ-7 並列SATソルバにおけるlemma共有およびプール制約伝播高速化(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- SATソルバ MiniSat の並列化とそのチューニング手法(HPC-2 : 数値解析I)
- HiRise : GUI構築のためのインクリメンタルな制約解消系(特集・インタラクティブソフトウェア)
- A-022 数式処理システムMathematica上における再帰除去システム(A分野:モデル・アルゴリズム・プログラミング)
- プロファイルを使用した並列LTLモデル検査のチューニング
- ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
- A-007 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化(モデル・アルゴリズム・プログラミング,一般論文)
- ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
- LMNtalモデル検査器における状態爆発対策(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- 強連結成分の特性を用いた並列モデル検査アルゴリズムSCC-OWCTYの設計と評価(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- ソフトウェア論文座談会
- 階層グラフ書換え言語LMNtalの処理系(ソフトウェア論文)
- LMNtal処理系および他言語インタフェースの設計と実装
- 制約に基づく解析による並行論理プログラムの自動デバッグ
- 特集「インタラクティブシステムとソフトウェア」の編集にあたって
- 6K-4 LMNtal処理系SLIMのモデル検査機能の並列化(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
- 6K-2 クラスタ向け並列precosatの開発と性能評価(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
- 1M-1 ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 論理・制約プログラミングと並行計算(論理と推論技術の展開)
- 特集「論理と推論技術の展開」の編集にあたって
- 6ZJ-8 軽量なLMNtal実行時処理系SLIMの設計と実装(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4N-2 KLICへのデータ並列処理機能の導入について
- 3K-2 汎用並列組合せ最適化パッケージの構想
- C. A. R. Hoare : Communicating Sequential Processes(20世紀の名著名論)
- シンガポール国立大学
- 私はCrusoeを使いたい(インタラクティブ・エッセイ)
- 視覚化に適した制約階層の拡張法
- A-014 LMNtalコンパイラにおける並び替えとグループ化を用いた命令列の最適化(A分野:モデル・アルゴリズム・プログラミング)
- 並列計算機システムFOLONの通信ライブラリの設計と評価
- 見込み計算を用いたニュースリーダの応答性改善法
- 10. 21世紀COEプロジェクト「プロダクティブICTアカデミア」(21世紀卓越した情報研究拠点プログラムの目指す研究(前編))
- 21世紀COEプロジェクト「プロダクティブICTアカデミア」
- 4T-7 WWW全文検索システムVernoのアーキテクチャ
- 4T-6 WWW全文検索システムVernoのデータベース
- 分散型WWW全文収集ロボットIron33
- 学習型WWW検索エンジンVerno
- LA_003 後継関数を持つリスト型非線形再帰プログラムに対する再帰除去法(A分野:モデル・アルゴリズム・プログラミング)
- 制約プログラミングに関する日本・フランス間の研究交流
- E-026 JPドメインにおける茶筌を用いた中国語ページの抽出(E分野:自然言語)
- B-030 キャッシュヒント自動付加を用いたソフトウェア高速化(B分野:ソフトウェア)
- LA-003 LMNtal処理系におけるグラフ構造の操作機能の設計と実装(A分野:モデル・アルゴリズム・プログラミング)
- SATソルバzchaffのMPIによる並列化(HPC-1 : 並列プログラミング)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- 言語モデルLMNtal
- 萩谷昌己,横森 貴共編 : DNAコンピュータ,培風館(2001)
- J. A. Robinson : A Machine-Oriented Logic Based on the Resolution Principle(20世紀の名著名論)
- インタフェースに基づく並行論理プログラム最適化コンパイラの構成法
- 人工知能とソフトウェア文化
- 並列KLIC処理系上での配列演算の最適化
- 並行論理プログラムのプログラム空間に関する考察
- 並行論理型言語における同期ポイント移動の安全性について
- 自己調整二分木の並列操作
- 4N-4 並行論理プログラム静的解析系Kimaの実装
- 3N-2 オブジェクト共有空間を利用した分散プログラミング支援フレームワーク
- 並行論理プログラムの参照数解析
- WISS '96会議報告
- 数値最適化による力学的グラフ可視化手法
- ユーザインタフェースのための線形制約解消系
- 静的解析と制約充足によるプログラム自動デバッグ
- 高次元アプローチによる一般無向グラフの対話的視覚化法(情報可視化, インタラクション: 技術と展開)
- 対話型インターフェースのための幾何制約解消の枠組み次世代インタラクションのための情報技術
- 基数制約に対応するクラスタ向け並列SATソルバとその評価(高信頼設計,2011年並列/分散/協調処理に関する『鹿児島』サマー・ワークショップ(SWoPP鹿児島2011))
- 日本ソフトウェア科学会第27回大会報告
- 対話型3次元アプリケーションのための幾何制約解消法(ユーザインタフェースとインタラクティブシステム)(コラボレーションアートとネットワークエンターテイメント)
- ユーザインタフェースのための線形等式・不等式制約解消系(ソフトウェアシステム)
- ユーザーインターフェースにおける制約解消法の研究動向
- GUIを対象とした線形計算による制約階層解消系の高速化
- 1ZA-8 GUI構築のための数値的な制約階層解消系の機能的改良(UI開発支援,一般講演,インタフェース)
- 理論と実際のギャップ : 並列プログラミング (<特別論説> 情報処理最前線)
- Moded Flat GHCのモード体系
- LMNtal並列モデル検査における状態生成数削減及び高速化