WEKO3
アイテム
パイ計算による仕様を検証する論理体系
https://ipsj.ixsq.nii.ac.jp/records/16613
https://ipsj.ixsq.nii.ac.jp/records/16613df9d0dec-1f49-474d-b6aa-f32ea4a31715
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO4611006.pdf (154.3 kB)
|
Copyright (c) 2005 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2005-08-15 | |||||||
| タイトル | ||||||||
| タイトル | パイ計算による仕様を検証する論理体系 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Logical System to Verify Specifications Written by Pi-calculus | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 産業技術総合研究所システム検証研究センター | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Research Center for Verification and Semantics National Institute of Advanced Science and Technology | ||||||||
| 著者名 |
竹内, 泉
× 竹内, 泉
|
|||||||
| 著者名(英) |
Izumi, Takeuti
× Izumi, Takeuti
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本発表では，拡張されたパイ計算のプロセスの性質を証明する論理体系を提案する．特に，この論理体系はプロセスの活性や停止性を証明する．この論理体系の対象であるパイ計算は，ネピの方法に従って代数仕様の項をパイ計算に付け加えることによって拡張されたものである．代数仕様の項があるので，パイ計算の原形そのままよりも，仕様の記述が便利になっている．パイ計算の不停止は余再帰的枚挙完全であるので，その完全な再帰的公理化は不可能である．そのため，論理体系の設計方針は，健全で，かつ，適当に証明力が強く，適当に簡明である，というものとなる．論理体系は，代数仕様の項をその項とするような様相述語論理である．各論理式はある1 個のプロセスの満たす性質を表す．様相記号はプロセスの遷移を表す．プロセスの並行合成に対応して，論理式の文法には並行合成を表す論理記号がある．それは線形論理の乗法的連言によく似た性質を持つ論理記号であり，論理規則もまた線形論理によく似たものとなっている． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | This presentation gives a logical system which proves the properties over process-terms of a modified variant of Pi-calculus. Especially, the logical system can prove liveness and termination of processes. The modification of Pi-calculus is to add terms of an algebra to Pi-calculus accoring to the style of Nepi. Because the termination on Pi-calculus is corecursively-enumerable-complete, one cannot axiomatise it recursively. Therefore, we should make the logical system such that it is sound, has the reasonable power to prove and is reasonably light. The logical system which is given here is a modal predicate logic whose terms are the terms of the algebra. Each formula denotes the property satisfied by a process. Modalities denote transitions. The logical system has a logical symbol to denote parallel composition of processes. The symbol is similar to multiplicative conjunction in linear logic, and the logical rules on it are also similar to those of linear logic. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 46, 号 SIG11(PRO26), p. 57-65, 発行日 2005-08-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
