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

• Project/Area Number: 16J08157
• Research Category: Grant-in-Aid for JSPS Fellows
• Allocation Type: Single-year Grants
• Section: 国内
• Research Field: Software
• Research Institution: The University of Tokyo
• Principal Investigator: 卜部 夏木 東京大学, 情報理工学系研究科, 特別研究員(DC1)
• Project Period (FY): 2016-04-22 – 2019-03-31
• Project Status: Completed (Fiscal Year 2018)
• Budget Amount: ¥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年度が最終年度であるため、記入しない。

Research Products

• [Journal Article] Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments (2019)
  • 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: 印刷中
  • Peer Reviewed
• [Journal Article] Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors (2018)
  • 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
  • Peer Reviewed
• [Journal Article] Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs (2018)
  • 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
  • Peer Reviewed
• [Journal Article] Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors (2018)
  • 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: 印刷中
  • Peer Reviewed
• [Journal Article] Categorical Liveness Checking by Corecursive Algebras (2017)
  • Author(s): Natsuki Urabe, Masaki Hara, Ichiro Hasuo
  • Journal Title: Proc. LICS 2017 Volume: - Pages: 1-12
  • DOI: 10.1109/lics.2017.8005151
  • Peer Reviewed
• [Journal Article] Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective (2017)
  • Author(s): Natsuki Urabe, Ichiro Hasuo
  • Journal Title: Logimal Methods in Computer Science Volume: 13
  • DOI: 10.23638/LMCS-13(3:20)2017
  • Peer Reviewed / Open Access
• [Journal Article] Categorical Liveness Checking by Corecursive Algebras (2017)
  • 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: 印刷中
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Coalgebraic Trace Semantics for Buechi and Parity Automata (2016)
  • 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
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Presentation] Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors (2018)
  • Author(s): Natsuki Urabe
  • Organizer: 14th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2018)
  • Int'l Joint Research
• [Presentation] Categorical Liveness Checking by Corecursive Algebras (2017)
  • Author(s): Natsuki Urabe
  • Organizer: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
  • Int'l Joint Research
• [Presentation] Coalgebraic Trace Semantics for Buechi and Parity Automata (2016)
  • Author(s): Natsuki Urabe
  • Organizer: The 27th International Conference on Concurrency Theory (CONCUR 2016)
  • Place of Presentation: Quebec City, Canada
  • Int'l Joint Research
• [Remarks] 卜部夏木 研究者ページ
  • URL: http://group-mmm.org/~nurabe/index.html