初等的でないフレームを持つ様相論理の統一化による証明法
スポンサーリンク
概要
- 論文の詳細を見る
本研究では, フレームのクラスが一階の制約で特徴づけられない体系KMに対して分解証明法を定義する。公理Mは時系列モデルが終了状態に到達することを表しており, デッドロックがないこと証明するのに利用することができる。このために, まず, 一階の制約でフレームが特徴づけられる体系に対する様相記号列の統一化による分解証明法を構成する。これまでも, Untilを持つ論理について公理系に基づいて規則を定義するものや, □に支配されるの選言肢, ◇に支配される連言肢を展開しない形の節形式を用いるものが提案されているが, 本研究では, 様相記号へのラベリングに対して意味論を記述する一階の言語におけるスコーレム化と対応をとることで, 節がラベルづけられた様相記号列をprefixとするリテラルの選言肢となる節形式を導入する。これにより, これまでに述語論理などの分解証明法において研究されてきた戦略を様相論理の分解証明法に導入する際の見通しがよくなるだけでなく, 証明の途中で選言, 連言を展開する必要がなく, 証明が分解規則によるステップのみとなるため証明の流れが見やすい。次に, 一階の言語におけるスコーレム化と対応できないKMの場合について分解証明法を拡張する。
- 一般社団法人情報処理学会の論文
- 1997-09-24
著者
関連論文
- 記号論的暗号解析を用いたOblivious Transferプロトコルの解析(セキュリティ,フォーマルアプローチ論文)
- 記号論及び計算論によるセキュリティ解析の相互関係(数理的技法による情報セキュリティ)
- 仮想ネットワーク技術を用いたキャンパスネットワークの設計と構築 (インターネットアーキテクチャ)
- 仮想ネットワーク技術を用いたキャンパスネットワークの設計と構築 (技術と社会・倫理)
- NAREGIグリッドミドルウェアによる大規模連携接続実証実験(OS-6:分散システム,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- 証明力が拡張された適切さの論理体系ER
- 線形論理CLL_eのモデルを用いた意味論
- 仮想ネットワーク技術を用いたキャンパスネットワークの設計と構築(システム構築技術2,インターネットと情報倫理教育,一般)
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法(セッション4-B : ネットワークセキュリティ(1))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法
- 大学における情報化戦略と理工系情報学科の貢献
- 様相記号列統一化による様相論理定理証明器における自己代入の利用
- 様相記号列統一化による様相論理定理証明器の健全性と完全性
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法(セッション4-B : ネットワークセキュリティ(1))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法
- 仮想ネットワーク技術を用いたキャンパスネットワークの設計と構築(システム構築技術2,インターネットと情報倫理教育,一般)
- e-サイエンス基盤としての計算機センターPOP(Point-of-Presence)連携
- 分割アルゴリズムに基づく同型グラフの検索について
- リスト構造に対する整合機能の形式化
- PoP(Point of Presence)によるe-サイエンスリソース連携(研究発表,ネットワーク研究開発テストベッド運用・利用,一般)
- e-サイエンス基盤としての計算機センターPOP (Point-of-Presence) 連携
- ソフトウェア科学会第1回大会
- 自然言語に基づく静的システムの仕様のプロトタイププログラムへの変換手法
- Formal Method Europe(FME)2001参加報告
- 画像の構造情報の抽出とその応用
- 形式オントロジーに基づく遺伝子調節のための数値モデル
- 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性
- 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性
- Spi計算の型付けによる公開鍵暗号方式を用いたプロトコルのメッセージ認証の検証
- 初等的でないフレームを持つ様相論理の統一化による証明法
- 無線LANにおけるセキュリティ技術の動向
- 導出法による線形論理CLL_eの自動証明戦略
- オブジェクトの項表現を意味論の基礎とする論理体系としてのOntologyとその表現力
- リアクティブシステムの仕様記述言語とその記述操作の特徴付け
- 時相論理を用いた試験等価性の特性化
- 産業界からの理工系情報学科の研究教育内容への期待と大学の取り組み
- 大学における情報化戦略と理工系情報学科の貢献(パネル討論)
- 20周年記念特集号の編集にあたって(20周年記念特集)
- 時間論理によるリアクティブシステム仕様の検証の効率化(セキュアコンピューティング)
- SSLとリレーサーバを用いたPOP before SMTPのセキュアな実現法
- リアクティブシステムの段階的充足可能性とSafety Propertyの関係
- セキュリティプロトコルにおける暗号化メッセージの送信者による認知に関する検証法
- セキュリティプロトコルの一貫性および正常終了一致の同一参加者による複数セッションを考慮した検証法
- セキュリティプロトコルの一貫性および正常終了一致の検証法
- セキュリティプロトコルの一貫性および正常終了一致の検証法
- 自然言語の語彙分割による形式的仕様記述
- 合成可能なタブローによる仕様の差分的無矛盾性判定について (プログラム変換と記号・数式処理)
- 証明力を拡張した適切さの論理$ER$ (プログラム変換と記号・数式処理)
- 適切さと論理RとERの証明力の比較
- 適切さの論理ERの決定可能性
- 証明力を拡張した適切さの論理ER
- 大学における情報科学教育とリテラシー教育
- 欠陥仕様からの修正情報抽出に関する研究
- 合成可能な時間論理タブローの構成法
- 結合子の適切さによる人間の演繹的な推論の形式化 (&特集>「記号論理とAI」)
- 普通のUntil演算子を持つ命題実時間論理について
- 時相論理による段階的仕様記述プロセスに対応した検証法
- 証明の失敗から得られる情報を用いる様相論理定理証明戦略
- 時相論理による仕様記述の無矛盾性判定のための再利用可能なタブローについて
- 純粋関数型言語を用いた超コンパクト音声認識デコーダの開発
- 紛失通信プロトコルの解析のための可能世界意味論に基づく形式体系
- ソフトウェア発展と検証技術の未来 (特集 ソフトウェア発展)
- オブジェクトの生成,消滅を表現可能な論理体系DOL
- オブジェクトの生成、消滅を表現可能な論理体系DOL
- 様相論理 (<特集>非標準論理とその応用)
- The Temporal Semantics of Logic Programming
- 時相論理によるリアクティブシステム仕様の実現可能性に関する分類 (21世紀のソフトウェア工学)
- SAT solverを用いるLTLタブロー構成法とその評価