文献

J-GLOBAL ID：201502205609878160   整理番号：15A0780932

リアクティブシステム仕様の外部環境制約式に関する研究

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

抄録/ポイント： 時相論理で記述されたリアクティブシステム仕様の満たすべき性質の一つに強充足可能性がある。これは「将来生起する環境からの入力が与えられたとき,いかなる入力に対しても仕様を満たす応答が存在する」という性質である。リアクティブシステムは環境に対して開いたシステムであるので,その仕様は環境からのすべての入力パターンを考慮する必要がある。そのため,強充足可能性はリアクティブシステム仕様の満たすべき重要な性質である。仕様が強充足不能であると判明した場合,仕様を修正する必要がある。このとき,仕様の欠陥情報を理解しやすい表現で得ることができれば,仕様を修正する助けとなる。そこで,本論文では強充足不能な仕様の外部環境制約式の導出手続きを提案する。外部環境制約式とは仕様を満たせない環境からの入力の集合を表す時相論理式である。本手続きでは,得られる制約式が単純で直感的な形を保つよう制約式の形を限定する。得られる制約式はその形において最も多くの欠陥情報を表現した式である。(著者抄録)

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

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

引用文献 (10件)：

• Abadi, M., Lamport, L., and Wolper, P.: Realizable and Unrealizable Specifications of Reactive Systems, in Proceedings of the 16th International Colloquium on Automata, Languages and Programing, pp. 1-17, (1989).
• Gastin, P. and Oddoux, D.: Fast LTL to Biichi Automata Translation, in Proc. of the 13th International Conference on Computer Aided Verification (CAV 2001), Lecture Notes in Computer Science, Vol.2102, pp.53-65, Springer (2001).
• Grädel, E., Thomas, W. and Wilke, T.(Eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, Vol.2500, Springer (2002).
• Mori, R. and Yonezaki, N.: Several Realizability Concepts in Reactive Objects, Information Modeling and Knowledge Bases, IOS Press (1993).
• Pnueli, A. and Rosner, R.: On the synthesis of a reactive module, in Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.179-190 (1989).

タイトルに関連する用語 (5件)： リアクティブシステム ,  仕様 ,  外部環境 ,  制約 ,  研究