真の並行プロセス代数のためのプロセス論理における充足可能性の決定不能性
スポンサーリンク
概要
- 論文の詳細を見る
本稿で、我々は真の並行プロセス代数のためのプロセス論理によって記述された仕様の充足可能性は決定不能であることを示す。この決定不能性は、仕様が有限状態をもち、離接演算子∨や通信要求をもたない場合にも成り立つ。真の並行性の概念は並行動作とインターリービング動作を明確に区別し、真の並行性によって拡張された多くのプロセス代数が提案されている。我々は非常に簡単な真の並行プロセス代数とプロセス論理を用いており、本稿で与えられる結果はこれら多くの真の並行プロセス代数に拡張可能である。
- 社団法人電子情報通信学会の論文
- 2001-05-21
著者
関連論文
- Promelaにおける割り込み制御処理の半自動モデル化 (コンカレント工学)
- Promelaにおける割り込み制御処理の半自動モデル化 (信号処理)
- Promelaにおける割り込み制御処理の半自動モデル化 (VLSI設計技術)
- Promelaにおける割り込み制御処理の半自動モデル化 (回路とシステム)
- 並行システムを解析するための逐次化と状態削減機能の実装--仕様の自動生成を目指して (信号処理)
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- LIpS : 際標準に基づく形式的仕様記述LOTOSの支援環境(3) : 抽象データ記述の処理[INTAP研究開発委員会プロトコル形式記述WG]
- LIpS : 際標準に基づく形式的仕様記述LOTOSの支援環境(2) : 中間言語 Arbalotos[INTAP研究開発委員会プロトコル形式記述WG]
- LIpS : 国際標準に基づく形式的仕様記述LOTOSの支援環境(1) : 設計概要[INTAP研究開発委員会プロトコル形式記述WG]
- 並行システムを解析するための逐次化と状態削減機能の実装 : 仕様の自動生成を目指して(システムと信号処理及び一般)