Analysis of Boolean Programs
Analysis of Boolean Programs
复制标题
布尔程序分析
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
M. Yannakakis
中科院分区：
文献类型：
--
作者：
Patrice Godefroid;M. Yannakakis
布尔程序是基于静态分析的软件模型检查的流行抽象领域。然而，对于该计算模型的模型检查的复杂性知之甚少。本文旨在通过对布尔计划的几种基本分析的最差复杂性进行全面研究，包括可及性分析，周期检测，LTL，CTL和CTL*模型检查。我们提出了这些问题的算法，并通过提供匹配的下限来表明我们的算法都是最佳的。我们还确定了特定的布尔计划类别，这些程序更容易分析，并将我们的结果与在俯卧撑模型检查中进行的先前工作进行比较。
Boolean programs are a popular abstract domain for static-analysis-based software model checking. Yet little is known about the complexity of model checking for this model of computation. This paper aims to fill this void by providing a comprehensive study of the worst-case complexity of several basic analyses of Boolean programs, including reachability analysis, cycle detection, LTL, CTL, and CTL* model checking. We present algorithms for these problems and show that our algorithms are all optimal by providing matching lower bounds. We also identify particular classes of Boolean programs which are easier to analyse, and compare our results to prior work on pushdown model checking.