【11-02】SKLCS Seminar on”概率递归关系尾概率的自动化分析”

Title: 概率递归关系尾概率的自动化分析
Speaker: 符鸿飞，上海交通大学
Time: 2023年11月2日（周四）,上午10点
Venue: 中国科学院软件研究所5号楼三层，334报告厅
Abstract: 概率递归关系是描述随机算法运行时间的基本机制，其构成主要包括算法每一步递归的预处理时间以及算法的递归调用。概率递归关系从随机算法的复杂细节中抽取出与算法运行时间相关的部分，因此是随机算法运行时间的一个简洁表示。由于其简洁性，概率递归关系通常作为分析随机算法时间复杂度的一个标准模型。在概率递归关系的时间复杂度分析中，运行时间尾概率是一个重要的精细化刻画，表达随机算法运行时间超过预设阈值不终止的概率随阈值增长的衰减性。运行时间尾概率分析由于涉及随机算法时间复杂度的精细刻画，因而在理论上有挑战性。在已有结果中，具有一定普适性（即能适用于一大类概率递归关系）的方法仅有1994年由Karp推导出的类似主定理的方法，而其他方法都基于手动推导且只适用于单独特定的概率递归关系。因此，是否存在具有一定普适性且能够改进Karp经典结果的方法是概率递归关系尾概率分析的主要问题。报告人基于先前所作概率程序形式验证方面的成果，通过鞅理论建立了概率递归关系运行时间尾概率的指数验证条件，并进一步通过研究新的针对指数约束条件的求解算法，给出了一个适用于单递归以及分治递归概率递归关系运行时间尾概率的分析算法。实验结果表明，该算法所导出的运行时间尾概率在渐进行为上严格比Karp方法所导出的界限更紧致，且逼近或等同于经典算法Quicksort和Quickselect上由人工证明所导出的紧致尾概率上界。本成果的意义在于是继Karp经典方法之后的第一个针对概率递归关系尾概率分析问题的显著推进，且相比Karp方法能够处理范围更广的概率递归关系。
Bio: 符鸿飞博士毕业于德国亚琛工业大学，师从Joost-Pieter Katoen教授，研究方向为模型检验与程序验证，在POPL、PLDI、CAV、OOPSLA、TOPLAS等国际著名学术会议及期刊上发表多篇基础性理论成果。获HSCC 2013最佳学生论文奖。部分成果发表在由剑桥大学出版社出版的专著章节中。