CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 10: 確率モデル検査による1次元イジングモデルの検証


実施年度2006, 2007, 2008
概要 自然界や情報科学における確率的な振る舞いを示す系は,確率モデル検査の検証 対象と成りうる. 近年,自然科学と情報科学の境界領域の解析に確率モデル検査が適用され始めて いる. 本研究では,磁性体の簡易なモデルであるイジングモデルに確率モデル検査を適 用し, 従来コンピュータシミュレーションで扱われている物理量に関して 確率モデル検査による解析が可能であることを示した.
担当者 関澤 俊弦,高橋 孝一
班名 抽象化ツール研究開発班
寄与 土屋達弘 (大阪大学),菊野亨 (大阪大学 )
関連する事例

題材

領域 量子スピン系 (電子物性物理)
題材の詳細
1次元イジングモデル
形態 反強磁性体,外部磁場なし
言語
規模 スピン数 10
題材の情報源 物性物理や量子スピン系の教科書に載っています (原典は 1924年の Ernst Ising の PhD論文 (ただしドイツ語).)

検証のデータ

目的
物理現象の解析
検証内容
平衡状態への到達可能性,
平衡状態近傍に留まる確率,
平衡状態から励起する確率,
平衡状態から励起しある磁化に到達するまでの遷移時間
結果
上記検証内容を記述し,検証可能であることを示した.
検証手法 モデル検査
モデル化法 半自動 (モデル生成プログラムを作成)
使用ツール PRISM 3.0
スケジュール、
労力、時間など
不明
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
検討中
論文発表 Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi: "Analyzing the One Dimensional Ising Model by Probabilistic Model Checking", Proceedings of The IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007), (Beijing, China). Acta Press, 199-204.
Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Koichi Takahashi, and Tohru Kikuno: "Probabilistic Model Checking of the One-Dimensional Ising Model", The IEICE Transactions on Information and Systems, Special Section on Formal Approach, Vol.E92-D, No.5, 1003-1011, May 2009.
口頭発表 Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi: "Analyzing the One Dimensional Ising Model by Probabilistic Model Checking", The IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007), (Beijing, China), 2007/10/10
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.