パイ計算による仕様を検証する論理体系
スポンサーリンク
概要
- 論文の詳細を見る
本発表では, 拡張されたパイ計算のプロセスの性質を証明する論理体系を提案する.特に, この論理体系はプロセスの活性や停止性を証明する.この論理体系の対象であるパイ計算は, ネピの方法に従って代数仕様の項をパイ計算に付け加えることによって拡張されたものである.代数仕様の項があるので, パイ計算の原形そのままよりも, 仕様の記述が便利になっている.パイ計算の不停止は余再帰的枚挙完全であるので, その完全な再帰的公理化は不可能である.そのため, 論理体系の設計方針は, 健全で, かつ, 適当に証明力が強く, 適当に簡明である, というものとなる.論理体系は, 代数仕様の項をその項とするような様相述語論理である.各論理式はある1個のプロセスの満たす性質を表す.様相記号はプロセスの遷移を表す.プロセスの並行合成に対応して, 論理式の文法には並行合成を表す論理記号がある.それは線形論理の乗法的連言によく似た性質を持つ論理記号であり, 論理規則もまた線形論理によく似たものとなっている.
- 2005-08-15
著者
関連論文
- 確率様相論理による秘匿性の証明 (代数と言語のアルゴリズムと計算理論)
- 確率様相論理による秘匿性の証明
- 自治体EAへの形式手法適用の試み
- 自治体EAへの形式手法適用の試み
- 定性空間表現の二次元平面への埋め込みについて
- 定性空間表現の二次元平面への埋め込みについて
- パイ計算による仕様を検証する論理体系
- 様相論理による通信の安全性の記述 (代数系アルゴリズムと言語および計算理論)
- AS-3-1 大規模なサービスプロセスの設計・検証手法(AS-3.ワークフローとビジネスプロセス管理への数理的アプローチ,シンポジウムセッション)
- 確率様相論理による秘匿性の証明