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

余代数定性验证方法的推广及定量验证方法的推导

基本信息

批准号：
16J08157
负责人：
卜部夏木
金额：
$ 1.22万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2016
资助国家：
日本
起止时间：
2016-04-22 至 2019-03-31
项目状态：
已结题

项目摘要

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

两年前，申请人通过使用范畴论对称为“排序函数”的验证方法进行概括和具体化，成功地获得了随机转移系统的称为“γ尺度鞅”的概念。利用这一点，可以定量估计随机转移系统停止概率的下界。今年，作为我们与京都大学的 Toru Takisaka 和高等研究大学的 Yuichiro Oyabu 联合研究的一部分，我们提出了一种使用 γ 尺度下鞅计算停止随机程序的概率下界的算法我们实际实施并进行了实验，以确认其有用性。申请人负责具体算法的部分推导和实现。申请人的贡献约为20%。总结结果的论文被国际会议 ATVA 2018 接受。对于随机系统，完成系统所需的步数大于或等于某个值的概率称为“尾部概率”。我们还与东京大学的 Satoshi Uchikura 合作，进行了使用鞅给出随机系统尾部概率上限的研究。申请人的贡献约为10%。总结结果的论文被 TACAS 2019 国际会议接受。我们还与大阪大学的Manami Sakakibara先生和Toshimitsu Ushio教授合作进行了离散事件系统的监督控制研究。在本研究中，我们考虑线性时序逻辑（LTL）的定量扩展，称为 LTL[F]，并开发一个控制离散事件系统的监督器，以便给定 LTL[F] 表达式的评估值超过某个阈值。我给了你一个配置方法。申请人的贡献约为50%。总结结果的论文将在未来提交给同行评审期刊。此外，今年的申请者还提交了去年在CMCS 2018国际研讨会上提交并接受的论文。此外，我们还参加了国际会议CPS Week 2018和ETAPS 2018，并进行讨论和研究趋势。另外，将前年、前年、今年的成果系统化为博士论文。