论文标题
利用图形算法的功能：计算机辅助验证的有效算法
Leveraging the Power of Graph Algorithms: Efficient Algorithms for Computer-Aided Verification
论文作者
论文摘要
该论文的目的是利用快速的图形算法和现代算法技术，用于模型检查和图形，MDP和游戏图中的模型检查和合成中的问题。结果包括符号算法，这是模型检查中众所周知的算法类别，该算法对输入模型进行有限的访问以进行有效表示。特别是，我们介绍以下结果：具有平均值Büchi目标的游戏图算法和均值付款Cobüchi目标，这些目标与均值付款目标的最佳运行时间范围之一相匹配。用于图形和MDP中的StreetT目标的接近线性时间随机算法。图形中有限的Büchi目标的亚客体时间算法和游戏图的立方时间算法。在游戏图和MDP中查询可及性目标的有条件下限。线性和近线性时间算法分别用于图形和MDP中的顺序可及性目标。游戏图中奇偶校目标的第一个准多项式时间符号算法。我们通过提供次级时间符号算法来打破从90年代进行MEC分解的长期运行时间。
The goal of the thesis is to leverage fast graph algorithms and modern algorithmic techniques for problems in model checking and synthesis on graphs, MDPs, and game graphs. The results include symbolic algorithms, a well-known class of algorithms in model checking that trades limited access to the input model for an efficient representation. In particular, we present the following results: Algorithms for game graphs with mean-payoff Büchi objectives and mean-payoff coBüchi objectives which match one of the best running time bounds for mean-payoff objectives. A near-linear time randomized algorithm for Streett objectives in graphs and MDPs. A sub-cubic time algorithm for bounded Büchi objectives in graphs and a cubic time algorithm for game graphs. Conditional lower bounds for queries of reachability objectives in game graphs and MDPs. Linear and near-linear time algorithms for sequential reachability objectives in graphs and MDPs respectively. The first quasi-polynomial time symbolic algorithm for parity objectives in game graphs. We break a long-standing running time bound for MEC decomposition from the '90s by providing a sub-quadratic time symbolic algorithm.
