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

概要

論文の詳細を見る
超大規模論理回路技術の進展により,設計対象システムの形式的仕様記述や形式的検証手法の研究が重要になってきている.形式的仕様記述や形式的検証のアプローチとしては,命題論理や第1階述語論理,時相論理等の論理体系に基づく方法や,VDMや抽象データ型による仕様記述等の代数的方法,また,正則集合や第1#表現等の系列記述に基づく方法等がある.特に時相論理は時間の概念を陽に表現できるため,現在,並行プロセスやハードウェアの設計検証との関連で研究が進められているが,従来の命題時相論理では有限オートマトンの性質が完全には記述できないため,種々のクラスの時相論理が提案されている.それらの中で,拡張時相論理はω-正則集合を表現できるが,そのためには無限個の時相論理記号を必要とする.一方,インターバル時相論理の表現能力は真に正則集合を含んでいるが,充足可能性判定問題が決定不能になる等の問題点を含んでいる.設計対象を有限オートマトンと考えると,有限個の時相論理記号で正則集合を表現できる時相論理の体系を明らかにすることが重要であると考えられる.このような観点から,ここでは,時相論理記号として「:」と「〓」を新たに導入し,正則集合と等価な表現能力を持ち充足可能性判定問題が決定可能な正則時相論理(RTL)を示す.
1987-02-15

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

スポンサーリンク

概要

著者

関連論文

スポンサーリンク