International collaborative studies on a logical specification and verification language.

逻辑规范和验证语言的国际合作研究。

• 批准号: 13558031
• 负责人: OKADA Mitsuhiro
• 金额: $ 4.29万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-13558031/
• 关键词: Real Time Systems; Formal Specification; Formal Verification; Linear Logic; Proof Search; 証明論

We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.

我们基于线性逻辑，与法国合作伙伴小组（Jean-Pierre Jouannaud's Group）合作开发并设计了一种为动态实时系统的正式规范和验证工具。通过动态实时系统，我们是指一个多代理系统，其中可能更改参与代理的数量，并且可能动态地更改时间约束，我们给出了一个自动转换过程，以将用户级别的自然规范转换为线性逻辑规范。我们还提供了一个消除程序，以从线性逻辑规范中消除密集的时间概念。然后，根据线性逻辑片段的证明搜索机制进行各种验证。密集的时间消除过程是通过建设性逻辑中已知的程序提取方法给出的。我们还为安全协议的正确性证明开发了一个逻辑框架，并应用了相同的概念。我们还研究了有关线性逻辑的一些相关逻辑研究，这是我们验证工具的逻辑框架。

项目成果

eds.M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security -- Theories and Systems, Lecture Notes in Computer Science, Hot Topics No.2609"Springer-Verlag. 470 (2003)

eds.M.Okada、B.Pierce、A.Scedrov、H.Tokuda、A.Yonezawa：“软件安全——理论与系统，计算机科学讲义，热门话题 No.2609”Springer-Verlag。

M.Okada, M.Kanouchi, A.Scedrov: "Phase Semantics for Light Linear Logic and Semantic Cut-Elimination Proof"Theoretical Computer Science. (近刊). (2002)

M.Okada、M.Kanouchi、A.Scedrov：“轻线性逻辑的相位语义和语义剪切消除证明”理论计算机科学（即将出版）。

M.Okada, F.Blarqui, J-P Jouannaul: "Inductive Data Type Systems"Theoretical Computer Science. 272. 41-68 (2002)

M.Okada、F.Blarqui、J-P Jouannaul：“归纳数据类型系统”理论计算机科学。

岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17・2. 224-231 (2002)

冈田光宏：“本体论的哲学和逻辑背景”人工智能学会杂志17・2（2002）。

H.Kushida, M.Okada: "A proof-theoretic study of the correspondence of classical logic and modal logic"Journal of Symbolic Logic. vol.68,4. 1403-1414 (2003)

H.Kushida，M.Okada：“经典逻辑和模态逻辑对应关系的证明理论研究”符号逻辑杂志。