Research on Construction of a Logic for Formal Methods and Properties of First-Order Extensions

形式方法逻辑的构造及一阶可拓性质的研究

• 批准号: 22500021
• 负责人: OKAMOTO Keishi
• 金额: $ 1.25万
• 依托单位: Sendai National College of Technology (2011-2012)National Institute of Advanced Industrial Science and Technology (2010)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22500021/
• 关键词: 数理論理学; 形式手法; 命題様相μ計算; 一階様相μ計算; モデル; 表現力; 論理; (論理の)表現力

If we formalize a target system then we can verify whether thesystem satisfy desired property. For formal description and verification, we must constructa mathematical logic that is a framework for description and verification. We propose alogic for requirements management based on Jackson's Reference Model and a logic forautomated route planning for milk-run transport logistics. Besides, we provedmodel-theoretic property and expressiveness results for first-order modal mu-calculus.

如果我们形式化一个目标系统，那么我们就可以验证该系统是否满足期望的性质.为了进行形式化描述和验证，必须构造一个数理逻辑，它是描述和验证的框架。基于杰克逊的参考模型，我们提出了一个逻辑的需求管理和逻辑自动化路线规划牛奶运行运输物流。此外，我们还证明了一阶模态μ演算的模型论性质和可表达性结果。

项目成果

検証のための論理構築

用于验证的逻辑构造

• 发表时间: 2011
• 作者: Watanabe S.;et al;岡本圭史
• 通讯作者: 岡本圭史

Automated route planning for milk-runtransport logistics with the NuSMV modelchecker

使用 NuSMV 模型检查器进行牛奶运输物流的自动路线规划

• 期刊: The IEICE Transactions onInformation and Systems, Special Sectionon Parallel and Distributed Computing andNetworking
• 作者: タムケオ ディーン;篠原亮太;Takashi Kitamura and Keishi Okamoto
• 通讯作者: Takashi Kitamura and Keishi Okamoto

Comparing expressiveness of first-order modal μ-calculus and first-order CTL*

比较一阶模态 μ 演算和一阶 CTL 的表达能力*

• 发表时间: 2010
• 期刊: 京都大学数理解析研究所講究録
• 作者: Kamijo H;Matsumura Y;Thumkeo D;Koike S;Masu M;Shimizu Y;Ishizaki T;Narumiya S.;Keishi Okamoto;Keishi Okamoto
• 通讯作者: Keishi Okamoto

Toward a Concise Proof of Completeness Theorem for Propositional Modal \mu-calculus

命题模态μ微积分完备性定理的简明证明

• 发表时间: 2010
• 作者: Yuki ANBO;Keishi OKAMOTO;Akito TSUBOI
• 通讯作者: Akito TSUBOI

命題様相μ計算の一階拡張について

关于命题模态μ演算的一阶推广

• 发表时间: 2012
• 作者: Tanizaki H;Egawa G;Inaba K;Honda T;Nakajima S;Moniaga CS;Otsuka A;Ishizaki T;Tomura M;Watanabe T;Miyachi Y;Narumiya S;Okada T;Kabashima K;岡本圭史
• 通讯作者: 岡本圭史