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

定性的検証手法の余代数による一般化と,定量的検証手法の導出

Research Project

Project/Area Number 16J08157
Research Category

Grant-in-Aid for JSPS Fellows

Allocation TypeSingle-year Grants
Section国内
Research Field Software
Research InstitutionThe University of Tokyo

Principal Investigator

卜部 夏木  東京大学, 情報理工学系研究科, 特別研究員(DC1)

Project Period (FY) 2016-04-22 – 2019-03-31
Project Status Completed (Fiscal Year 2018)
Budget Amount *help
¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 2018: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2017: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2016: ¥700,000 (Direct Cost: ¥700,000)
Keywords形式検証 / 圏論 / 不動点 / 確率的システム / マルチンゲール / ランキング関数 / テイル確率 / スーパバイザリ制御 / Buechiオートマトン / parityオートマトン / supermartingale / 確率的オートマトン / ranking function / 余代数 / 定量的システム / 模倣
Outline of Annual Research Achievements

前々年度,申請者は「ランキング関数」という検証手法を圏論的に一般化・具体化する事で確率的遷移系に対し「γ縮尺劣マルチンゲール」と呼ばれる概念を得る事に成功した.これを用いると確率的遷移系の停止確率の下限を定量的に見積もることができる.今年度は京都大学の滝坂透氏,総合研究大学院大学の大藪雄一郎氏との共同研究の一環で,確率的プログラムの停止確率の下限をγ縮尺劣マルチンゲールを用い計算するアルゴリズムを提案し,それを実際に実装・実験を行ってその有用性を確かめた.申請者は具体的なアルゴリズムの導出および実装の一部を担当した.申請者の貢献度は20%程度である.結果をまとめた論文は国際会議ATVA 2018に採択された.
確率的システムに対し,その終了までにかかるステップ数がある値以上になる確率を「テイル確率」と呼ぶ.東京大学の内藏理史と共同で,マルチンゲールを用いて確率的システムのテイル確率の上限を与える研究も行った.申請者の貢献度は10%程度である.結果をまとめた論文は国際会議TACAS 2019に採択された.
また,大阪大学の榊原愛海氏および潮俊光教授と共同で離散事象システムのスーパバイザリ制御に関する研究も行った.本研究ではLTL[F]と呼ばれる線形時相論理(LTL)の定量的な拡張を考え,与えられたLTL[F]式の評価値がある閾値を超えるように離散事象システムを制御するスーパーバイザを構成する方法を与えた.申請者の貢献は50%程度である.結果をまとめた論文は今後査読付きの雑誌に投稿される予定である.
また,前年度国際ワークショップCMCS 2018に投稿され採択されていた論文の発表が本年度申請者によって行われた.それ以外にも,国際会議CPS Week 2018およびETAPS 2018に参加し,議論及び動向調査を行った.
また,前々年度,前年度,本年度の成果を博士論文として体系化した.

Research Progress Status

平成30年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

平成30年度が最終年度であるため、記入しない。

Report

(3 results)
  • 2018 Annual Research Report
  • 2017 Annual Research Report
  • 2016 Annual Research Report
  • Research Products

    (12 results)

All 2019 2018 2017 2016 Other

All Journal Article (8 results) (of which Peer Reviewed: 8 results,  Open Access: 2 results,  Acknowledgement Compliant: 2 results) Presentation (3 results) (of which Int'l Joint Research: 3 results) Remarks (1 results)

  • [Journal Article] Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments2019

    • Author(s)
      Satoshi Kura, Natsuki Urabe and Ichiro Hasuo
    • Journal Title

      Proceeding of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)

      Volume: 印刷中

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors2018

    • Author(s)
      Urabe Natsuki and Hasuo Ichiro
    • Journal Title

      Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers

      Volume: 11202 Pages: 214-234

    • DOI

      10.1007/978-3-030-00389-0_12

    • ISBN
      9783030003883, 9783030003890
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs2018

    • Author(s)
      Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, Ichiro Hasuo
    • Journal Title

      Proc. ATVA 2018, Lecture Notes in Computer Science

      Volume: 11138 Pages: 476-493

    • DOI

      10.1007/978-3-030-01090-4_28

    • ISBN
      9783030010898, 9783030010904
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors2018

    • Author(s)
      Natsuki Urabe and Ichiro Hasuo
    • Journal Title

      Proceedings of the 14th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2018)

      Volume: 印刷中

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Categorical Liveness Checking by Corecursive Algebras2017

    • Author(s)
      Natsuki Urabe, Masaki Hara, Ichiro Hasuo
    • Journal Title

      Proc. LICS 2017

      Volume: - Pages: 1-12

    • DOI

      10.1109/lics.2017.8005151

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective2017

    • Author(s)
      Natsuki Urabe, Ichiro Hasuo
    • Journal Title

      Logimal Methods in Computer Science

      Volume: 13

    • DOI

      10.23638/LMCS-13(3:20)2017

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Categorical Liveness Checking by Corecursive Algebras2017

    • Author(s)
      Natsuki Urabe, Masaki Hara, Ichiro Hasuo
    • Journal Title

      Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

      Volume: 印刷中

    • Related Report
      2016 Annual Research Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Journal Article] Coalgebraic Trace Semantics for Buechi and Parity Automata2016

    • Author(s)
      Natsuki Urabe, Shunsuke Shimizu, Ichiro Hasuo
    • Journal Title

      Leibniz International Proceedings in Informatics (LIPIcs)

      Volume: 59

    • DOI

      10.4230/LIPIcs.CONCUR.2016.24

    • Related Report
      2016 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Presentation] Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors2018

    • Author(s)
      Natsuki Urabe
    • Organizer
      14th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2018)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Categorical Liveness Checking by Corecursive Algebras2017

    • Author(s)
      Natsuki Urabe
    • Organizer
      32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
    • Related Report
      2017 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Coalgebraic Trace Semantics for Buechi and Parity Automata2016

    • Author(s)
      Natsuki Urabe
    • Organizer
      The 27th International Conference on Concurrency Theory (CONCUR 2016)
    • Place of Presentation
      Quebec City, Canada
    • Related Report
      2016 Annual Research Report
    • Int'l Joint Research
  • [Remarks] 卜部夏木 研究者ページ

    • URL

      http://group-mmm.org/~nurabe/index.html

    • Related Report
      2016 Annual Research Report

URL: 

Published: 2016-05-17   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi