Research on Construction of a Logic for Formal Methods and Properties of First-Order Extensions
| Project/Area Number | 22500021 |
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Sendai National College of Technology(2011-2012)
National Institute of Advanced Industrial Science and Technology(2010) |
|---|
Principal Investigator |
OKAMOTO Keishi 仙台高等専門学校, 情報システム工学科, 准教授 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KITAMURA Takashi 産業技術総合研究所, セキュアシステム研究部門, 研究員 (70530484)
|
|---|
| Project Period (FY) |
2011 – 2012
|
| Project Status |
Completed(Fiscal Year 2012)
|
| Budget Amount *help |
¥1,950,000 (Direct Cost : ¥1,500,000、Indirect Cost : ¥450,000)
Fiscal Year 2012 : ¥650,000 (Direct Cost : ¥500,000、Indirect Cost : ¥150,000)
Fiscal Year 2011 : ¥650,000 (Direct Cost : ¥500,000、Indirect Cost : ¥150,000)
Fiscal Year 2010 : ¥650,000 (Direct Cost : ¥500,000、Indirect Cost : ¥150,000)
|
|---|
| Keywords | 数理論理学 / 形式手法 / 命題様相μ計算 / 一階様相μ計算 / モデル / 表現力 / 論理 / (論理の)表現力 |
|---|
| Research Abstract |
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.
|
Report
(4results)
Research Products
(21results)
