線形時相論理の為の効率的記号モデル検査方式

• Item type: SIG Technical Reports(1)
• 公開日: 1993-10-28
• タイトル: 線形時相論理の為の効率的記号モデル検査方式
• タイトル / 言語: en
• タイトル: Efficient model checking for Liner - time Temporal Logic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京工業大学情報工学科
• 著者所属: 東京工業大学情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Computer Science Tokyo Institute of Technology
• 著者所属(英): en
• 著者所属(英): Department of Computer Science Tokyo Institute of Technology
• 著者名: 中根, 清光; 米田, 友洋
• 著者名(英): Kiyomitsu, Nakane; Tomohiro, Yoneda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 設計されたシステムが与えられた仕様どおりに動作するかどうかを確かめる設計検証はシステムの大規模化、複雑化により重要な役割を担うようになっている。一方、検証対象システムが大きくなると検証に要する計算量が急激に増加するという、いわゆる状態爆発という問題がある。この問題を解決する一つの方法として二分決定木(nary Desicion Diagr)を利用した論理関数処理に基づく記号モデル検査法が提案されている。本報告では、システムがペトリネットによって記述され、検証すべき性質が線形時相論理(ner?time Temporal Log)で表されている場合に、記号モデル検査法を効率的に行う方法を提案する。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: The design verification to check whether designed systems satisfy given specifications becomes much important especially for complex, large-scale systems. On the other hand, as the systems to be verified become larger, the state explositon problem that the vefication costs increase exponentially. To avoid this problem, symbolic model checking based on manipulation of logic functions using Binary Decision Diaram has been proposed. This paper proposes some idea to accelerate symbolic model checking, where the systems are described by Petri-net, properties to be verified are formulated by Liner-time Temporal Logic.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 1993, 号 94(1993-SLDM-068), p. 155-162, 発行日 1993-10-28
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会