正則集合と表現等価な正則時相論理RTL

• Item type: Journal(1)
• 公開日: 1987-02-15
• タイトル: 正則集合と表現等価な正則時相論理RTL
• タイトル / 言語: en
• タイトル: RTL : Regular Temporal Logic Expressively Equivalent to Regular Set
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 基礎理論
• 著者所属: 京都大学工学部情報工学教室
• 著者所属: 京都大学工学部情報工学教室
• 著者所属(英): en
• 著者所属(英): Department of Information Science, Faculty of Engineering, Kyoto University
• 著者所属(英): en
• 著者所属(英): Department of Information Science, Faculty of Engineering, Kyoto University
• 著者名: 平石, 裕実; 矢島, 脩三
• 著者名(英): Hiromi, Hiraishi; Shuzo, Yajima
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 超大規模論理回路技術の進展により 設計対象システムの形式的仕様記述や形式的検証手法の研究が重要になってきている.形式的仕様記述や形式的検証のアプローチとしては 命題論理や第1階述語論理 時相論理等の論理体系に基づく方法や VDMや抽象データ型による仕様記述等の代数的方法 また 正則集合や第1#表現等の系列記述に基づく方法等がある.特に時相論理は時間の概念を陽に表現できるため 現在 並行プロセスやハードウェアの設計検証との関連で研究が進められているが 従来の命題時相論理では有限オートマトンの性質が完全には記述できないため 種々のクラスの時相論理が提案されている.それらの中で 拡張時相論理はω-正則集合を表現できるが そのためには無限個の時相論理記号を必要とする.一方 インターバル時相論理の表現能力は真に正則集合を含んでいるが 充足可能性判定問題が決定不能になる等の問題点を含んでいる.設計対象を有限オートマトンと考えると 有限個の時相論理記号で正則集合を表現できる時相論理の体系を明らかにすることが重要であると考えられる.このような観点から ここでは 時相論理記号として「:」と「〓」を新たに導入し 正則集合と等価な表現能力を持ち充足可能性判定問題が決定可能な正則時相論理(RTL)を示す.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 28, 号 2, p. 117-123, 発行日 1987-02-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764