• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 22500021
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field Fundamental theory of informatics
Research InstitutionSendai 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

(4 results)
  • 2012 Annual Research Report   Final Research Report ( PDF )
  • 2011 Annual Research Report
  • 2010 Annual Research Report
  • Research Products

    (21 results)

All 2013 2012 2011 2010 Other

All Journal Article (10 results) (of which Peer Reviewed: 8 results) Presentation (11 results)

  • [Journal Article] Automated route planning for milk-run transport logistics with the NuSMV model checker2013

    • Author(s)
      Takashi Kitamura and Keishi Okamoto
    • Journal Title

      The IEICE Transactions on Information and Systems, Special Section on Parallel and Distributed Computing and Networking(Conditionally Accepted)

      Volume: ―

    • NAID

      130003385424

    • Related Report
      2012 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 要求・仕様参照モデルに基づく要求追跡の形式手法2010

    • Author(s)
      北村崇師,岡本圭史,武山誠, Jackson の
    • Journal Title

      Proceedings of the IPSJ/SIGSE ソフトウェアエンジニアリングシンポジウム

      Pages: 149-154

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Journal Article] Formal Verification ina First-Order Extension of Modal μ-calculus2010

    • Author(s)
      Keishi Okamoto
    • Journal Title

      Information and MediaTechnologies

      Volume: 5(1) Pages: 40-47

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Journal Article] Comparing expressiveness of first-order modal μ-calculus and first-order CTL2010

    • Author(s)
      Keishi Okamoto
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: 1708

    • Related Report
      2012 Final Research Report
  • [Journal Article] Formal Validation and Requirements Management Based on the Jackson's Reference Model for Requirements and Specifications2010

    • Author(s)
      Takashi KITAMURA, Keishi OKAMOTO, Makoto TAKEYAMA
    • Journal Title

      Proceedings of the 16th IEEE Pacific Rim International Symposium on Dependable Computing

      Volume: (Published electronically)

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Jacksonの要求・仕様参照モデルに基づく要求追跡の形式手法2010

    • Author(s)
      北村崇師, 岡本圭史, 武山誠
    • Journal Title

      Proceedings of the IPSJ/SIGSEソフトウェアエンジニアリングシンポジウム

      Pages: 149-154

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Formal Verification in a First-Order Extension of Modal μ-calculus2010

    • Author(s)
      Keishi Okamoto
    • Journal Title

      Information and Media Technologies

      Volume: 5(1) Pages: 40-47

    • NAID

      130004549126

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Comparing expressiveness of first-order modal μ-calculus and first-order CTL*2010

    • Author(s)
      Keishi Okamoto
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: 1708 Pages: 1-14

    • Related Report
      2010 Annual Research Report
  • [Journal Article] Automated route planning for milk-runtransport logistics with the NuSMV modelchecker

    • Author(s)
      Takashi Kitamura and Keishi Okamoto
    • Journal Title

      The IEICE Transactions onInformation and Systems, Special Sectionon Parallel and Distributed Computing andNetworking

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Journal Article] Formal Validation andRequirements Management Based on theJackson's Reference Model forRequirements and Specifications

    • Author(s)
      Takashi KITAMURA,Keishi Okamoto,MakotoTAKEYAMA
    • Journal Title

      Proceedings of the 16th IEEE Pacific RimInternational Symposium on DependableComputing

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Presentation] 一階時相論理の表現力について2013

    • Author(s)
      岡本圭史
    • Organizer
      日本数学会2013年度年会
    • Place of Presentation
      京都大学
    • Related Report
      2012 Annual Research Report 2012 Final Research Report
  • [Presentation] 命題時相論理の一階拡張について2012

    • Author(s)
      岡本圭史
    • Organizer
      2010年日本数学会秋季総合分科会
    • Place of Presentation
      東京理科大学
    • Year and Date
      2012-03-27
    • Related Report
      2012 Final Research Report 2011 Annual Research Report
  • [Presentation] Anautomated route planning for milk-runtransport logistics using model checking2012

    • Author(s)
      Takashi Kitamura, Keishi Okamoto
    • Organizer
      4th International Workshop on Parallel andDistributed Algorithms and Applications
    • Place of Presentation
      Okinawa, Japan
    • Related Report
      2012 Final Research Report
  • [Presentation] An automated route planning for milk-run transport logistics using model checking2012

    • Author(s)
      Takashi Kitamura, Keishi Okamoto
    • Organizer
      4th International Workshop on Parallel and Distributed Algorithms and Applications
    • Place of Presentation
      Okinawa, Japan
    • Related Report
      2012 Annual Research Report
  • [Presentation] 命題様相μ計算の一階拡張について2012

    • Author(s)
      岡本圭史
    • Organizer
      仙台ロジックセミナー
    • Place of Presentation
      東北大学
    • Related Report
      2012 Annual Research Report
  • [Presentation] 検証のための論理構築2011

    • Author(s)
      岡本圭史
    • Organizer
      論理学的手法に基づくプログラム検証技術
    • Place of Presentation
      東北大学
    • Year and Date
      2011-12-07
    • Related Report
      2011 Annual Research Report
  • [Presentation] Formal Validation and Requirements Management Based on theJackson's Reference Model forRequirements and Specifications2010

    • Author(s)
      Takashi KITAMURA,Keishi Okamoto,MakotoTAKEYAMA
    • Organizer
      The 16thIEEE Pacific Rim International Symposiumon Dependable Computing
    • Place of Presentation
      National Institute of Informatics,Tokyo, Japan
    • Year and Date
      2010-12-15
    • Related Report
      2012 Final Research Report
  • [Presentation] Formal Validation and Requirements Management Based on the Jackson's Reference Model for Requirements and Specifications2010

    • Author(s)
      Takashi KITAMURA, Keishi OKAMOTO, Makoto TAKEYAMA
    • Organizer
      The 16th IEEE Pacific Rim International Symposium on Dependable Computing
    • Place of Presentation
      National Institute of Informatics, Tokyo, Japan
    • Year and Date
      2010-12-15
    • Related Report
      2010 Annual Research Report
  • [Presentation] Toward a Concise Proof ofCompleteness Theorem for PropositionalModal ¥mu-calculus2010

    • Author(s)
      Yuki ANBO, Keishi OKAMOTO and AkitoTSUBOI
    • Organizer
      2010年日本数学会秋季総合分科会
    • Place of Presentation
      名古屋大学
    • Year and Date
      2010-09-22
    • Related Report
      2012 Final Research Report
  • [Presentation] Toward a Concise Proof of Completeness Theorem for Propositional Modal \mu-calculus2010

    • Author(s)
      Yuki ANBO, Keishi OKAMOTO, Akito TSUBOI
    • Organizer
      2010年日本数学会秋季総合分科会
    • Place of Presentation
      名古屋大学
    • Year and Date
      2010-09-22
    • Related Report
      2010 Annual Research Report
  • [Presentation] Jacksonの要求・仕様参照モデルに基づく要求追跡の形式手法2010

    • Author(s)
      北村崇師,岡本圭史,武山誠
    • Organizer
      ソフトウェアエンジニアリングシンポジウム2010
    • Place of Presentation
      東洋大学
    • Year and Date
      2010-09-01
    • Related Report
      2012 Final Research Report 2010 Annual Research Report

URL: 

Published: 2010-11-30   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi