Research on Construction of a Logic for Formal Methods and Properties of First-Order Extensions
Research on Construction of a Logic for Formal Methods and Properties of First-Order Extensions
形式方法逻辑的构造及一阶可拓性质的研究
批准号：
22500021
负责人：
OKAMOTO Keishi
金额：
$1.25万
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2011
资助国家：
日本
项目状态：
已结题
起止时间：
2011 至 2012
中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
検証のための論理構築
用于验证的逻辑构造
用于验证的逻辑构造
DOI：
--
发表时间：
2011
期刊：
影响因子：
--
作者：
[Watanabe S., et al, 岡本圭史]
通讯作者：
岡本圭史
Automated route planning for milk-runtransport logistics with the NuSMV modelchecker
使用 NuSMV 模型检查器进行牛奶运输物流的自动路线规划
使用 NuSMV 模型检查器进行牛奶运输物流的自动路线规划
DOI：
--
发表时间：
期刊：
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 的表达能力*
比较一阶模态 μ 演算和一阶 CTL 的表达能力*
DOI：
--
发表时间：
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
命题模态μ微积分完备性定理的简明证明
命题模态μ微积分完备性定理的简明证明
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
[Yuki ANBO, Keishi OKAMOTO, Akito TSUBOI]
通讯作者：
Akito TSUBOI
Formal Validation and Requirements Management Based on the Jackson's Reference Model for Requirements and Specifications
基于杰克逊需求和规范参考模型的形式验证和需求管理
基于杰克逊需求和规范参考模型的形式验证和需求管理
DOI：
--
发表时间：
2010
期刊：
Proceedings of the 16th IEEE Pacific Rim International Symposium on Dependable Computing
影响因子：
--
作者：
[Takashi KITAMURA, Keishi OKAMOTO, Makoto TAKEYAMA]
通讯作者：
Makoto TAKEYAMA
共 18 条
ロクアイタンポポ（仮称）の特徴明確化とバイオテクノロジー分野の実習ツールの開発
-
批准号：22H04271
-
项目类别：Grant-in-Aid for Encouragement of Scientists
-
资助金额：$0.31万
-
财政年份：2022
-
负责人：OKAMOTO Keishi
-
依托单位：
Macroscopic anatomical utilization of CT images gained before dissection practice
-
批准号：16K08445
-
项目类别：Grant-in-Aid for Scientific Research (C)
-
资助金额：$3.08万
-
财政年份：2016
-
负责人：OKAMOTO Keishi
-
依托单位：
海外基金