文献

J-GLOBAL ID：201502209080910270   整理番号：15A0780931

分解証明法を利用したリアクティブシステム仕様の強充足可能性判定器の提案

著者 (2件)： 中村風太 (埼玉大 大学院理工学研究科) ,  吉浦紀晃 (埼玉大 大学院理工学研究科)
資料名： 情報処理学会研究報告(Web)  (IPSJ Technical Report (Web))
巻： 2015  号： SE-187  ページ： VOL.2015-SE-187,NO.22 (WEB ONLY)  発行年： 2015年03月05日 
JST資料番号： U0451A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 時間論理により記述されたリアクティブシステム仕様の満たすべき性質の一つに強充足可能性がある。システム利用者からのいかなる要求列についても,それに対し仕様を満たすようなシステムのある応答列が存在するという性質である。仕様が強充足可能性を満たしているかを判定するためにモデルを利用した判定法が存在するが,二重指数の計算コストがかかり大きな仕様の判定に対してあまり有効ではない。そこで本論文では,モデルを利用しない判定法として,様相論理に対する分解証明法を利用した仕様の強充足可能性判定器の提案を行う。提案法の判定手続きを与え,提案法における健全性及び完全性を示す。(著者抄録)

シソーラス用語： *仕様 ,  要求仕様 ,  自然言語処理 ,  *検証 ,  性質 ,  オートマトン ,  時間論理 ,  線形性
準シソーラス用語： *リアクティブシステム仕様 ,  強充足可能性 ,  *設計仕様 ,  線形時間論理

分類 (2件)： 自然語処理  (JE06000L) ,  オートマトン理論  (JB04000O)

引用文献 (10件)：

• Daniel Jackson: "Automating first-order relational logic", Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of softwareenigineering, pp.130-139, 2000.
• 島川昌也,萩原茂樹,米崎直樹:"仕様の自動検証に適したLTLフラグメント",日本ソフトウェア科学学会第23回大会,2006.
• David Harel, Amir Pnueli: "On the development of reactive systems", K.R.Apt,editor,Logics and Models of Concurrent Systems, Volume F13 of NATO ASI Series, pp.477-498.springer-Verlag, 1985.
• Zohar Manna, Amir Pnueli: "the temporal logic of reactive and concurrent systems Specification", Springer-Verlag,New York, 1992.
• 森亮靖,米崎直樹:"時相論理によるリアクティブシステム仕様の実現可能性に関する分類",コンピュータソフトウェア,Vol.15,No.3 pp.17-24,1998.

タイトルに関連する用語 (6件)： 分解 ,  証明 ,  リアクティブシステム ,  仕様 ,  充足可能性 ,  提案