π-計算の名前制限の名前生成による実装の正しさ
スポンサーリンク
概要
- 論文の詳細を見る
プロセス代数π-計算は,プロセス間の通信リンクの動的接続を表現できる形式モデルである.本論文では,π-計算の実装に必要となる通信リンクの実装方法について述べる.π-計算では,通信リンクを「名前制限」と呼ばれる概念で形式化する.一方,実装では通信リンクは「名前生成」で扱うのが容易である.両者の同等性の形式的な証明は与えられていない.また,π-計算に対してデータタイプを加えた体系では,両者の同等性に関する反例が存在する.本論文では,データタイプ部を加えたπ-計算を扱い,名前制限と名前生成の同等性を論じる.
- 社団法人電子情報通信学会の論文
- 2002-03-01
著者
-
真野 健
NTTコミュニケーション科学基礎研究所
-
小暮 潔
日本電信電話株式会社NTTコミュニケーション科学基礎研究所
-
河辺 義信
日本電信電話株式会社nttコミュニケーション科学基礎研究所
-
小暮 潔
日本電信電話株式会社 Nttコミュニケーション科学基礎研究所
-
小暮 潔
日本電信電話(株)基礎研究所
-
真野 健
日本電信電話株式会社NTTコミュニケーション科学基礎研究所
-
堀田 英一
日本電信電話株式会社NTT情報流通プラットフォーム研究所
-
堀田 英一
日本電信電話株式会社 Ntt情報流通プラットフォーム研究所
関連論文
- 確率様相論理による秘匿性の証明 (代数と言語のアルゴリズムと計算理論)
- 実世界指向情報統合に向けて
- 歩行者ナビゲーションにおける情報伝達の利用者適応の分析
- 実世界指向情報統合に向けて
- 確率様相論理による秘匿性の証明
- B.A.Davey and H.A.Priestley 著, "Introduction to Lattices and Order", Cambridge University Press, 248p., 1990
- コンピュータサイエンスシリーズ 15 離散数学, 牛島和夫(編著), 相利民, 朝廣雄一(著), コロナ社(2006-09), A5判, 定価(本体3,000円+税)
- 否定的情報により拡張された型付き素性構造
- 増進的複製による型付き素性構造差分計算手法
- 型付き素性構造の差分演算
- 増進的複製による型付き素性構造汎化手法
- COLING '92 Nantes参加報告
- 文法規則の構造共有による選言的素性構造単一化の効率化
- イベント順序証明システムの正当性の形式的証明
- コミュニケーション科学技術の新領域開拓活動--ディジタルシティの研究 (特集 NTTにおけるオープン・ラボ活動)
- π計算に基づくプログラミング言語NepiのためのGUI機能
- ダイナミック・スライス型リンク方式による時刻証明の長期有効性保証方法(オフィスインフォメーションシステム及び一般)
- タイムスタンプ長期有効性保証フレームワーク(オフィスインフォメーションシステム及び一般)
- イベント順序証明システムの脅威分析
- イベント順序証明システムの実現機構
- イベント順序証明技術を用いた長期有効性保証タイムスタンプシステム
- スケーラブルで単一攻撃点のないイベント順序証明システム実現機構
- イベント順序証明技術を用いた長期有効性保証タイムスタンプシステム
- スケーラブルで単一攻撃点のないイベント順序証明システム実現機構
- 高階書換え系の単一正規形性
- 高階書き換え系の単一正規形性
- 圧力分布センサによる人の触行動の実時間識別とその個人適応手法
- Nepi : π計算に基づくネットワーク・プログラミング言語
- ゲーム列による安全性証明の形式化と自動化(数理的技法による情報セキュリティ)
- 匿名性とプライバシ保護の数理的技法 (特集 コミュニケーション環境の未来に向けた研究最前線)
- ETAPS 2006参加報告(会議レポート)
- Nepiネットワークプログラミングシステムの形式的検証(ソフトウェア工学の基礎)
- π-計算の名前制限の名前生成による実装の正しさ
- プロセス代数に基づくネットワークプログラム言語 (特集論文1 情報科学研究の最前線--より安全で快適な情報処理技術を目指して) -- (快適にコンピュータを使えるために)
- π-計算に基づくモバイルエージェントの形式化
- アクタモデルのπ計算に基づく意味づけ : エージェントの形式化に向けて
- 関数部分知識と匿名性検証(理論,数理的技法による情報セキュリティ,平成19年研究部会連合発表会)
- 攻撃者を考慮した匿名性検証法 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (形式的手法)
- D-18 移動軌跡データモデルと領域に基づく問合せ処理(データ編成と高速化,D.データベース)
- 歩行者ナビゲーションにおける情報伝達の利用者適応の分析
- Generic Communication Protocol Program を利用したエージェントの interoperability の実現
- チャネルに基づく選択付き通信のための分散プロトコル
- Nepi^2: π計算に基づくネットワーク・プログラミングのための2レベル計算体系
- 超高速ネットワークのためのルーチング技術
- 電子投票プロトコルに対する無証拠性の定理証明
- フォーマルメソッドによるセキュリティ&プライバシ (特集 20周年を迎えたコミュニケーション科学)
- 「情報処理学会論文誌 : プログラミング」の編集について
- 匿名性・プライバシーの工学的定式化とその学際的応用
- CoSyProofs 2009参加報告(会議レポート)
- 認知変数連結論 : 認知心理学を見つめ直す, 中島義明(著), コロナ社(2007-11), B6判, 定価(本体2,600円+税)
- 6. 匿名性とプライバシのためのフォーマルメソッド(Part III:新領域の開拓,フォーマルメソッドの新潮流)
- 順序ソート項書換え系における合流性のモジュラ性
- 確率様相論理による秘匿性の証明
- 電子投票プロトコルに対する無証拠性の定理証明 (特集 人と共存するコンピュータセキュリティ技術)
- コンシェルジュサーバを持つ電話システムの形式的検証